wave 15 of 16 - #5025
Merged
Merged
Conversation
Scaffolding-only start for wave 15 (AmbientLatticeSum residue + IsingModel.lean root umbrella). No implementation yet. Refs #4984
…iteBounds Wave 15 of 16 of the #4984 header-inventory-claim campaign, first of four new-authoring files. `InfiniteBounds.lean` had no `/-!` block at all (its sole ratchet charge was `MISSING_MODULE_DOC`), so this is authorship rather than rewording. Every claim is derived from the printed Lean type of the three declarations (`lake env lean` `#check` against the branch's own oleans), not from source text or declaration names: `freeEnergyInfinite` unfolds to `Filter.limsup` of the stage sequence; the two upper bounds take `[Nonempty V]` and the edge-count hypothesis while the value equation takes neither; and the assertion that the general bound's right-hand side, evaluated at `h = 0` under `0 ≤ J` and `0 < β`, is the same real number as the zero-field bound's was checked in Lean rather than asserted. Comment-only: the comment-stripped token stream, the comment-stripped line list and the comment-aware import list are byte-identical to `main`, and the three `/--` declaration doc blocks are byte-identical too. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…iteHighTemp Wave 15 of 16 of the #4984 header-inventory-claim campaign, second of four new-authoring files and the largest of them at 14 declarations. `InfiniteHighTemp.lean` had no `/-!` block (sole charge `MISSING_MODULE_DOC`). Every claim is derived from the printed Lean type of each declaration, not from source text or declaration names. The header states the binder picture verified over all fourteen — `[DecidableEq V]`, `[Nonempty V]`, the stagewise `Fintype` family and the edge-count hypothesis on every one of them — and discloses the single exception that carries two ambient graphs, hence two stagewise `Fintype` instances, with its edge-count hypothesis on the larger graph alone. The nine zero-field statements are described by the shape of their conclusions rather than by their names; in particular the two called `_ratio_bound*` bound a difference, not a ratio, and the header says difference. Comment-only: the comment-stripped token stream, the comment-stripped line list and the comment-aware import list are byte-identical to `main`, and the fourteen `/--` declaration doc blocks are byte-identical too. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…additiveConvergence Wave 15 of 16 of the #4984 header-inventory-claim campaign, third of four new-authoring files. `SuperadditiveConvergence.lean` had no `/-!` block (sole charge `MISSING_MODULE_DOC`). Every claim is derived from the printed Lean type of the four declarations. The three structural hypotheses are quoted as they appear in those types; `DisjointTowerHypotheses` is described as the `Prop`-valued structure bundling exactly them; and the three convergence shapes are distinguished by how the upper bound on the stage sequence arrives and whether the structural hypotheses arrive singly or bundled. The negative universals — no `[Nonempty V]`, no `Ferromagnetic p`, no sign condition on any parameter anywhere in the module — were checked against all four types, not inferred. The Glimm-Jaffe citation was verified by page-scoped extraction of page 68 of the local PDF (book page 68 = PDF page 84), which carries Proposition 4.6.1 and the sentence quoted; the header also records that the proposition is stated there for a translation-invariant ferromagnetic nearest-neighbour interaction and is not proved in that section, so that the formalised hypotheses are not mistaken for the book's. Comment-only: the comment-stripped token stream, the comment-stripped line list and the comment-aware import list are byte-identical to `main`, and the seven `/--` doc blocks (including the structure's field docs) are byte-identical too. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…rella Wave 15 of 16 of the #4984 header-inventory-claim campaign, fourth and last of the new-authoring files and the campaign's top-level umbrella case (wave 12 handled the `AmbientLattice/Analyticity.lean` umbrella the same way). Umbrella-specific verification. The file was confirmed to hold zero local declarations before the header was written: it has 549 `import` lines, one blank line and nothing else — no declaration, no namespace, no `open`, no `set_option`. The header therefore describes the aggregation it performs and claims no theorem of its own. Reachability was computed over the whole tree: 1915 of the library's 1916 modules are reachable from this file, the one exception being `IsingModel.TestGenerators`, which the separate `test` library imports directly (`test/IsingModel/Generators.lean`, `test/IsingModel/SentinelProps.lean`); the header names that exception rather than claiming totality. Every subject area named was checked to be reachable from here, and the two-layer description was checked against the printed types of `IsingModel.partitionFunction` (a graph on a `[Fintype ι]` vertex type) and `IsingModel.Ambient.partitionFunctionΛ` (a `Λ : Finset V` inside an arbitrary `G : SimpleGraph V`). The `/-!` block follows the imports rather than heading them because Lean rejects a module docstring before the import section ("invalid 'import' command, it must be used in the beginning of the file", confirmed by experiment); the header says so, so that its position does not read as an accident. Comment-only: the comment-stripped token stream, the comment-stripped line list and the comment-aware import list are byte-identical to `main` — in particular all 549 imports are untouched and in the same order. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…module docstrings Wave 15 of 16 of the #4984 header-inventory-claim campaign. These three files carried no module docstring but did carry four mid-file `Moved:` blocks announcing how many wrappers had migrated to a named sibling — the campaign's `RELOCATION` class. Each file now opens with a `/-!` header describing what it is for, and the `Moved:` blocks are gone. The four relocation pointers were checked against the live tree before removal, and all four were accurate: `AmbientLatticeSumFreeEnergy` holds 13 declarations, `AmbientLatticeSumGe- Ferromagnetic` 12, `AmbientLatticeSumFInfHSymMono` 6 and `AmbientLatticeSumLogZ` 14. The claim each block made about import paths was checked too: all four siblings remain in the transitive import closure of the file that pointed at them, through `AmbientLatticeSum/InducedUnion.lean`. Every replacement claim is derived from the printed Lean type of the 32 declarations covered. Two exclusivity claims were machine-checked rather than eyeballed: in `TrivialSlices.lean` exactly three statements take `[Nonempty V]` and exactly one names two graphs, and no statement in the file assumes `Ferromagnetic p` or any sign condition; in `TendstoAtTop.lean` `Ferromagnetic p` is the only Prop-valued hypothesis and `[Infinite V]`, `[DecidableEq V]` and the stagewise `Fintype` instance are the only instance binders. Following wave 11's rejected phrasing about exhaustions, `LambdaSuperadditivity.lean`'s remark about the shell `Λ.volume (n + 1) \ Λ.volume n` is scoped to the growth axis — an `Exhaustion` requires `Monotone` there and not strict increase — rather than claiming that monotonicity is all an exhaustion asks, which would be false of its `exhaust` field. Comment-only: the comment-stripped token stream, the comment-stripped line list and the comment-aware import list are byte-identical to `main` on all three files, and their 32 `/--` declaration doc blocks are byte-identical too. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
… descriptions Wave 15 of 16 of the #4984 header-inventory-claim campaign. These four root siblings opened with "Narrow child module for the N ..." followed by a name roster (the `NARROW_CHILD` class, plus one `PAREN_COUNT` in `AmbientLatticeSumFreeEnergy.lean`). Each now describes what its statements say and what they assume, with no roster and no count of the module's contents. Every claim is derived from the printed Lean type of the 45 declarations covered. The universals were machine-checked over those types: all 12 statements of `AmbientLatticeSumGeFerromagnetic.lean` assume `Ferromagnetic p` and none requires a nonempty volume; none of the 14 in `AmbientLatticeSumLogZ.lean` assumes `Ferromagnetic p` as a bundle or a nonempty volume; in `AmbientLatticeSumFreeEnergy.lean` exactly the 7 bounds and closed forms carry a nonemptiness hypothesis and the 6 symmetry and monotonicity statements carry none; in `AmbientLatticeSumFInfHSymMono.lean` exactly the 4 monotonicity statements take `[Nonempty V]` and the edge-count hypothesis, and the 2 symmetry statements have no Prop-valued hypothesis at all. Each monotonicity family's sign conditions are listed per item rather than as one coordinated list, since the three directions do not share them. One genuine falsehood was repaired rather than renumbered. `AmbientLatticeSumLogZ.lean` claimed its eight shapes existed "for both Λ and AlongExhaustion versions"; the two closed forms exist at the finite-volume layer only, and 8 x 2 = 16 contradicts the module's own count of 14. The new header states that those two have no counterpart along an exhaustion, and adds the checkable fact — confirmed in Lean — that both hold at the empty volume, where each side is 0. Comment-only: the comment-stripped token stream, the comment-stripped line list and the comment-aware import list are byte-identical to `main` on all four files, and their 45 `/--` declaration doc blocks are byte-identical too. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…keys Wave 15 of 16 of #4984 closes 13 charges over 13 keys, so the baseline moves 180/108 -> 167/95. The diff removes exactly the 13 rows this wave's 11 files carried and nothing else: 4 `MISSING_MODULE_DOC` (`IsingModel.lean`, `AmbientLatticeSum/InfiniteBounds`, `/InfiniteHighTemp`, `/SuperadditiveConvergence`), 4 `RELOCATION` (`AmbientLatticeSum/LambdaSuperadditivity` twice, `/TendstoAtTop`, `/TrivialSlices`), 4 `NARROW_CHILD` (`AmbientLatticeSumFInfHSymMono`, `AmbientLatticeSumFreeEnergy`, `AmbientLatticeSumGeFerromagnetic`, `AmbientLatticeSumLogZ`) and 1 `PAREN_COUNT` (`AmbientLatticeSumFreeEnergy`). The wave's freeze comment pre-registered 180/108 -> 167/<=97; the keys landed at 95 because no two cleared rows shared a key. `--check-baseline-drift` against `origin/main` reports "the pin moved only where this diff explains it", and `--check` is level at 167/95. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Each sentence is replaced by one that the declarations in the same file support. * SuperadditiveConvergence: `G` is not unconstrained -- the super-additivity hypothesis names it in every shape and `BoundedEdgeDensity G Λ` in the two shapes that obtain the upper bound instead of assuming it. * LambdaSuperadditivity: only the partition function, its logarithm and the cardinality-weighted free energy rise under a disjoint union; the unweighted `freeEnergyΛ` is compared across a union nowhere in the module. * AmbientLatticeSumLogZ: scope the absence of an along-exhaustion counterpart to this module, since both counterparts exist under `AmbientLattice/SpecialCases`. * TrivialSlices: the closed form asks for the `Fintype` instance on the induced edge set, so what it does not ask of `Λ` is nonemptiness. * IsingModel: the umbrella carries this docstring besides its import lines. Lean content is untouched: outside the `/-!` blocks every file is byte-identical to the merge base, all 51 `/--` blocks in these five files included. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Round-2 review found two residual inaccuracies of the same family as the round-1 Low-1 charge, both in prose this PR introduces. TrivialSlices: the `DisjointTowerHypotheses.of_log_linear_card` sentence said the builder "asks only for" cardinality additivity and a non-degenerate first stage, omitting its instance binders. The declaration also binds `[DecidableEq V]` and `[∀ n, Fintype (inducedGraph G (Λ.volume n)).edgeSet]` -- exactly the two instance binders `DisjointTowerHypotheses` itself carries -- so the sentence now names them. This repairs the untouched twin of the sentence six lines above it, which round 1 had already corrected. TendstoAtTop: "`Ferromagnetic p` is the only Prop-valued hypothesis" was false. `Infinite` is declared `class Infinite (α : Sort*) : Prop`, so `[Infinite V]`, named in the same sentence, is Prop-valued too, whereas `Fintype` and `DecidableEq` are data. The claim is now split: `Ferromagnetic p` is the only explicit hypothesis, and the Prop-valued binders are `Ferromagnetic p` together with `[Infinite V]`. Every binder claim was checked against the telescope Lean itself prints, and the sweep was extended to every exclusivity and binder-kind claim in all eleven files of the wave; the other two kind claims (`DisjointTowerHypotheses` is `Prop`-valued; the two field-symmetry statements have no Prop-valued hypothesis at all) verify as written. Prose only: outside the `/-!` blocks both files are unchanged, all doc comments and imports are byte-identical, `lake build` is warning-free over 4944 jobs and the header-inventory ratchet stays at 167/95. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Wave 15 of 16 —
AmbientLatticeSumresidue +IsingModel.leanroot umbrellaHeader-intension-rewrite campaign (#4984), wave 15 of 16. Scope: 11 files (6 in
IsingModel/AmbientLatticeSum/, 4 directIsingModel/AmbientLatticeSum*.leanroot siblings, 1IsingModel.leanroot umbrella), 13 charges, 98 declarations, 4MISSING_MODULE_DOC. Frozenagainst
origin/main=ea52604caf027f1dfa4d84b65f8ac5a06fd8ed38(wave 14 / PR #5023's mergecommit). No overlap with wave 11 (
AmbientLattice/MagnetizationInfinite/, disjoint path).Prose-only: module docstrings rewritten to state each declaration's actual binder/hypothesis
intension (Prop- vs data-valued, exclusivity of "only"/"exactly" claims, instance-binder
inventories), verified against machine-printed
#check/#printtypes on this branch's ownoleans, never against source text or declaration names. Zero Lean logic change (see AC4 below).
Review history — 3 rounds, 8 findings total, all fixed and independently re-verified
.self-local/reports/dev-review-4984-w15.md): CHANGES REQUESTED, 6 findings(Med-1
SuperadditiveConvergence.lean:29"nothing here constrains it"; Med-2LambdaSuperadditivity.lean:13"can only raise these quantities"; Med-3AmbientLatticeSumLogZ.lean:14-15"no counterpart along an exhaustion"; Low-1TrivialSlices.lean:14"no hypothesis on Λ whatever"; Low-2IsingModel.lean:556"consists ofimport lines alone"; Low-3 implementer-report miscount of
/--blocks). All 6 fixed in commita7e6c1a2, each confirmed independently by Codex cross-review (2 of 6 found only by thisreview, diff-hunk-scoped Codex missed the whole-tree-context findings Med-3/Low-3).
.self-local/reports/dev-review-4984-w15-round2.md): re-verified all 6 round-1fixes as genuinely FIXED, then ran a full exclusivity/unscoped-negative sweep across all 11
files and found 2 new residual Low findings that neither round 1 nor Codex had caught:
Low-4
TrivialSlices.lean:19-20("the builder asks only for …" omitted theFintypeinstancebinder from its own enumeration) and Low-5
TendstoAtTop.lean:13-14(misclassified[Infinite V]as not Prop-valued, whenInfiniteis in fact declared aPropclass inmathlib). Both are the same defect class as round 1's findings, recurring 6 lines apart
within the same wave. Both fixed and pushed in commit
d7ba0764..self-local/reports/dev-review-4984-w15-round3.md): APPROVE, zero newfindings. Both round-2 residuals independently re-verified as genuinely fixed against
machine-printed binder telescopes (not against the implementer's report). Independent
re-derivation of the implementer's full 11-file sweep, plus re-check of every previously
cleared exclusivity claim, found nothing regressed. Independent Codex cross-review agreement.
AC1–AC8 evidence table
python3 scripts/header_inventory_claim_ratchet.py --check→ PASS, exact match; this wave is prose-only so the ratchet is unchanged by rounds 2–3, only by the round-1 fix commita7e6c1a2).lake env lean#check/#printoutput on this branch's own oleans, cross-checked against mathlib source where a class's Prop/Type-valuedness was load-bearing (e.g.Infinite,Fintype,Decidable).git diff --statfor every fix commit touches only/-! ... -/module docstrings; round 3 additionally proved this mechanically via comment-stripped, whitespace-normalised SHA-256 equality ofTrivialSlices.leanandTendstoAtTop.leanacrossa7e6c1a2..d7ba0764(1b76ac85cd7f,e4ba288a0d3d).lake build(0 warnings,warningAsError = true+weak.linter.mathlibStandardSet = true),lake exe GKSTest,header_inventory_claim_ratchet.py --checkPASS at 167/95,audit_gate.py --fullPASS, citation audit PASS,import_dag_contractPASS, zero Japanese (rg "[ぁ-んァ-ン一-龯]"→ none), line length ≤ 93 codepoints (100 limit) including em-dash prose.a7e6c1a2(round-1 fixes),d7ba0764(round-2 fixes) — both push-verified againstorigin/docs/4984-w15-ambientlatticesum-headers, working tree clean at each round's review.[DecidableEq V], stagewiseFintype,[Infinite V],[Nonempty V]) re-derived per-file from a comment-stripped binder inventory, not copied from the implementer's report; round 3 additionally spot-checked all previously-cleared exclusivity claims across all 11 files for regression.Final state
Ratchet baseline after this wave: 167 charges / 95 keys (wave 16 starts from this number).
Reports:
.self-local/reports/dev-review-4984-w15.md,-round2.md,-round3.md;.self-local/reports/dev-implement-4984-w15.md,-followup.md,-followup2.md.Refs #4984