Module 7 — The separation constraint

If every corner of a recovery chain is weak, the corners cannot be close together. The bound is e^Δ_k ≥ 2/ε, and the interesting thing about it is that it is never attained: the chain that comes closest still exceeds it, by 2.2% at ε = 0.3 and by two parts in a million at ε = 0.003. The constant 2 is sharp only in the limit.

proved Theorem 11.1 — weak corners must be far apart

For the L→R ordinary-Petz chain and 0 < ε < 2, if ζ_j ≤ ε for every corner j ≥ k — only the corners to the right of p_k are used — then e^Δₖ ≥ 2/ε, and e^Δₙ₋¹ ≥ 1 + 2/ε. The proof is a one-dimensional downward recursion. With γ_j = coth(Δ_j/2) − 1 = 2/(e^Δ_j − 1) the exact corner data of Lemma 10.3 give γ_j ≤ ζ_j(1 + γ_j+1/2), and downward induction from γ_n = 0 reaches the fixed point γ_j ≤ 2ε/(2−ε).

Lemma 10.3 is what makes this possible: the corner strengths are functions of the modular lengths alone, 1/ζₖ = sinh²(Δₖ/2) coth(Δₖ₊₁/2) + (1/2) sinh Δₖ, so e^Δ_k ≤ 1 + 2/ζ_k with equality if and only if k = n−1, where Δ_n = ∞ and the coth is 1.

Where this comes from: claim page · rigor/network_corner_calculus.tex (Thm. 11.1, Lem. 10.3) · rigor/g1a_separation.py · rigor/ref_p6_3_separation.py — referee pass REF-P6-3b, 2026-09-16.

conjectural The second-order network law, and why the separation matters to it

The conjecture is −log F = ∑_j,k ζ_jζ_k G(y_j − y_k) + o(|ζ|²), G = c Ĝ, Ĝ(0) = 1/(12π²). Theorem 11.1 is the part of it that is proved. It is what bounds the off-diagonal terms: all corners weak forces every separation above log(2/ε), so the cross terms are O(ε² sup_{Δ ≥ log(2/ε)} |Ĝ|) and distinct junctions add in ζ².

What is not settled: the law itself, the uniformity of its o(|ζ|²) remainder in the separations (needed wherever ζ → 0 and Δ → ∞ together), and everything about Ĝ away from the origin. Positive-definiteness does not make Ĝ pointwise positive; its sign for Δ > 0 is open.

Where this comes from: claim page · rigor/phase6_brief.md (track W2) · module 6 builds the chains this law is about

What is exact here, and what is measured

The recursion below is a closed form: given the strengths, one square root per corner gives every Δ_j exactly, because Lemma 10.3 turns 1/ζ_j into the quadratic (c+1)E² − (4/ζ_j + 2c)E + (c−1) = 0 in E = e^Δ_j, with c = 1 + γ_j+1. Your browser runs exactly that. The five minima it is checked against were computed by the referee's independent script and are read from its output file, with the line they came from under each number.

The whole theorem in one line: weak corners are pushed apart, and the recursion that proves it starts at the far end of the chain, where Δ_n = ∞. With JavaScript enabled you can set ε, drag each corner strength, and watch the bound bind.

Drag the corner strengths

Each handle is one corner, and the hypothesis is the dashed line: every strength at or below ε. Drag a handle, or focus it and use the arrow keys.

ε, the weakness bound logarithmic slider

Corners at and to the right of p_k only these enter the hypothesis

Saturate every corner the configuration that minimises the separation

The backward recursion, drawn

It runs right to left, from γ_n = 0 at the far end of the chain to the corner the bound is about. The grey line is the fixed point 2ε/(2−ε) that the induction never crosses; the bars are the exact γ_j your strengths produce.

Approached, never attained

The exact constrained minimum of e^Δ_k against the bound 2/ε. The curve is the recursion running in your browser; the dots are the referee's independent computation, read from its output file.

Claims this module carries

claim	status
the separation constraint, Theorem 11.1	proved
the second-order network law	conjectural

The second row is a conjecture: only its separation constraint is proved, and its remainder and its kernel Ĝ are open.