v1.1.0 — the three headline results of Part III are unconditional
The three headline results of Part III now stand without hypotheses.
prop:tiltlclt (tilted local limit theorem) |
unconditional |
thm:rigid (rigidity of the gap series) |
a theorem, with no conditional clause |
thm:transfer (the transfer function) |
a theorem, with no conditional clause |
All three shared a single missing ingredient, prob:R1 — the Edgeworth expansion of the tilted local limit theorem in region R1, with explicit constants. It is now written out in Appendix A with every constant proved rather than measured, and it has had the independent reading this project requires before an argument counts as proved.
What changed since v1.0.0
The reading is on record, and it is described precisely. It arrived in three parts, each covering the text as it then stood: the three lemmas line by line (r162), the three repairs landed against them (r164), and the restated proposition with the T* construction and all five explicit constants of ρ, each re-derived from scratch and found to agree symbolically (r171). No single reading has covered the appendix as a whole, because the text changed between the parts in response to the earlier ones — the appendix head says so, because a reader who wants the stronger statement is entitled to know it has not been supplied.
Nothing was deleted. prob:R1 stays in the paper, restated as CLOSED with what closed it. The honest-scope entry records in its own text that it read "proof skeleton, with the analytic ingredients in place" until r171. A status that improves is still a status change, and a reader who cannot see the old one cannot audit the new one.
The remaining caveat is louder, not quieter. The algorithmic reading used to attach two conditions to the sentence about restart counts. One was ours and is gone. The other is not, and now stands alone: the uniformity of the terminal distribution is an assumption about the search, not a fact about the landscape.
A referee pass was run before this release. Thirteen statements, read in a fresh context by a reader given three jobs and nothing else — restate the claim, name what would falsify it, flag any single word doing hidden work. Three came back clear. It found three defects that twenty mechanical checks and a typesetter had passed over, and every one of them was a claim about our own evidence rather than about the mathematics: three incompatible descriptions of one reading; an absolute "conditional on nothing" sitting where its qualification was not; and a miscount of which statements had been waiting. All are fixed here. Log: lean/pnp/refpass_r175.log; procedure: tools/referee_pass.md.
What this still is not
None of it is peer-reviewed. Every theorem, proposition and lemma declares its status — proved, derived, measured, or conjectured — at the place where it is stated. A DOI makes a version permanent. It does not make it true.
Tool and computational resource disclosure
Carried out with AI language models (Anthropic's Claude) as tools, under the author's direction, following recommendation 01 for individual mathematicians of the Leiden Declaration on Artificial Intelligence and Mathematics, which the author has signed. Each manuscript names the tools, the versions, and the computational resources — one personal computer, no cluster and no accelerator — and names the provision of the Declaration that this work does not meet.
Licences
Code (lean/, the Python scripts): Apache-2.0, matching Mathlib. Manuscripts (paper/): CC BY 4.0.