All issues

Search results

Errata: pre-existing /-- doc-comment defects in the AmbientLatticeSum layer (found in wave 15 of #4984)

Status: Open.

#5026 In phasetr/ising-model;

· phasetr opened on Aug 10, 2026

Errata: the RandomCurrent tree anchors the random-current representation at FV §3.7 (it is §3.10.6, pp. 143-145) and the switching lemma at GJ §5.1 Thm 5.1.2 / FV Thm 9.35 (it is FV Lemma 3.55, p. 144)

Status: Open.

#5024 In phasetr/ising-model;

· phasetr opened on Aug 10, 2026

Errata: ExpBounds.lean calls a generic SimpleGraph V theorem a "ℤ^d wrapper" (wave-11 inverted-vocabulary defect, found in #4984 wave 13)

Status: Open.

#5022 In phasetr/ising-model;

· phasetr opened on Aug 10, 2026

Errata: pre-existing /-- declaration-doc defects in AmbientLattice/Analyticity* (found in #4984 wave 12)

Status: Open.

#5019 In phasetr/ising-model;

· phasetr opened on Aug 10, 2026

Errata: four prose defects in AmbientLattice declaration docs (malformed cardinality identity, J=0 mislabelled as infinite temperature, unproved susceptibility bound, nonexistent mathlib lemma cited)

Status: Open.

#5017 In phasetr/ising-model;

· phasetr opened on Aug 10, 2026

Errata: a verbatim-duplicate _pow_two_lt_of_nonempty wrapper that takes no nonemptiness hypothesis, plus its doc comment (wave 10a scope)

Status: Open.

#5011 In phasetr/ising-model;

· phasetr opened on Aug 9, 2026

Errata: FourPoint.lean:373's "(non-vanishing)" closed-form claim is false at h=0 (upstream twin of PR #5006's fixed M2)

Status: Open.

#5008 In phasetr/ising-model;

· phasetr opened on Aug 9, 2026

Errata: Glimm-Jaffe Theorem 4.2.3 is the convergence theorem, not GKS-II, and there is no Proposition 4.2.3

Status: Open.

#5007 In phasetr/ising-model;

· phasetr opened on Aug 9, 2026

Errata: three sites identify the direct-path rate (or a finite-region infimum) with the inverse correlation length, one of them self-contradictory inside docs/index.md

Status: Open.

#5005 In phasetr/ising-model;

· phasetr opened on Aug 9, 2026

Errata: 4 further pairs of alpha-identical declarations in the LGC Complex layer, 2 doc comments stating hypotheses their statements do not carry, and a stale import-preservation note

Status: Open.

#5002 In phasetr/ising-model;

· phasetr opened on Aug 9, 2026

Errata: 6 pairs of alpha-identical Lean declarations (3 in the LGC concrete layer, 3 graph-generic), plus a doc comment stating a distinction that does not exist

Status: Open.

#5000 In phasetr/ising-model;

· phasetr opened on Aug 9, 2026

Errata: Glimm-Jaffe Proposition 4.2.4 does not exist, and Corollary 4.3.5's page is 63 not 62

Status: Open.

#4993 In phasetr/ising-model;

· phasetr opened on Aug 8, 2026