Paper X: Universal Residual Seeds and Conditional Occupied-System Completion

Download original file

This is the original TeX manuscript source. Use the paper’s PDF for typeset equations.

Read the typeset paper

Read this chapter with formatted equations

1 \section*{A route through the complete reading edition}
2 \addcontentsline{toc}{section}{Reading route and current contract}
3 The central distinction is between a residual root, a coherent branch, and an
4 occupied packet in a carrier. Sections 2--7 develop the finite and formal
5 machinery. Sections 8--11 assemble its arithmetic uses under stated hypotheses.
6 The residue-counting continuation is retained in Appendix C. Appendix D states
7 the later checked conditional endpoint, while Appendix E supplies the worked
8 visual atlas.
9 
10 \begin{tabularx}{\linewidth}{@{}p{.24\linewidth}X@{}}\toprule
11 Read for & Follow this route\\\midrule
12 The mathematical core & Residual partition, reconstruction, smooth and singular counts, cohomology packets, directed seed rank.\\
13 The arithmetic assembly & Common coefficient data, finite Frobenius separation, explicit carrier summands, and inverse-limit-closed profiles.\\
14 The formal contract & The separate Lean guide prints the terminal source and all three direct dependency modules, with a statement register and hypothesis-by-hypothesis explanation.\\
15 The finite examples & Atlas pages V1--V30 show the actual residue tables, projector tests, countermodels, and norm-character examples.\\\bottomrule
16 \end{tabularx}
17 
18 \paragraph{The live ledger is conditional 20/20.}
19 This is the recorded closure of the amended formal contract, not a certification
20 of every historical prose sentence at its broadest possible interpretation.
21 The final source is over the rational absolute Galois group. Its carrier data,
22 constituent comparisons, and completed source family are explicit inputs.
23 The 17/20 passages attached to Block 27 and the scalar/Mellin continuation remain
24 historical records. A later stronger residual-system attempt records 19/20 and
25 no promoted endpoint. These records concern different source contracts.
26 
27 \paragraph{Two outputs require two sets of inputs.}
28 The terminal theorem proves that a transported target family exists and that the
29 declared summand can be recovered inside a supplied compatible carrier. It does
30 not identify those two objects. An application that needs such an identification
31 must supply its comparison. Likewise, zero multiplicities are permitted by the
32 formal assembly, so a nonzero conclusion retains a separate nonzero premise.
33 
34 \paragraph{Proofs, checks, and publication.}
35 The exact mathematical arguments, computational illustrations, and inherited
36 Lean records have different evidential roles. The October 10 reading pass corrected
37 the digit-extraction display, reconciled checkpoint wording, and rebuilt the
38 reader set without a fresh Lean kernel check. The separately dated October 20
39 verification records identify the newly selected source, production execution,
40 owned-declaration audit, and bounded checks. The unrecovered October 16--17
41 packages are not substituted into that evidence. The complete historical
42 frontmatter and its original limits are preserved in Appendix B rather than
43 placed in front of the current table of contents.

Back to source controls

Back to Paper X: Universal Residual Seeds and Conditional Occupied-System Completion