CORE24_PROOF_GUIDE.md
Machine Native Reasoning
CORE24_PROOF_GUIDE.md
1 # Core 2.4 — proof guide
2
3 ## Statement
4
5 Fix a field K, a finite-dimensional state space V, finite candidate and action
6 catalogues, a distinguished candidate theta0, and a linear protected readout Q.
7 Let A_a = T_a^theta0. All operation words are executed left to right.
8
9 Define E as the linear span of A_w (T_a^theta - A_a) v over every finite word w,
10 action a, candidate theta and initial vector v. The formal result establishes
11 that the following are equivalent:
12
13 1. Q T_w^theta = Q A_w for every fixed candidate theta and every word w, as
14 operator identities on the whole state space.
15 2. E is contained in ker Q.
16 3. There is a surjective linear projection to a common carrier, shared linear
17 updates and a matched readout, intertwining every candidate action.
18
19 The canonical witness is V/E. The same quotient predicts any finite sequence
20 of candidate/action pairs, allowing the candidate to change at every step.
21 The reference need not be identified from observations; it is supplied as one
22 of the candidates, exactly as in the source.
23
24 ## Proof route
25
26 `CommonQuotient.lean` defines the actual word map, generator set and span.
27 It proves range containment, reference and candidate invariance, agreement
28 implying invisibility, actual quotient updates, quotient readout, the converse,
29 and arbitrary switching. The word executor is explicitly related to the
30 inherited `Komorebi.MachineTheory.run` convention.
31
32 The key forward implication tests the assumed word-operator identity not only
33 at v but at T_a^theta v. This is why an all-initial-vector premise matters.
34 The noncommuting example in the fourth module demonstrates the failure of a
35 one-initial-state replacement.
36
37 `CommonQuotientInterface.lean` defines `CommonModel`, the full carrier and
38 projection data, and constructs `canonicalModel`. A given common model yields
39 agreement rather than serving as an assumed answer. Arbitrary function-valued
40 updates and readouts also imply the agreement when their commuting equations
41 hold. A separate universal comparison map factors every other common projection
42 through V/E, is surjective, preserves actions and is unique. The span is
43 independent of the chosen reference among actual candidates.
44
45 `DiscrepancyClosure.lean` starts from the sum of discrepancy ranges and repeatedly
46 adds reference images. It proves monotonicity, containment, plateau completeness
47 and stabilization by `Module.finrank K V`. The main endpoints are
48 `source_core24` and `source_core24_reference`.
49
50 `CommonQuotientExamples.lean` supplies the source's three-coordinate family,
51 a noninjective two-coordinate projection, delayed observable return, fixed-
52 initial agreement with a switching failure, reference independence, an unrelated-
53 reference counterexample and zero discrepancy for identical candidates.
54
55 ## Source correspondence
56
57 The original theorem is `r:common`, Core 2.4, at canonical source lines 233–250.
58 Setup is at lines 224–232. `THEOREM_MAP.json` retains those exact source records.
59 The source's finite-dimensional, finite-catalogue assumptions are explicit in
60 the two source-facing endpoints. Several supporting algebraic statements do not
61 need them; this is proved generality, not a changed source premise.
62 The third source condition says “updates” and “readout” without repeating their
63 linearity. `agreement_of_function_factor` covers that more permissive reading,
64 while the positive construction provides linear maps. The formal source theorem
65 therefore does not obtain its equivalence by imposing an unsupported necessary
66 assumption on arbitrary source data.
67
68 ## Interpretation
69
70 The canonical quotient removes exactly the propagated inter-candidate
71 discrepancies. It is not asserted to be the smallest predictor for Q. It need
72 not reconstruct the full state, identify hidden dynamics, learn an encoder or
73 be numerically stable. Infinite-dimensional finite-stage stabilization is not
74 claimed. The underlying quotient and classical choices are mathematical data,
75 not a verified executable numerical algorithm.
76
77 ## Checks
78
79 `checks/CheckCommonQuotientAPI.lean` checks raw all-vector agreement, supplied
80 linear factors, function-valued factors, the distinguished raw reference,
81 finite stabilization and arbitrary switching. Nine negative fixtures remove
82 or contradict decisive conditions in exact rational examples.
83
84 `scripts/check_common_quotient.py` is a separate exhaustive exact regression on
85 F_2^2 with two candidates and two actions. It enumerates all 65,536 operator
86 families and 262,144 scalar-readout contracts. State-pair reachability is run to
87 exhaustion for both fixed candidates and arbitrary switching, then compared with
88 an independently iterated discrepancy span and canonical coset dynamics.
89 69,184 readout contracts are admissible, and 8,640 have immediate invisibility
90 without propagated invisibility. These counts are finite cases, not theorems
91 or empirical measurements. The cumulative gates rerun this checker separately
92 from the Lean proofs and compare its exact result records.