You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
PR Checklist — SL-A to SL-E Lemma 5.1 Ingredient Thread
2026-07-12 GOVERNANCE NOTE (dev-issue-manager, OFF-BOOK): This entire thread targets GJ's literal "everywhere continuity" closing sentence of Thm 17.5.1, which GJ's own printed proof (pp. 311–312) does not itself establish (Lipschitz m⁻ + Lemma 17.5.2 sandwich only, constant C>1 never shown to collapse). docs/index.md:1764–1771 labels every OZ Wall-#2 brick produced by this thread "off-book optional", each row stating primary GJ Thm 17.5.1 rigorous content (gj_theorem_17_5_1_rigorous) is already done. No "Ornstein-Zernike"/"Simon-Lieb" theorem exists in the GJ book body (bibliography-only hit). This thread is OFF-BOOK, not an in-scope GJ-book proposition; see #4405 "GOVERNANCE RECONSTRUCTION" and #4259 Next-concrete-step for the STOP-and-ask finding (do not resume M2/B4 without a fresh explicit user authorization decision).
Purpose: Track the staged build of Lemma 5.1 (GJ eq. (17.5.1), random-current weight edge-partition factorization) toward the lsc half of Theorem 17.5.1.
Thread: Part of Group 1a (random-current / Simon-Lieb D-family explicit tracking for hLogLip gate relocation).
Status: SL-D₁ COMPLETE (SL-A through SL-D₁b all MERGED, axiom-free); SL-D₂ CORRECTED + SUPERSEDED (2026-07-12, .self-local/tex/rc-oz-lemma51-SLD2-inequality.tex) — user provided Aizenman 1982 (Commun. Math. Phys. 86, 1-48) PDF at ~/junk/0-pdf-for-translation/Aizenman.1982.p48.*.pdf and directed engagement (user's own concrete provisioning act, not agent self-authorization). TRACKING CORRECTION: "Aizenman Lemma 4.1" does NOT exist in the source (verified pdftotext full-text search: zero hits); the subgraph-conditioning content is Aizenman §9, Lemma 9.2 eq.(9.11) p.25 + Lemma 9.3(iii)/(iv) eq.(9.13)-(9.14) pp.25-26 (both Griffiths/GKS-monotonicity, inequality-driven, not an exact switching identity) and §3 Lemma 3.2 p.7 (combinatorial switching identity, used elsewhere in the paper, not for this ingredient). math-before-code re-derivation (rc-oz-lemma51-SLD2-inequality.tex) further found: (a) hLogLip is a pure upper bound (log-derivative = nonnegative excess, already proven by merged Current.hasDerivAt_log_correlation_beta), so SL-D₂ only needs the one-sided inequality version, which closes on existing merged repo infra (correlation_deleteEdges_le = Aizenman Lemma 9.3; correlation_inducedGraph_eq_weightSum_ratio re-instantiated = Aizenman Lemma 9.2) — it is not an irreducible research core; (b) the entire SL-A/B/C/D pivotal-fiber route is in fact bypassable for hLogLip via two already-merged bricks (Current.doubledSourcefree_edgeExcess_eq_truncated4pt + correlation_beta_deriv_le_lebowitz); the genuine remaining research core is the OZ two-point-ratio summability bound(1/⟨σxσy⟩)Σₑ(⟨σxσu⟩⟨σyσv⟩+⟨σxσv⟩⟨σyσu⟩) + |E|/⟨σxσy⟩ ≤ (K/J)·d(x,y) — a convolution/decay estimate, independent of SL-D₂. SL-E gated on this OZ ratio bound, not on SL-D₂.
✅ SL-A/B/C/D₁/M1 = mainline infra (not wasted work)
SL-A (edge-partition), SL-B (component extraction), SL-C (avoiding-set/bridge-uniqueness), SL-D₁ (range-independence, weight factorization Σ_C=(βJ)·Ξ_int·Ξ_ext) and M1 (Lebowitz convolution upper bound) are standing, axiom-free, reusable infra for the random-current / OZ route; they are not superseded/deleted, only advanced on the critical path. M1 discharges the false "crude Lebowitz blow-up" diagnosis and reduces hLogLip to the genuine remaining core.
SL-D₂ (subgraph-conditioning, exterior collapse): re-framed 2026-07-12 as a one-sided inequalityΞ_ext ≤ ⟨σbσy⟩_Λ·weightSum^{C^c}(∅), which closes on already-merged repo infra (correlation_deleteEdges_le + correlation_inducedGraph_eq_weightSum_ratio re-instantiated) modulo bounded ↑Λ-vs-V subtype plumbing (SL-D₂(a), moderate, not a research core). SL-D₂ is off the hLogLip critical path (see below) but remains available as an alternative route if needed.
SL-D₂.0 math-before-code CORRECTED (2026-07-12): .self-local/tex/rc-oz-lemma51-SLD2-inequality.tex — sourced against the actual Aizenman 1982 PDF (§9 Lemma 9.2/9.3, not the non-existent "Lemma 4.1"); supersedes the equality-framed rc-oz-lemma51-SLD-collapse.tex verdict.
SL-D₂(a) plumbing (optional, only if pivotal route retained): Current.exteriorWeightSum_le_correlation_mul_weightSum_empty, bounded subtype/edge-set identification.
▶ TRUE REMAINING CORE (genuine research residual, on the critical path): the OZ two-point-ratio summability bound (1/⟨σxσy⟩)·Σₑ(⟨σxσu⟩⟨σyσv⟩+⟨σxσv⟩⟨σyσu⟩) + |E|/⟨σxσy⟩ ≤ (K/J)·d(x,y)
(GJ p.312 OZ content: two-leg decay convolution is O(d(x,y)) uniformly). This is NOT SL-D₂ and NOT the pivotal fiber; it is reached directly from two already-merged bricks (Current.hasDerivAt_log_correlation_beta + correlation_beta_deriv_le_lebowitz).
✅ M1 MERGED (PR feat(gj-17.5-oz-M1): Lebowitz convolution upper bound on log-derivative #4495, main cf1909a0): Route-B Lebowitz convolution upper bound on log-derivative — ∂_β log⟨σxσy⟩ ≤ (J/⟨σxσy⟩)·∑_e L_uvxy (OZ ratio reduction, outer-shell brick, axiom-free via merged infra). Discharges false "crude Lebowitz blow-up" diagnosis from earlier design, reduces target to OZ summability. New file IsingModel/Inequalities/SourcefreeConnectionLebowitzConvolutionBound.lean. M1 does NOT stand alone; M2 (sharp lower-bound two-point decay, multi-session research core) + SL-E capstone required to close.
▶ M2 IN QUEUE: Sharp matching two-point lower bound (OZ 壁; genuine multi-session research) = the OZ two-point-ratio summability bound itself. Convolution/decay estimate (GJ p.312, FFS Ch.12 backbone-tail content; not in Aizenman 1982). Bypasses SL-D₂ entirely. Upon M2 discharge + SL-E capstone assembly, Lemma 5.1/hLogLip closes.
B1 (degenerate-edge Lebowitz bound via GKS-II + tanh, axiom-free, PR feat(gj-17.5-oz-M2-B1): degenerate-edge Lebowitz bound via GKS-II (axiom-free) #4496, main ec186b46): degenerate edges (u or v ∈ {x,y}) contribution S_deg ≤ (deg(x)+deg(y))·J/tanh(βJ)·d(x,y) via existing infra (gks_second + single-edge tanh bound); axiom-free, hedge is hypothesis (not axiom); does NOT close M2 (B2/B3/B4 remain).
B2 — RETRACTED/FALSE for d≥2 (design report .self-local/reports/design-oz-M2-nondegenerate.md, 2026-07-12): off-axis crossed-edge geometric tube sum. The claimed poly(0)·D tube bound is FALSE: latticeDistance is ℓ¹ (non-unique fat geodesics); excess-0 shell alone has ∏_i(|Δ_i|+1) points (e.g. d=2 diag: (n+1)²), so ∑_a ρ^{d(a,x)+d(a,y)} = ρ^D·∏_i(|Δ_i|+1+c) is O(D^d), not O(D). Do NOT commit as designed.
B3 — RETRACTED (design report, 2026-07-12): dimension-dependent non-degenerate reduction does NOT close even granting H_low as hypothesis: substituting H_low only removes the (ρ_+/ρ)^D factor; the residual ∏_i(|Δ_i|+1+c) is still O(D^d) (AM-GM), so S_nd ≤ K·D is unreachable via this route. B3 is not H_low-gated-closable; it depends on the (false) B2 tube bound.
B4 (matching two-point lower bound H_low, genuine OZ 壁): the irreducible research core — two-point decay matching ⟨σxσy⟩ ≥ c·ρ^{d(x,y)} (rate ρ ≥ 2d·tanh(βJ)) uniformly at the summation rate. GJ p.312 / OZ bubble / FFS Ch.12 backbone-tail content; binding-pair pseudo-mass deriv infra structurally incapable. From-scratch multi-session research (3-6 PR, Aizenman §9 / FFS 12 / repo-absent bottleneck).
⚠️ hedge/B0 (single-edge tanh lower bound ⟨σ_u σ_v⟩ ≥ tanh(βJ)): Unconditional discharge requires gated refactor (private-helper relocation; no inline axiom/sorry); do NOT attempt direct axiomatization. B1 uses hedge as hypothesis (present route, no obstacle).
Then: OZ summability design: fresh dev-design for (E1) geometric two-point decay input, (E2) matching lower-leg bound (twoPointFunction_ge_tanh_betaJ_pow_dist, already present), (E3) convolution/summability count — (E3) is the genuine multi-session OZ core (M2 B1–B4 component assembly).
Then: Staged implementation PRs per design, each axiom-free / Tier-1-clean / reviewed, scoped strictly to Group 1a Lemma 5.1 / hLogLip.
SL-E (capstone assembly): binding the OZ ratio bound → hLogLip → §17.5.1 lsc. Gated on the OZ summability core above, not on SL-D₂.
Roadmap Note
Scope: Group 1a (Lemma 5.1 SL-A→E) only; no spillover to Group 1b/1c or untracked research. Each ingredient lands axiom-free/Tier-1-clean before next.
Canonical status: #4259 (Current status + Next concrete step); #4405 (Group 1a section).
2026-07-12 CORRECTION (issue-manager governance — B2/B3 design finding, .self-local/reports/design-oz-M2-nondegenerate.md): Independent design verification of M2's non-degenerate decomposition found the prior "B2/B3 no new hypothesis / YES-graded" checklist entries and the tex .self-local/tex/rc-oz-lemma51-M2-convolution-estimate.tex §sec:verdict grading (B2="YES", B3="YES given H_low") to be WRONG (overclaim), retracted:
B2 is FALSE for d≥2 (not a difficulty-graded-low brick, the claimed proposition is mathematically false): latticeDistance is ℓ¹, whose geodesics are non-unique/"fat" (multinomial count); the excess-0 shell alone between x,y has ∏_i(|Δ_i|+1) points (e.g. d=2, y=(n,n): (n+1)² points), so the two-focus vertex-convolution generating function ∑_a ρ^{d(a,x)+d(a,y)} = ρ^{D}·∏_i(|Δ_i|+1+c) is O(D^d), not the claimed poly(0)·D tube bound.
B3 does not close even granting H_low as hypothesis: substituting H_low into the ratio only kills the (ρ_+/ρ)^D factor; the residual ∏_i(|Δ_i|+1+c) term is still O(D^d) (AM-GM), not O(D), so S_nd ≤ K·D is NOT obtained. B3 is not "H_low-gated axiom-free"; it is unreachable by this route regardless of hypothesis.
H_low itself is suspect as stated (rate ρ≥ρ_+=2d·tanh(βJ), ℓ¹ metric): the true on-axis decay rate is ~tanh(βJ) (directed-path/SAW dominated), far below ρ_+; H_low as ⟨σxσy⟩ ≥ c₀·ρ_+^{D} is false for large D under the true asymptotics. The log(2d) gap between the merged upper rate (2d·tanh, ℓ¹ SAW-entropy overcount) and the merged easy lower rate (tanh) is an artifact of upper-bound looseness (isotropic ℓ¹ overcounting), not a missing matching lower bound; the correct fix direction is a sharper anisotropic/Euclidean-rate upper bound, not H_low.
Genuine core: the non-degenerate S_nd bound requires the true OZ mechanism (Euclidean rate + diffusive √-width tube/prefactor) — i.e., §18 OZ machinery itself, not an elementary H_low-gated reduction. This is consistent with, and further specifies, the pre-existing MEMORY finding that "hLogLip = §18 walk-sum content, multi-session, no clean 1-PR entry."
Overreach boundary: B2/B3 MUST NOT be committed as designed (would formalize a false/broken proposition). The tex rc-oz-lemma51-M2-convolution-estimate.tex §sec:bricks/§sec:verdict grading of B2/B3 as "YES" and the H_low framing require correction by lean-math-scribe/dev-docs-sync (not performed here; issue-manager records the fact only). Next step for M2 is re-scoping the non-degenerate core directly onto the genuine §18 OZ body (anisotropic sharp upper bound / true OZ convolution) — this is multi-session from-scratch research with no clean 1-PR entry, requiring further explicit user authorization/scoping, not autonomous continuation.
2026-07-12 GOVERNANCE FINAL — PERMANENTLY BANNED (explicit user directive, supersedes all prior authorization)
User directive (this session, verbatim intent): "現時点で異常だとわかっている内容はもう絶対に触れない" — this entire thread (OZ / Ornstein-Zernike / Simon-Lieb / SL-D₂ / M2 B2-B3 / hLogLip-via-OZ) is PERMANENTLY BANNED, effective immediately, superseding the "SL-D₂ AUTHORIZED" / "M2 IN QUEUE" state recorded above. Do not resume SL-D₂, M2-B2/B3/B4, or any further ingredient in this thread under any future autonomous /goal reissuance — a fresh, explicit, unambiguous user re-authorization naming this thread specifically is required, not implied by general "continue" instructions.
Disposition: this issue stays OPEN (close/reopen is the user's decision, not issue-manager's), but is retired from the active work queue. SL-A/B/C/D₁/M1/M2-B1 remain merged, axiom-free, standing infra (not deleted/reverted) — only further work on this thread's remaining ingredients (SL-D₂, M2-B2/B3/B4, SL-E) is banned.
Replacement route: GJ Thm 17.5.1 everywhere-continuity is now pursued via the §18 cluster-expansion / window-analyticity route, tracked at #4386 (redefined 2026-07-12) — a route independent of everything in this thread. See #4405 item 1a′ and #4259 Next concrete step.
2026-07-12 (cont.): dev-issue-manager governance — PARKED at honest capstone (user directive), both candidate primary sources tested insufficient
Two user-provided candidate primary sources for closing the OZ wall have now been tested and found insufficient:
Aizenman 1982: BLACK (.self-local/reports/research-aizenman1982-oz-feasibility.md, .self-local/tex/aizenman1982-gapcloser-verdict.tex) — zero magnetic field, one-sided/wrong-rate bounds only, m(β) continuity merely cited to Simon, not proved.
CIV03 (Campanino–Ioffe–Velenik 2003): fixed-β sharp OZ asymptotic WHITE (over-delivers), but β-continuity of the mass BLACK (never stated/proved in the paper) and entirely h=0 (BLACK for ∂/∂h) (.self-local/reports/research-civ03-oz-feasibility.md, .self-local/tex/civ03-gapcloser-verdict.tex). Prerequisites (countable-alphabet RPF theory, Kato perturbation, Gibbs-Markov LLT) absent from mathlib/repo; realistic scale 13–23 PR-blocks even before addressing the missing β-continuity extension.
Per explicit user directive ("調査結果を明記の上で区切る"), this thread (#4418) is PARKED, not closed (close/reopen remains the user's decision). SL-A/B/C/D₁/M1/M2-B1 remain merged as standing axiom-free infra (not reverted, not further extended). SL-D₂/M2-B2/B3/B4/SL-E remain banned/parked, not resumed. Reopening requires a new constructive β-analyticity reference or explicit multi-month from-scratch authorization (per #4386/#4405 parking terms), not a general re-issuance of /goal. Full detail: #4386, #4405.
PR Checklist — SL-A to SL-E Lemma 5.1 Ingredient Thread
2026-07-12 GOVERNANCE NOTE (
dev-issue-manager, OFF-BOOK): This entire thread targets GJ's literal "everywhere continuity" closing sentence of Thm 17.5.1, which GJ's own printed proof (pp. 311–312) does not itself establish (Lipschitzm⁻+ Lemma 17.5.2 sandwich only, constantC>1never shown to collapse).docs/index.md:1764–1771labels every OZ Wall-#2 brick produced by this thread "off-book optional", each row stating primary GJ Thm 17.5.1 rigorous content (gj_theorem_17_5_1_rigorous) is already done. No "Ornstein-Zernike"/"Simon-Lieb" theorem exists in the GJ book body (bibliography-only hit). This thread is OFF-BOOK, not an in-scope GJ-book proposition; see #4405 "GOVERNANCE RECONSTRUCTION" and #4259 Next-concrete-step for the STOP-and-ask finding (do not resume M2/B4 without a fresh explicit user authorization decision).Purpose: Track the staged build of Lemma 5.1 (GJ eq. (17.5.1), random-current weight edge-partition factorization) toward the lsc half of Theorem 17.5.1.
Thread: Part of Group 1a (random-current / Simon-Lieb D-family explicit tracking for hLogLip gate relocation).
Status: SL-D₁ COMPLETE (SL-A through SL-D₁b all MERGED, axiom-free); SL-D₂ CORRECTED + SUPERSEDED (2026-07-12,
.self-local/tex/rc-oz-lemma51-SLD2-inequality.tex) — user provided Aizenman 1982 (Commun. Math. Phys. 86, 1-48) PDF at~/junk/0-pdf-for-translation/Aizenman.1982.p48.*.pdfand directed engagement (user's own concrete provisioning act, not agent self-authorization). TRACKING CORRECTION: "Aizenman Lemma 4.1" does NOT exist in the source (verifiedpdftotextfull-text search: zero hits); the subgraph-conditioning content is Aizenman §9, Lemma 9.2 eq.(9.11) p.25 + Lemma 9.3(iii)/(iv) eq.(9.13)-(9.14) pp.25-26 (both Griffiths/GKS-monotonicity, inequality-driven, not an exact switching identity) and §3 Lemma 3.2 p.7 (combinatorial switching identity, used elsewhere in the paper, not for this ingredient). math-before-code re-derivation (rc-oz-lemma51-SLD2-inequality.tex) further found: (a) hLogLip is a pure upper bound (log-derivative = nonnegative excess, already proven by mergedCurrent.hasDerivAt_log_correlation_beta), so SL-D₂ only needs the one-sided inequality version, which closes on existing merged repo infra (correlation_deleteEdges_le= Aizenman Lemma 9.3;correlation_inducedGraph_eq_weightSum_ratiore-instantiated = Aizenman Lemma 9.2) — it is not an irreducible research core; (b) the entire SL-A/B/C/D pivotal-fiber route is in fact bypassable for hLogLip via two already-merged bricks (Current.doubledSourcefree_edgeExcess_eq_truncated4pt+correlation_beta_deriv_le_lebowitz); the genuine remaining research core is the OZ two-point-ratio summability bound(1/⟨σxσy⟩)Σₑ(⟨σxσu⟩⟨σyσv⟩+⟨σxσv⟩⟨σyσu⟩) + |E|/⟨σxσy⟩ ≤ (K/J)·d(x,y)— a convolution/decay estimate, independent of SL-D₂. SL-E gated on this OZ ratio bound, not on SL-D₂.✅ Completed Ingredients
86777335):Current.weight_edge_partition_factor+Current.weight_dominant_edge_factor— axiom-free.a7cb893f):Current.reachableCluster,Current.interiorEdges,Current.weight_cluster_interior_factor,Current.pivotalNumerator_eq_sum_by_cluster— axiom-free.049a7841): cluster-conditioning (GJ p.312) — axiom-free.572c72f6): fiber-indexed source-set partition via interior/exterior decomposition — axiom-free foundational scaffold for Fubini.b4e414f9): nondegeneracy fix via symmetric-difference sources — axiom-free.fc093154): block-source bridge + block-summability (walk-confinement ⊇ = unique moderate step) — axiom-free.a004b977): weight-leveltsumFubiniΣ_C = (βJ)·Ξ_int·Ξ_ext; final SL-D₁ ingredient, completes D1a + D1b whole — axiom-free.cf1909a0): Route-B OZ ratio reduction; reduces hLogLip target to OZ two-point-ratio summability bound; axiom-free via merged infra.✅ SL-A/B/C/D₁/M1 = mainline infra (not wasted work)
SL-A (edge-partition), SL-B (component extraction), SL-C (avoiding-set/bridge-uniqueness), SL-D₁ (range-independence, weight factorization
Σ_C=(βJ)·Ξ_int·Ξ_ext) and M1 (Lebowitz convolution upper bound) are standing, axiom-free, reusable infra for the random-current / OZ route; they are not superseded/deleted, only advanced on the critical path. M1 discharges the false "crude Lebowitz blow-up" diagnosis and reduces hLogLip to the genuine remaining core.⏳ Pending / On-going — TRUE REMAINING CORE = OZ two-point-ratio summability (NOT SL-D₂)
Ξ_ext ≤ ⟨σbσy⟩_Λ·weightSum^{C^c}(∅), which closes on already-merged repo infra (correlation_deleteEdges_le+correlation_inducedGraph_eq_weightSum_ratiore-instantiated) modulo bounded↑Λ-vs-Vsubtype plumbing (SL-D₂(a), moderate, not a research core). SL-D₂ is off the hLogLip critical path (see below) but remains available as an alternative route if needed..self-local/tex/rc-oz-lemma51-SLD2-inequality.tex— sourced against the actual Aizenman 1982 PDF (§9 Lemma 9.2/9.3, not the non-existent "Lemma 4.1"); supersedes the equality-framedrc-oz-lemma51-SLD-collapse.texverdict.Current.exteriorWeightSum_le_correlation_mul_weightSum_empty, bounded subtype/edge-set identification.(1/⟨σxσy⟩)·Σₑ(⟨σxσu⟩⟨σyσv⟩+⟨σxσv⟩⟨σyσu⟩) + |E|/⟨σxσy⟩ ≤ (K/J)·d(x,y)(GJ p.312 OZ content: two-leg decay convolution is
O(d(x,y))uniformly). This is NOT SL-D₂ and NOT the pivotal fiber; it is reached directly from two already-merged bricks (Current.hasDerivAt_log_correlation_beta+correlation_beta_deriv_le_lebowitz).cf1909a0): Route-B Lebowitz convolution upper bound on log-derivative —∂_β log⟨σxσy⟩ ≤ (J/⟨σxσy⟩)·∑_e L_uvxy(OZ ratio reduction, outer-shell brick, axiom-free via merged infra). Discharges false "crude Lebowitz blow-up" diagnosis from earlier design, reduces target to OZ summability. New fileIsingModel/Inequalities/SourcefreeConnectionLebowitzConvolutionBound.lean. M1 does NOT stand alone; M2 (sharp lower-bound two-point decay, multi-session research core) + SL-E capstone required to close.ec186b46): degenerate edges (u or v ∈ {x,y}) contributionS_deg ≤ (deg(x)+deg(y))·J/tanh(βJ)·d(x,y)via existing infra (gks_second+ single-edge tanh bound); axiom-free, hedge is hypothesis (not axiom); does NOT close M2 (B2/B3/B4 remain)..self-local/reports/design-oz-M2-nondegenerate.md, 2026-07-12): off-axis crossed-edge geometric tube sum. The claimedpoly(0)·Dtube bound is FALSE:latticeDistanceis ℓ¹ (non-unique fat geodesics); excess-0 shell alone has∏_i(|Δ_i|+1)points (e.g. d=2 diag:(n+1)²), so∑_a ρ^{d(a,x)+d(a,y)} = ρ^D·∏_i(|Δ_i|+1+c)isO(D^d), notO(D). Do NOT commit as designed.(ρ_+/ρ)^Dfactor; the residual∏_i(|Δ_i|+1+c)is stillO(D^d)(AM-GM), soS_nd ≤ K·Dis unreachable via this route. B3 is not H_low-gated-closable; it depends on the (false) B2 tube bound.⟨σxσy⟩ ≥ c·ρ^{d(x,y)}(rateρ ≥ 2d·tanh(βJ)) uniformly at the summation rate. GJ p.312 / OZ bubble / FFS Ch.12 backbone-tail content; binding-pair pseudo-mass deriv infra structurally incapable. From-scratch multi-session research (3-6 PR, Aizenman §9 / FFS 12 / repo-absent bottleneck).⟨σ_u σ_v⟩ ≥ tanh(βJ)): Unconditional discharge requires gated refactor (private-helper relocation; no inline axiom/sorry); do NOT attempt direct axiomatization. B1 uses hedge as hypothesis (present route, no obstacle).dev-designfor (E1) geometric two-point decay input, (E2) matching lower-leg bound (twoPointFunction_ge_tanh_betaJ_pow_dist, already present), (E3) convolution/summability count — (E3) is the genuine multi-session OZ core (M2 B1–B4 component assembly).Roadmap Note
Scope: Group 1a (Lemma 5.1 SL-A→E) only; no spillover to Group 1b/1c or untracked research. Each ingredient lands axiom-free/Tier-1-clean before next.
Canonical status: #4259 (Current status + Next concrete step); #4405 (Group 1a section).
2026-07-12 CORRECTION (issue-manager governance — B2/B3 design finding,
.self-local/reports/design-oz-M2-nondegenerate.md): Independent design verification of M2's non-degenerate decomposition found the prior "B2/B3 no new hypothesis / YES-graded" checklist entries and the tex.self-local/tex/rc-oz-lemma51-M2-convolution-estimate.tex§sec:verdict grading (B2="YES", B3="YES given H_low") to be WRONG (overclaim), retracted:latticeDistanceis ℓ¹, whose geodesics are non-unique/"fat" (multinomial count); the excess-0 shell alone between x,y has∏_i(|Δ_i|+1)points (e.g. d=2, y=(n,n): (n+1)² points), so the two-focus vertex-convolution generating function∑_a ρ^{d(a,x)+d(a,y)} = ρ^{D}·∏_i(|Δ_i|+1+c)isO(D^d), not the claimedpoly(0)·Dtube bound.(ρ_+/ρ)^Dfactor; the residual∏_i(|Δ_i|+1+c)term is stillO(D^d)(AM-GM), notO(D), soS_nd ≤ K·Dis NOT obtained. B3 is not "H_low-gated axiom-free"; it is unreachable by this route regardless of hypothesis.ρ≥ρ_+=2d·tanh(βJ), ℓ¹ metric): the true on-axis decay rate is~tanh(βJ)(directed-path/SAW dominated), far belowρ_+;H_lowas⟨σxσy⟩ ≥ c₀·ρ_+^{D}is false for large D under the true asymptotics. Thelog(2d)gap between the merged upper rate (2d·tanh, ℓ¹ SAW-entropy overcount) and the merged easy lower rate (tanh) is an artifact of upper-bound looseness (isotropic ℓ¹ overcounting), not a missing matching lower bound; the correct fix direction is a sharper anisotropic/Euclidean-rate upper bound, not H_low.rc-oz-lemma51-M2-convolution-estimate.tex§sec:bricks/§sec:verdict grading of B2/B3 as "YES" and the H_low framing require correction bylean-math-scribe/dev-docs-sync(not performed here; issue-manager records the fact only). Next step for M2 is re-scoping the non-degenerate core directly onto the genuine §18 OZ body (anisotropic sharp upper bound / true OZ convolution) — this is multi-session from-scratch research with no clean 1-PR entry, requiring further explicit user authorization/scoping, not autonomous continuation.2026-07-12 GOVERNANCE FINAL — PERMANENTLY BANNED (explicit user directive, supersedes all prior authorization)
User directive (this session, verbatim intent): "現時点で異常だとわかっている内容はもう絶対に触れない" — this entire thread (OZ / Ornstein-Zernike / Simon-Lieb / SL-D₂ / M2 B2-B3 / hLogLip-via-OZ) is PERMANENTLY BANNED, effective immediately, superseding the "SL-D₂ AUTHORIZED" / "M2 IN QUEUE" state recorded above. Do not resume SL-D₂, M2-B2/B3/B4, or any further ingredient in this thread under any future autonomous
/goalreissuance — a fresh, explicit, unambiguous user re-authorization naming this thread specifically is required, not implied by general "continue" instructions.Disposition: this issue stays OPEN (close/reopen is the user's decision, not issue-manager's), but is retired from the active work queue. SL-A/B/C/D₁/M1/M2-B1 remain merged, axiom-free, standing infra (not deleted/reverted) — only further work on this thread's remaining ingredients (SL-D₂, M2-B2/B3/B4, SL-E) is banned.
Replacement route: GJ Thm 17.5.1 everywhere-continuity is now pursued via the §18 cluster-expansion / window-analyticity route, tracked at #4386 (redefined 2026-07-12) — a route independent of everything in this thread. See #4405 item 1a′ and #4259 Next concrete step.
2026-07-12 (cont.):
dev-issue-managergovernance — PARKED at honest capstone (user directive), both candidate primary sources tested insufficientTwo user-provided candidate primary sources for closing the OZ wall have now been tested and found insufficient:
.self-local/reports/research-aizenman1982-oz-feasibility.md,.self-local/tex/aizenman1982-gapcloser-verdict.tex) — zero magnetic field, one-sided/wrong-rate bounds only,m(β)continuity merely cited to Simon, not proved..self-local/reports/research-civ03-oz-feasibility.md,.self-local/tex/civ03-gapcloser-verdict.tex). Prerequisites (countable-alphabet RPF theory, Kato perturbation, Gibbs-Markov LLT) absent from mathlib/repo; realistic scale 13–23 PR-blocks even before addressing the missing β-continuity extension.Per explicit user directive ("調査結果を明記の上で区切る"), this thread (#4418) is PARKED, not closed (close/reopen remains the user's decision). SL-A/B/C/D₁/M1/M2-B1 remain merged as standing axiom-free infra (not reverted, not further extended). SL-D₂/M2-B2/B3/B4/SL-E remain banned/parked, not resumed. Reopening requires a new constructive β-analyticity reference or explicit multi-month from-scratch authorization (per #4386/#4405 parking terms), not a general re-issuance of
/goal. Full detail: #4386, #4405.