The reader carries three distinct contracts. A larger date or a larger numerator does not make their hypotheses interchangeable.
| Record | What it establishes |
|---|---|
| Historical 17/20 | Block 27 and the scalar/Mellin continuation. Claims 9.1, 9.2, and 11.1 were partial in those revisions. |
| Checked 20/20 | The amended conditional occupied-system assembly. Completed source members, closed target profiles, compatible carrier presentations, and local comparisons remain explicit inputs. |
| Later 19/20 | A stronger residual-system attempt with no promoted terminal endpoint and an unavailable pinned Lean executable. It is a different contract, not a failed recompilation of the checked source. |
Two conclusions, not an unstated identification
The terminal theorem constructs a transported target family and independently recovers a summand of the supplied carrier. To identify them requires an explicit comparison. The carrier result is pointwise at an arbitrary coefficient place. Recovering carriers at every place needs the relevant presentations there. Zero multiplicity is allowed. Nonzero occupancy needs a separate nonzero premise.
What the examples verify
The appendix supplies reproducible finite examples and exact Python checks. No plotted pixel decides a congruence, rank, determinant, root, or character sum. The original Lean sources and recorded audits are preserved. The October 10 editorial release performed no fresh Lean compilation. The separate October 20 production replay is reported in the Lean guide; it introduces no new formal theorem.
Read this as
A completed conditional theorem is a theorem with its hypotheses, not a claim that every arithmetic application supplies them.