docs(errata): PR1 of 2 — false-claim corrections from #4984 campaign errata - #5030
Draft
phasetr wants to merge 11 commits into
Draft
docs(errata): PR1 of 2 — false-claim corrections from #4984 campaign errata#5030phasetr wants to merge 11 commits into
phasetr wants to merge 11 commits into
Conversation
This was referenced Aug 11, 2026
Six module headers expanded the `vd` prefix as "van-den-Berg". In this repository `vd` abbreviates vertex-disjoint: `vdCompatiblePolymerFamilies` is defined by filtering on `IsCompatiblePolymerFamilyVertexDisjoint` (`ClusterExpansion/Families/VertexDisjoint.lean`), and no van den Berg result is cited anywhere in the tree. Verified: `grep -rn "Berg" IsingModel/ docs/ README.md scripts/` returned these six lines before and returns nothing after. Comment-only. Refs #4987 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
`freeEnergyAlongExhaustion_latticeGraph_eq_log_div_card` was documented as an "alternate form of `freeEnergyAlongExhaustion_eq_inv_card_mul_log` using the Fintype-card expression", but the lemma it names already uses `Fintype.card`, so no distinction is being drawn. The doc now records that the two conclusions are the same proposition and differ only in the ambient lemma delegated to, and points at `freeEnergyAlongExhaustion_latticeGraph_eq_inv_Λcard_mul_log` as the genuinely different cardinality spelling. Verified in Lean: `@..._eq_log_div_card = @..._eq_inv_card_mul_log := rfl` is accepted, at both the lattice-graph and the ambient layer. Comment-only; no declaration is added, removed or renamed. Refs #5000 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
`correlationInfinite_le_const_mul_beta_of_high_temp` was documented as holding "For `0 ≤ J`, `1 ≤ d`, `0 < b` ...", but its binder telescope carries no `1 ≤ d`; the dimension bound is dropped from the prose. `freeEnergyComplex_continuousAt_real_pos_h_latticeGraph` was documented as continuity at "real positive `h₀`", but it takes `(h₀ : ℝ)` with no positivity hypothesis and holds at every real `h₀`. The headline is corrected and the mismatch with the `_pos_h_` in the name is recorded. Both telescopes read off `#check`. Comment-only; the names are left alone, since renaming is a separate decision. Refs #5002 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
correlation length Three sites asserted that `−log tanh(βJ)`, or a finite-region infimum of per-pair pseudo-masses, *is* the inverse correlation length. The tree proves only bounds: `latticeMass_le_neg_log_tanh_betaJ`, `latticeMass_two_sided_bound`, and `onAxisInverseCorrelationLength_le_neg_log_tanh` are all inequalities, and no equality with that rate exists anywhere. * `UnconditionalFiniteRegionLipschitz.lean` header: "faithful inverse-correlation-length rate" -> "direct-path rate", the name the neighbouring `LatticeMassHighTemperature/UpperBound.lean` already uses. * `finiteRegionPseudoMassDist`: the claim that the finite infimum "is the genuine inverse correlation length restricted to `A`" is replaced by the faithful-radius statement plus an explicit note that no relation to `latticeMass` is proved here. Measured at the merge base: the file sets mentioning `finiteRegionPseudoMassDist` (24) and `latticeMass` (85) intersect in zero files. * `docs/index.md` #4333 row: it simultaneously claimed the `hprofile` of #4330-#4332 "is now an unconditional theorem" and, in parentheses, that the theorem is at a different rate. The row now states that the unconditional bound does not discharge that binder -- `#check` shows the binder is `pseudoMassG α ρ (−log(βJ·2d))` at a fixed radius while the theorem is `pseudoMassG α (latticeDistance d x z) (−log tanh(βJ))` -- and names the rate-agnostic engine as what it does discharge. Lean changes are comment-only. `citation_audit.py` is unaffected: the findings/ratchet counts are identical with the merge base's `docs/index.md`. Refs #5005 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
The docstring of `truncated4Infinite_J_zero_of_pairwise_distinct` called the closed form `-2·tanh(β·h)^4` "(non-vanishing)". `Ferromagnetic ⟨0,h,β⟩` only requires `0 ≤ h`, so `h = 0` is admissible and there the form is `0`. Replaced by the zero/nonzero split over the admissible range, matching the already-corrected sibling in `TwoPointTruncatedTrivialSlices.lean`. Both halves checked in Lean: `-2 * Real.tanh (β * 0) ^ 4 = 0`, and `-2 * Real.tanh (β * h) ^ 4 < 0` for `0 < h`, `0 < β`. The surrounding `-2·t⁴ ≤ 0` sentence was correct and is kept. Comment-only. Refs #5008 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
`partitionFunctionAlongExhaustion_high_temp_expansion_h_zero_pow_two_lt_of_nonempty` was documented as holding "under nonempty volume". Its hypotheses are `0 < β * J` and `0 < |E|`; it takes no `(Λ.volume n).Nonempty`, unlike the `_of_nonempty` wrappers in `HighTemperatureBoundsRatioLogFeNonempty`, which do take it and convert it with `hne.card_pos`. The doc now names the hypotheses it actually has and records the divergence from its siblings. Telescope read off `#check`. Comment-only; the duplicate declaration itself is left in place. Refs #5011 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
* `magnetizationΛ_ge_tanh`: "`|A|^1 = |A|.card = 1`" is not a well-formed identity. Replaced by the wording already used for the parallel `magnetizationInfinite_J_zero`: `A.card = 1`, so the power reduces to `tanh(β·h)` -- which is exactly what the proof's `Finset.card_singleton` rewrite does. * `correlationAlongExhaustion_J_zero_of_subset` and `correlationInfinite_J_zero` called the `J = 0` slice the "infinite-temperature slice". Infinite temperature is `β → 0`; `J = 0` is the non-interacting slice, and `β` is free in the first while the second requires `0 < β` through `Ferromagnetic`. Both now say what `MagnetizationInfinite/TrivialSlices.lean` already says. * `susceptibilityInfinite`: the doc asserted `|χ_Λ(i)| ≤ 2·|Λ|` as an available fact. No such bound exists in the tree (that string occurs nowhere else). Replaced by the provable point the sentence was making -- `susceptibility` sums `truncated2` over the volume, so the summand count grows with the stage and no stage-uniform bound is proved here. * `susceptibilityInfinite_le_abs_h`: cited `ciSup_le_ciSup`, which does not exist at this mathlib pin. The proof applies `ciSup_mono`. Comment-only. Refs #5017 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
* `partitionFunctionΛ_high_temp_expansion_h_zero_closed_evenSubgraphs` carried an odd number of `**` markers, so its bold span did not close where it appeared to. Stray marker removed. * Declaration docs across `Analyticity*` use `pFE`, `vdSum` and `ε(t)` as if they named definitions. `vdPolymerFamilies_sum` and its `.erase ∅` variant have no definition at all -- they are written out in full in every statement -- and neither `pFE` nor `vdSum` is introduced anywhere. Each affected module header now carries the expansion and says these are prose shorthands rather than library names, extending the legend device the same headers already use for `Ξ` and `ε`. `AnalyticityLambdaMayerRecurrenceEpsilon` and `AnalyticityLambdaMayerPfeEdgeBounds` are unchanged: their headers already introduce `ε t` as a shorthand with no definition behind it, which is the only shorthand their declaration docs use. Comment-only. Refs #5019 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
`partitionFunctionΛ_high_temp_expansion_h_zero_upper_bound` was documented as a "ℤ^d wrapper". `#check` shows it is stated for an arbitrary `G : SimpleGraph V` over an arbitrary `V` with `Λ : Finset V`; nothing in its signature or proof mentions `latticeGraph`, `cubicExhaustion` or any other ℤ^d construct. In the `AmbientLattice/` tree ℤ^d vocabulary is what has to be absent, since the layer is graph-generic and the specializations live downstream in `Concrete/`. Reworded to the form its siblings in the same file already use, naming the wrapped `IsingModel.partitionFunction_high_temp_expansion_h_zero_upper_bound`. The provenance token in the sentence is re-emitted unchanged. Comment-only. Refs #5022 Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
difference is not a ratio * `freeEnergyInfinite_high_temp_h_zero_upper_bound_exp_uniform` was advertised as "globally tighter than `freeEnergyInfinite_le_uniform_upper_bound` at `h = 0` (the cosh-based bound)". Both claims are wrong. The right-hand sides are the same real number under this theorem's hypotheses -- `log 2 + |β|·(|J|·c + |0|) = log 2 + β·J·c` for `0 ≤ J`, `0 < β`, checked in Lean -- and the named lemma's conclusion contains no `Real.cosh` at all; `cosh` enters only through the lower bound used for coboundedness. * `freeEnergyInfinite_high_temp_h_zero_ratio_bound` and its `_beta_zero` companion are headlined as "ratio upper bound" while their conclusions bound a difference, which their own doc bodies display two lines below. Both headlines corrected, each noting that the `_ratio_bound` in the name does not describe the statement. Renames are a separate decision and are not made here. Comment-only. Refs #5026 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
PR 1 of 2 in the capped errata-correction window authorized per Codex's final ruling in
.self-local/reports/dev-review-4984-post-triage-remainder.md(item 1: "scope down andAUTHORIZE NOW, hard cap 2 PRs / ~12-20 h"). This PR corrects false/misleading substantive prose
(declaration docs, module headers,
docs/index.md) found during the #4984 header-rewritecampaign. It does not touch declaration deletion, renaming, imports, umbrellas, D1/#5028, or any
mechanical citation population (those are excluded per the ruling and/or handled elsewhere).
Scope (verified live against merge base
532fe328a9bcf67d9797790ae07052cc310d3439beforescaffolding)
vdas "van-den-Berg" instead of "vertex-disjoint", and carry zero ratchet charges so no wave will reach them #4987 — whole issue: six merged headers expandvdas "van-den-Berg" instead of"vertex-disjoint"; zero ratchet charges so no wave will reach them.
(gated refactoring, out of scope here per the issue's own post-campaign-triage comment); only
the false-documentation claims in scope.
own comment, Parts 1 and 3 are PARKED).
with the inverse correlation length, one self-contradictory inside
docs/index.md.FourPoint.lean:373's "(non-vanishing)" closed-form claim is false ath = 0(upstream twin of the defect PR wave 9 of 16 #5006 fixed for M2)._pow_two_lt_of_nonemptywrapper that takes no nonemptiness hypothesis, plus its doc comment (wave 10a scope) #5011 — documentation portion only (item 2, the doc comment asserting a hypothesis itsstatement does not carry; items 1 and 3 are PARKED per the issue's own comment).
cardinality identity,
J=0mislabelled as infinite temperature, unproved susceptibility bound,nonexistent mathlib lemma cited).
/--declaration-doc defects in AmbientLattice/Analyticity* (found in #4984 wave 12) #5019 — sub-findings E2-E3 only (E2: malformed bold marker inAnalyticityLambdaCapstones.lean; E3: informal shorthandspFE/ε(t)/vdSumthat resolve tono repo
def). E1 (task-ID/PR-number references in declaration docs) is excluded from this PR.ExpBounds.leancalls a genericSimpleGraph Vtheorem a "ℤ^d wrapper" (wave-11 inverted-vocabulary defect, found in #4984 wave 13) #5022 — whole issue:ExpBounds.leancalls a genericSimpleGraph Vtheorem a "ℤ^d wrapper"(inverted-vocabulary defect).
/--doc-comment defects in the AmbientLatticeSum layer (found in wave 15 of #4984) #5026 — sub-findings E1-E2 only (E1: a bound advertised as strictly sharper than one it isnumerically equal to; E2: "ratio bound" naming/prose on statements that bound a difference). E3
(task-ID/PR-number references) is excluded from this PR.
Exclusions (binding, per the ruling)
No declaration deletion or rename, no import/umbrella changes, no D1/#5028 work, no
PR #Nprovenance cleanup, no corpus-wide audit, no new scanners/gates/baselines, no blanket
substitutions, no third PR.
Test plan
grep -rn "sorry" IsingModel/stays empty (doc-only edits; no proof-term changes expected).#print axiomsperlean-verify-auditbefore merge.dev-cross-cli-review) before merge.this campaign have repeatedly been found stale).
Notes
This is a draft PR opened with the standard empty-commit scaffold; implementation is a
separate dispatch.
Refs #Ntrailers are used (notCloses #N) because issue-by-issue closuredecisions are made after each fix is verified, and several of the above issues (#5000/#5002/#5011)
retain a PARKED portion that stays open regardless of this PR's outcome.
Refs #4987
Refs #5000
Refs #5002
Refs #5005
Refs #5008
Refs #5011
Refs #5017
Refs #5019
Refs #5022
Refs #5026