# Core 2.4 source correspondence

| Source object or obligation | Actual formal object or endpoint |
|---|---|
| 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` |
| Words executing the first listed action first | `wordMap`, `wordMap_eq_run`, `wordMap_append` |
| Propagated span E | `generators`, `discrepancy`, `generator_mem` |
| All initial vectors, every fixed candidate, every finite word | `ObservableAgreement`, checked again as pointwise equations in the API |
| E lies in the protected readout kernel | `agreement_iff_invisible` |
| Reference invariance and invariance under every candidate | `reference_invariant`, `candidate_invariant` |
| Actual quotient V/E and shared updates | `quotientUpdate`, `quotientUpdate_candidate` |
| Descended protected readout | `quotientReadout`, `quotientReadout_mk` |
| Existence of a complete common model | `CommonModel`, `canonicalModel`, `agreement_iff_commonModel` |
| Necessary direction for arbitrary function updates/readout | `agreement_of_function_factor` |
| Candidate switching between operations | `switchedMap`, `switched_quotient`, `switching_output` |
| Finite span iteration terminates | `seed`, `closureStep`, `stage`, `bounded_plateau`, `stage_finrank_eq` |
| Complete source endpoint | `source_core24`, `source_core24_reference` |

The canonical source, source PDF and 27-entry source index are unchanged. The
existing result number, title, lines and printed page are checked against that
index by the complete verifier. Source maps only record an accepted formal
status when the current complete gates and comparison pass. The program's
English prose is not certified merely because a declaration has a similar name.

The source speaks about a common linear quotient, not necessarily a minimal
predictor. The formalization retains that distinction. Choosing another actual
reference yields the same discrepancy submodule, but arbitrarily replacing the
reference by a system outside the family can invalidate the equivalence.

Review level: source-to-formal reasoning review within this development, plus
source-facing compiler checks and explicit counterexamples. No external
independent review or historical-priority judgment is asserted.