Machine Native Reasoning

Download original file

Read the formatted document

1 # Core 2.4 source correspondence
2 
3 | Source object or obligation | Actual formal object or endpoint |
4 |---|---|
5 | Fixed candidate family T and distinguished reference A | `T : Theta -> A -> V ->_l[K] V`, explicit `theta0`; `source_core24_reference` also accepts R with `T theta0 = R` |
6 | Words executing the first listed action first | `wordMap`, `wordMap_eq_run`, `wordMap_append` |
7 | Propagated span E | `generators`, `discrepancy`, `generator_mem` |
8 | All initial vectors, every fixed candidate, every finite word | `ObservableAgreement`, checked again as pointwise equations in the API |
9 | E lies in the protected readout kernel | `agreement_iff_invisible` |
10 | Reference invariance and invariance under every candidate | `reference_invariant`, `candidate_invariant` |
11 | Actual quotient V/E and shared updates | `quotientUpdate`, `quotientUpdate_candidate` |
12 | Descended protected readout | `quotientReadout`, `quotientReadout_mk` |
13 | Existence of a complete common model | `CommonModel`, `canonicalModel`, `agreement_iff_commonModel` |
14 | Necessary direction for arbitrary function updates/readout | `agreement_of_function_factor` |
15 | Candidate switching between operations | `switchedMap`, `switched_quotient`, `switching_output` |
16 | Finite span iteration terminates | `seed`, `closureStep`, `stage`, `bounded_plateau`, `stage_finrank_eq` |
17 | Complete source endpoint | `source_core24`, `source_core24_reference` |
18 
19 The canonical source, source PDF and 27-entry source index are unchanged. The
20 existing result number, title, lines and printed page are checked against that
21 index by the complete verifier. Source maps only record an accepted formal
22 status when the current complete gates and comparison pass. The program's
23 English prose is not certified merely because a declaration has a similar name.
24 
25 The source speaks about a common linear quotient, not necessarily a minimal
26 predictor. The formalization retains that distinction. Choosing another actual
27 reference yields the same discrepancy submodule, but arbitrarily replacing the
28 reference by a system outside the family can invalidate the equivalence.
29 
30 Review level: source-to-formal reasoning review within this development, plus
31 source-facing compiler checks and explicit counterexamples. No external
32 independent review or historical-priority judgment is asserted.

Back to source controls