docs(4984): wave 16/16 — final header-intension rewrite (ClusterExpansion/TranslationInvariance/LGC/etc.) - #5027
Merged
Merged
Conversation
State the geometric-majorant results by their binders and hypotheses: an arbitrary type with no instance assumption, a graded Finset with a per-element weight bound and a fibre-cardinality bound quantified over every natural number, and the finite and closed geometric conclusions. Verified against the printed types of both declarations. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Separate the purely real-analytic geometric-moment identity from the polymer estimates, name the smallness parameter and the summand actually estimated, distinguish the abstract-gas form from its even-gas specialization, and state the concluding support-card bound. Verified against the printed types of all seven declarations. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
State the complex-activity estimate by its binders, its two Kotecky-Preiss smallness hypotheses measured at the norm of the activity, and its conclusion. Verified against the printed type. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Describe the site and configuration bijections, the pointwise simp lemmas, the translation- invariance instance and its transfer to induced graphs, and the two energy layers, distinguishing the identities whose binders carry no ambient graph from those that do. Verified against the printed types of all twelve declarations. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
State the spin-product and correlation transport identities with their actual hypotheses, and the two set-level identities that prepare the exhaustion layer. Verified against the printed types of all four declarations. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…e header Record the stagewise identity together with the dite dichotomy that shapes its proof, and the infinite-volume identity with the Ferromagnetic hypothesis it needs; correlationInfinite is the supremum over stages, not a limit. Verified against the printed types of both declarations and of correlationAlongExhaustion, correlationInfinite and Exhaustion.shift. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Name the boxes and the ferromagnetism argument of freeEnergyInfinite_linearBox, state each monotonicity direction with its own sign hypotheses, derive positivity and non-vanishing from the log 2 lower bound, and state the field-symmetric convergence. Verified against the printed types of all six declarations and of linearBox. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Same shape as the 1D box header, with the width hypothesis and the anisotropic box: the stripe grows in the first coordinate while the second stays at the fixed width. Verified against the printed types of all six declarations and of stripeBrick2D. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
SignedSums: replace the structural-split inventory by what the two signed sums are, how they are evaluated, how isomorphism invariance is transported, and the complete-graph boundary values, noting that the component lemma carries no instance assumption. TwoPointCapstonePrereqs: replace the prerequisite count by the support-cardinality bound and by the parity equivalence that restates the closed high-temperature expansion in htSubgraphSum form. Verified against the printed types of all eighteen declarations, private ones included. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…sion AnalyticSideConditions: replace the relocation claim by the content of the branch data, the equicontinuity route and what each constructor consumes and computes. RelCompact: give the module a header stating the shared hypotheses and conclusion and how much Lee-Yang data each form supplies or produces, and rewrite the two declaration docstrings that carried the pilot bookkeeping so that the alpha-identical pair is described as sharing one statement with two proof routes. Verified against the printed types of all nine declarations and of the branch-data structures; the GJ 4.6.2 citation was checked against the text. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
…sion These three files are the wave-9 residue. Replace the narrow-child counts and the name inventories by what truncated4TwoPoint and truncated4Infinite are on the lattice graph and what each symmetry or trivial slice asserts. The symmetry header also drops a false uniform proof claim: the r-u exchange is a composite of the two adjacent ones, not an unfold plus Finset extensionality. Verified against the printed types of all nine declarations and of both truncated definitions. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Replace the possessive property count and the name list by why a common box is needed, what carries the transport, and what dualCutInBox satisfies, spelling out the anchored dart-reachability hypotheses. Verified against the printed types of all eight declarations and of dualSupport, dualCutSub, BoundaryDart, DartReachable and the contour bound; the FV 3.7.2 citation is unchanged. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
167 charges / 95 keys -> 151 charges / 79 keys, exactly the wave-16 pre-registration: all sixteen Lean-lane keys are cleared and the residual 151/79 is the docs lane alone. Refs #4984 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Each correction was re-derived from the printed Lean type before the wording changed, not taken from the review verbatim. MayerSumDiffSupportBound: the tsum bound is uniform in v only. The order n is bound by the tsum in fixedVertexGasTouching_tsum_le, so there is no order binder for a uniformity claim to attach to. SignedSums: the complete-graph boundary values apply the two general D evaluations directly (allSignedSubgraphSum_eq_zero_of_edgeFinset_nonempty and _eq_one_of_edgeFinset_empty), not the card-transfer statement the previous connective pointed at. DualCutInBox: the anchored hypothesis is DartReachable F d (phi (d.left)), whose unfolding is a ReflTransGen chain from the dart's dual edge to the anchor's, the opposite of the stated direction. ConfigEquiv: edgeSpin is Sym2.lift of a product of two spin signs, a per-edge spin product and not an energy, so the layer it belongs to is transport rather than energy. Comment-only: the comment-stripped token stream of all four files is byte-identical to the parent commit. 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.
Purpose
Wave 16 of 16 (FINAL wave) of the header-intension rewrite campaign tracked by
#4984. Rewrites the last 16 charged Lean-lane files so that the Lean lane of
#4984 reaches zero charges. Scope frozen by
dev-issue-manager:.self-local/reports/dev-issue-manager-4984-wave16-freeze.md.Scope (16 files / 16 charges / 16 keys / 84 declarations, 8 new module-doc headers)
Family breakdown (files / charges / decls / new-authoring):
ClusterExpansion/(direct)ClusterExpansion/AlternatingCompleteGraph/TranslationInvariance/Concrete/LatticeGraphCorrelation/(wave-9 residue)Concrete/LinearBrick/Concrete/StripeBrick2D/AmbientComplexAnalyticity/Peierls/Work-type split: 8 reword files / 44 declarations, 8 authoring files / 40 declarations
(48% of the wave's declarations are new-authoring).
Per-file manifest (verified against the actual merged diff,
git diff main..originfor thisbranch — 17 files, 16 header files + 1 ratchet baseline re-pin):
IsingModel/AmbientComplexAnalyticity/AscoliData/Constructors/AnalyticSideConditions.lean(RELOCATION, reword)IsingModel/AmbientComplexAnalyticity/ClosedBallPatches/RelCompact.lean(PREDICATE_COUNT, reword)IsingModel/ClusterExpansion/AlternatingCompleteGraph/SignedSums.lean(PREDICATE_COUNT, reword)IsingModel/ClusterExpansion/GeometricFiberSum.lean(MISSING_MODULE_DOC, author)IsingModel/ClusterExpansion/MayerSumDiffSupportBound.lean(MISSING_MODULE_DOC, author)IsingModel/ClusterExpansion/MayerSumDiffSupportBoundComplex.lean(MISSING_MODULE_DOC, author)IsingModel/ClusterExpansion/TwoPointCapstonePrereqs.lean(PREDICATE_COUNT, reword)IsingModel/Concrete/LatticeGraphCorrelation/SiteIndepMagTwoPointTruncated4Symm.lean(NARROW_CHILD, reword)IsingModel/Concrete/LatticeGraphCorrelation/TwoPointTruncatedHigherTruncated4.lean(NARROW_CHILD, reword)IsingModel/Concrete/LatticeGraphCorrelation/TwoPointTruncatedSwapsTrunc4.lean(NARROW_CHILD, reword)IsingModel/Concrete/LinearBrick/Monotone.lean(MISSING_MODULE_DOC, author)IsingModel/Concrete/StripeBrick2D/Monotone.lean(MISSING_MODULE_DOC, author)IsingModel/Peierls/DualCutInBox.lean(POSSESSIVE_COUNT, reword)IsingModel/TranslationInvariance/ConfigEquiv.lean(MISSING_MODULE_DOC, author)IsingModel/TranslationInvariance/FiniteVolume.lean(MISSING_MODULE_DOC, author)IsingModel/TranslationInvariance/InfiniteCorrelation.lean(MISSING_MODULE_DOC, author)scripts/audit/header_claim_baseline.tsv(ratchet re-pin, data only, expected)The 3
Concrete/LatticeGraphCorrelation/files above are a wave-9 omission,swept into this wave per
dev-issue-managergovernance finding G3 (wave 16 isthe terminal freeze; no future freeze pass exists to catch orphans).
Pre-registered ratchet move
167 charges / 95 keys → 151 charges / 79 keys (both exact, confirmed by round 2's
independent re-run of
header_inventory_claim_ratchet.py --check: baseline == live). Bothfigures reconcile with the 16-row TSV delta (8
MISSING_MODULE_DOC+ 3NARROW_CHILD+1
POSSESSIVE_COUNT+ 3PREDICATE_COUNT+ 1RELOCATION, each count 1). This move takesthe Lean lane to zero charges repo-wide (
MISSING_MODULE_DOC= 0 repo-wide); the residual151/79 is entirely the
docs/index.md(149) +docs/architecture-import-layers.md(2) docslane, which is out of scope for every wave W5–W16 per #4984's own body. Per round 2's
non-blocking observation (O1 in
.self-local/reports/dev-review-4984-w16-round2.md), this 167→151 drop is a proxy: atleast one retired row (
PREDICATE_COUNT SignedSums.lean) corresponds to a claim thatsurvives, true, in a grammar-unrecognized shape. The accurate framing is "Lean-lane
recognized-charge count is now zero", not "all inventory-style phrasing has been
eliminated."
Implementation and review history
Round 1 implementation (
.self-local/reports/dev-implement-4984-w16.md): all 16 filesrewritten (8 new module-doc headers authored via
lake env lean/#checktype-levelverification, 8 rewords), 84 declarations covered. Round 1 review
(
.self-local/reports/dev-review-4984-w16-round1.md, head2c71d65d): CHANGES REQUESTED— 1 Med + 3 Low, all comment-only:
MayerSumDiffSupportBound.lean:25— "uniform invand in the order" asserteda quantifier structure (
n) the printed type does not carry (nis bound by thetsum);fixed by dropping "and in the order".
SignedSums.lean:25— the connective "this yields" mis-attributed the boundaryvalues to the card-transfer result rather than the two evaluation theorems; fixed by
rewording the connective.
DualCutInBox.lean:23— "reachability … from the dart chosen" had theDartReachabledirection reversed (the hypothesis runs fromdto the anchor); fixed byflipping the direction in prose.
ConfigEquiv.lean:27— callededgeSpin(a per-edge spin-product transportlemma, not an energy) part of "the energy identities"; fixed by removing the category slip.
All four fixed in commit
2985c7d9, comment-only (AC4-verified).Round 2 review (
.self-local/reports/dev-review-4984-w16-round2.md, head2985c7d9):APPROVE, zero findings. Each of the 4 fixes re-derived independently against printed Lean
types (not the implementer's report). Independent Codex cross-review: APPROVE, full
agreement with
dev-review. Also ran a campaign-closing sanity pass re-deriving 11 furtherdeclarations (beyond round 1's full 84-declaration coverage) chosen from the highest-risk
claim classes (quantifier structure, iff-direction, exclusivity) — zero further findings.
Test plan
scripts/header_inventory_claim_ratchet.py --checkshows ratchet moved to 151/79 (PASS,re-confirmed independently at round 2, K0–K4 conservation checks all PASS,
MISSING_MODULE_DOC= 0 repo-wide,NON_PROSE_ANCHOR= 0,UNTERMINATED_COMMENT= 0)lake buildwarning-free (PASS, exit 0, zerowarninglines; the twoinfo: Try this: ring_nflines are pre-existing, in files untouched by this wave)grep -rn "sorry" IsingModel/empty (0 hits)lake env lean/#checkprintedtypes (wave 13/14 type-level verification methodology — never source text or declaration
names); all 84 declarations across all 16 files checked at round 1, plus 11 further
declarations re-checked at round 2's closing sanity pass
zero findings, full agreement with
dev-review)Campaign status (this is the final wave)
This PR closes the Lean lane of the #4984 header-intension-rewrite campaign (waves 1–16, all
merged after this PR). Per
dev-issue-manager's wave-16 governance pass(
.self-local/reports/dev-issue-manager-4984-wave16-freeze.md), merging this PR is acampaign terminus, not a wave boundary: the docs-lane residual (151/79,
docs/index.md+docs/architecture-import-layers.md) was never part of any wave and remains open/unscoped;22 open errata issues found during the campaign (#4987 onward) remain open and unresolved;
neither is authorized to auto-continue into. #4984 itself stays OPEN — this PR does not
close it. A campaign-terminus status comment recording this is posted separately on #4984.
Refs #4984