README_v0.10.0_PREDECESSOR.md
KZFC and Residual Reflection
README_v0.10.0_PREDECESSOR.md
1 # Komorebi KZFC residual reflection v0.10.0
2
3 ## Completed mathematical block
4
5 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:
6
7 Guard(K) -> SmallProductClosed(K).
8
9 Consequently, in every model of that explicit ZFC theory:
10
11 Guard(K) -> Extension(K) -> Fine(K) -> Compactness(K) -> Reflection(K).
12
13 All size witnesses, ranking graphs, function images, selections, relation tables and assignments are internal sets. External well-foundedness and external cardinality are not assumptions.
14
15 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.
16
17 ## Principal declarations
18
19 All are in `Komorebi/Foundation/InternalProductArithmetic.lean`.
20
21 * `smallProductClosed_of_guard`
22 * `model_zfc_productArithmeticSentence`
23 * `internal_extension_implies_fine`
24 * `internal_extension_implies_compactness`
25 * `internal_extension_implies_reflection`
26 * `model_zfc_extensionCompactnessSentence`
27 * `model_kzfc_compactness_witness`
28
29 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.
30
31 ## Scope and remaining work
32
33 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.
34
35 No uncountable existence, independence, relative consistency, new consistency strength or priority claim is made. No arbitrary derived-residual classification is added.
36
37 ## Contents
38
39 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.
40
41 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.
42
43 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.