Four pre-existing defects in /-- declaration doc comments under
IsingModel/AmbientLattice/, found while rewriting the /-! module headers of the same
files in wave 11 of #4984 (PR #5016).
None is a Lean-content defect: every statement and proof is correct, and every one of these
files builds with zero warnings. They are all prose claims in declaration docs. Wave 11
deliberately leaves all 87 /-- blocks in its file set byte-identical to main (the
practice established by waves 10a/10b), so they are filed here rather than fixed in that PR.
E1 — a malformed cardinality identity
IsingModel/AmbientLattice/MagnetizationInfiniteLambdaHSymmetry.lean:197-199, doc of
magnetizationΛ_ge_tanh:
specialization of correlationΛ_ge_tanh_pow_card at A = {i} where
|A|^1 = |A|.card = 1.
|A|^1 = |A|.card is not a well-formed claim — it equates a power of the cardinality with the
cardinality, and |A| and |A|.card denote the same thing written two ways. The intended
content is that A.card = 1 at a singleton, so Real.tanh (β * h) ^ A.card reduces to
Real.tanh (β * h).
The correct wording already exists in the same wave's file set, at
IsingModel/AmbientLattice/MagnetizationInfinite/TrivialSlices.lean:65, for the exactly
parallel magnetizationInfinite_J_zero:
(A.card = 1, so the power reduces to tanh(β·h))
E2 — the J = 0 slice labelled "infinite-temperature" (2 occurrences)
IsingModel/AmbientLattice/MagnetizationInfiniteHZeroJZero.lean:86 (doc of
correlationAlongExhaustion_J_zero_of_subset) and :126 (doc of correlationInfinite_J_zero)
both call the J = 0 slice the "infinite-temperature slice".
Infinite temperature is β → 0. J = 0 is the non-interacting slice, and in both theorems β
is free — correlationInfinite_J_zero in fact requires 0 < β through
Ferromagnetic ⟨0, h, β⟩, i.e. it is stated away from infinite temperature.
The repository already records the distinction explicitly, in the doc of
magnetizationInfinite_J_zero at
IsingModel/AmbientLattice/MagnetizationInfinite/TrivialSlices.lean:70-73:
§4.1 (non-interacting J = 0 slice; β is constrained only by
Ferromagnetic.hβ : 0 < β, not by the infinite-temperature limit β → 0)
So this is an internal inconsistency between two docs in the same directory, decidable without
consulting Glimm–Jaffe.
E3 — an unproved bound stated as an available fact
IsingModel/AmbientLattice/MagnetizationInfiniteSusceptibility.lean:43-46, doc of
susceptibilityInfinite:
susceptibility is not automatically bounded as the exhaustion grows: |χ_Λ(i)| ≤ 2·|Λ|,
which diverges with |Λ|.
No such bound exists anywhere in the tree (grep -rn "2·|Λ|" IsingModel/ returns this one
prose line). susceptibilityΛ unfolds to IsingModel.susceptibility, defined as
∑ j : ι, truncated2 G p i j, and the repo proves susceptibility_nonneg but no absolute
bound. The load-bearing point the sentence is making — that the number of summands grows with
the stage volume, so the stagewise family need not be bounded above — is true and provable;
the specific constant 2·|Λ| is not backed by anything here.
E4 — a citation to a lemma that does not exist
IsingModel/AmbientLattice/MagnetizationInfiniteSusceptibility.lean:97, doc of
susceptibilityInfinite_le_abs_h:
the pointwise comparison plus ciSup_le_ciSup gives the result.
ciSup_le_ciSup does not exist in mathlib at this pin (grep -rn "ciSup_le_ciSup" .lake/packages/mathlib/ is empty). The proof actually applies ciSup_mono
(Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean:165).
Related, already repaired in PR #5016
Two module-header claims in the same file set were false and are repaired by wave 11's
rewrite rather than filed here, since that PR rewrites those headers anyway:
MagnetizationInfiniteSusceptibility's header advertised "its 4 properties
(susceptibilityInfinite_eq_ciSup, _apply, _nonneg, _le_abs_h)". The module holds one
definition and three theorems, and susceptibilityInfinite_apply exists nowhere in the tree.BetaDerivative's header claimed 10 magnetizationAlongExhaustion regularity wrappers had
moved to BetaDerivativeMagnetization, which holds two.
Scope note
The scan behind this issue covered the /-- docs of all 87 declarations in wave 11's 14-file
set, not a sample: every backticked snake_case token in those docs was resolved against the
9782 declaration names in IsingModel/, leaving six unresolved, of which five are legitimate
(_gen is a suffix fragment; abs_choice, abs_nonneg, ciSup_le, le_antisymm are
mathlib) and one is E4. E1–E3 were found by targeted checks, so this list is complete for the
defect classes checked, not necessarily for all defect classes.
Refs #4984
Four pre-existing defects in
/--declaration doc comments underIsingModel/AmbientLattice/, found while rewriting the/-!module headers of the samefiles in wave 11 of #4984 (PR #5016).
None is a Lean-content defect: every statement and proof is correct, and every one of these
files builds with zero warnings. They are all prose claims in declaration docs. Wave 11
deliberately leaves all 87
/--blocks in its file set byte-identical tomain(thepractice established by waves 10a/10b), so they are filed here rather than fixed in that PR.
E1 — a malformed cardinality identity
IsingModel/AmbientLattice/MagnetizationInfiniteLambdaHSymmetry.lean:197-199, doc ofmagnetizationΛ_ge_tanh:|A|^1 = |A|.cardis not a well-formed claim — it equates a power of the cardinality with thecardinality, and
|A|and|A|.carddenote the same thing written two ways. The intendedcontent is that
A.card = 1at a singleton, soReal.tanh (β * h) ^ A.cardreduces toReal.tanh (β * h).The correct wording already exists in the same wave's file set, at
IsingModel/AmbientLattice/MagnetizationInfinite/TrivialSlices.lean:65, for the exactlyparallel
magnetizationInfinite_J_zero:E2 — the
J = 0slice labelled "infinite-temperature" (2 occurrences)IsingModel/AmbientLattice/MagnetizationInfiniteHZeroJZero.lean:86(doc ofcorrelationAlongExhaustion_J_zero_of_subset) and:126(doc ofcorrelationInfinite_J_zero)both call the
J = 0slice the "infinite-temperature slice".Infinite temperature is
β → 0.J = 0is the non-interacting slice, and in both theoremsβis free —
correlationInfinite_J_zeroin fact requires0 < βthroughFerromagnetic ⟨0, h, β⟩, i.e. it is stated away from infinite temperature.The repository already records the distinction explicitly, in the doc of
magnetizationInfinite_J_zeroatIsingModel/AmbientLattice/MagnetizationInfinite/TrivialSlices.lean:70-73:So this is an internal inconsistency between two docs in the same directory, decidable without
consulting Glimm–Jaffe.
E3 — an unproved bound stated as an available fact
IsingModel/AmbientLattice/MagnetizationInfiniteSusceptibility.lean:43-46, doc ofsusceptibilityInfinite:No such bound exists anywhere in the tree (
grep -rn "2·|Λ|" IsingModel/returns this oneprose line).
susceptibilityΛunfolds toIsingModel.susceptibility, defined as∑ j : ι, truncated2 G p i j, and the repo provessusceptibility_nonnegbut no absolutebound. The load-bearing point the sentence is making — that the number of summands grows with
the stage volume, so the stagewise family need not be bounded above — is true and provable;
the specific constant
2·|Λ|is not backed by anything here.E4 — a citation to a lemma that does not exist
IsingModel/AmbientLattice/MagnetizationInfiniteSusceptibility.lean:97, doc ofsusceptibilityInfinite_le_abs_h:ciSup_le_ciSupdoes not exist in mathlib at this pin (grep -rn "ciSup_le_ciSup" .lake/packages/mathlib/is empty). The proof actually appliesciSup_mono(
Mathlib/Order/ConditionallyCompleteLattice/Indexed.lean:165).Related, already repaired in PR #5016
Two module-header claims in the same file set were false and are repaired by wave 11's
rewrite rather than filed here, since that PR rewrites those headers anyway:
MagnetizationInfiniteSusceptibility's header advertised "its 4 properties(
susceptibilityInfinite_eq_ciSup,_apply,_nonneg,_le_abs_h)". The module holds onedefinition and three theorems, and
susceptibilityInfinite_applyexists nowhere in the tree.BetaDerivative's header claimed 10magnetizationAlongExhaustionregularity wrappers hadmoved to
BetaDerivativeMagnetization, which holds two.Scope note
The scan behind this issue covered the
/--docs of all 87 declarations in wave 11's 14-fileset, not a sample: every backticked snake_case token in those docs was resolved against the
9782 declaration names in
IsingModel/, leaving six unresolved, of which five are legitimate(
_genis a suffix fragment;abs_choice,abs_nonneg,ciSup_le,le_antisymmaremathlib) and one is E4. E1–E3 were found by targeted checks, so this list is complete for the
defect classes checked, not necessarily for all defect classes.
Refs #4984