Detailed ordinary proofs and construction records
On this page · Permalink · Source line 2213
The following appendices typeset the complete selected current construction proofs from Blocks 166 and 167. Their source notation, numbered source subsections, exact hypotheses, and mathematical scope are retained. The synthesis appendices state the final combined results; component notes also document narrower lemmas, alternative routes, and failed interpretations. In particular, the separate classical arithmetic-induction application in the leading-capacity note is not an input to the direct constructor.
Historical research identifiers, filenames, and references to earlier blocks are preserved to make the arguments traceable to the accompanying Markdown files. Earlier “pending” review language is superseded by the retained internal review records included with those source files, at their recorded dates and scopes. No external peer review is claimed. Negative capacity conclusions concern the original maximal-type carrier; the later low-rank enlargement does not repeal them. These appendices are ordinary mathematical proofs. Neither their typesetting nor the inherited formalization certificates constitute a fresh Lean proof of these arithmetic results or of Conjecture 66.