KZFC and Residual Reflection

Komorebi KZFC residual reflection v0.10.0

Completed mathematical block

The arbitrary-model arithmetic premise isolated in v0.9.0 is now proved. From the unchanged encoded ZFC axioms and the unchanged regular-uncountable cardinal guard:

Guard(K) -> SmallProductClosed(K).

Consequently, in every model of that explicit ZFC theory:

Guard(K) -> Extension(K) -> Fine(K) -> Compactness(K) -> Reflection(K).

All size witnesses, ranking graphs, function images, selections, relation tables and assignments are internal sets. External well-foundedness and external cardinality are not assumptions.

The proof uses bounded internal rankings and rowwise image bounds, rather than the full infinite-cardinal-square/order-type development proposed in the previous outline.

Principal declarations

All are in Komorebi/Foundation/InternalProductArithmetic.lean.

• smallProductClosed_of_guard
• model_zfc_productArithmeticSentence
• internal_extension_implies_fine
• internal_extension_implies_compactness
• internal_extension_implies_reflection
• model_zfc_extensionCompactnessSentence
• model_kzfc_compactness_witness

The last theorem assumes a model of KZFC and extracts a compactness witness inside it. It does not produce a model or prove the added sentence true.

Scope and remaining work

The internal compactness-to-filter-extension converse remains unfinished. Thus this release completes the forward implication but not the full arbitrary-model equivalence. The external/concrete classification from earlier checkpoints is preserved.

No uncountable existence, independence, relative consistency, new consistency strength or priority claim is made. No arbitrary derived-residual classification is added.

Contents

The source inventory is 48 mathematical modules and 502 named theorem declarations, of which 8 modules and 63 declarations are new. Supporting and syntax-interpretation lemmas count toward these totals. All 40 predecessor mathematical modules are preserved byte-for-byte.

See BLOCK_10_REPORT.md and THEORY.md for the proof, PROOF_BOUNDARY.md for the exact nonclaims, REPRODUCE.md for compiler commands, and verification/RESULTS.json with verification/process_record.json for the active run status. Historical attempts are not current PASS evidence.

Compiler binaries and dependency caches are not shipped. The pinned Lean 4.34.0-rc2 portable runtime and Mathlib revision are recorded in the reproduction instructions.