cft-cmi

Separation constraint: all-weak L->R Petz chains have e^{Delta_k} >= 2/eps (sharp)

Status: proved — a complete structured proof.

Area: Lattice, thermal, massive and gapped geometries (O7, O9, O10) · Card type: theorem · Knowledge-base id: corner-separation-constraint

Statement

L->R ordinary-Petz chain (start A_1A_2, adjoin A_{k+1} conditioning on A_k), corners p_2..p_{n-1}, kappa_k = 2 l_{k+1}/(l_k(l_k+l_{k+1})), zeta_k = kappa_k L_{k-1}(T-L_{k-1})/T, Delta_k = y_{k+1}-y_k the modular length of A_k (Delta_n := +infinity). EXACT IDENTITIES (Lem 10.3): zeta_k = sinh(Delta_{k+1}/2)/(sinh(Delta_k/2) sinh((Delta_k+Delta_{k+1})/2)), equivalently 1/zeta_k = sinh^2(Delta_k/2) coth(Delta_{k+1}/2) + (1/2) sinh(Delta_k) -- the corner strengths are functions of the MODULAR LENGTHS alone; consequently e^{Delta_k} <= 1 + 2/zeta_k, with equality IF AND ONLY IF k = n-1 (where Delta_n = infinity and coth = 1) and strict inequality for k <= n-2, the exact gap being 2 sinh^2(Delta_k/2)(coth(Delta_{k+1}/2) - 1); and (e^{Delta_k}-1) zeta_k = 2 r_k(1+v_k)/(1+r_k) >= 2 r_k/(1+r_k) (REF-P6-0 item 6). SEPARATION THEOREM (Thm 11.1): if zeta_j <= eps < 2 for every corner j >= k (only the corners to the RIGHT of p_k are used), then e^{Delta_k} >= 2/eps, and e^{Delta_{n-1}} >= 1 + 2/zeta_{n-1} >= 1 + 2/eps for the last corner. Proof: with gamma_j := coth(Delta_j/2) - 1 = 2/(e^{Delta_j}-1), the identity gives e^{Delta_j} >= 1 + 4/(zeta_j (2 + gamma_{j+1})), hence the recursion gamma_j <= zeta_j(1 + gamma_{j+1}/2); downward induction from gamma_n = 0 gives the fixed point gamma_j <= 2 eps/(2-eps), and substituting back gives e^{Delta_k} >= 1 + (4/eps)/(2 + 2 eps/(2-eps)) = 2/eps. SHARPNESS: only as eps -> 0. REF-P6-3 computed the EXACT constrained minimum of e^{Delta_k} by a closed backward recursion in the modular variables: 6.8134, 20.0499, 66.6817, 200.0050, 666.6682 at eps = 0.3, 0.1, 0.03, 0.01, 0.003, i.e. (eps/2) min = 1.0220, 1.0025, 1.00022, 1.000025, 1.000002 -- the bound is exceeded by 2.2% at eps = 0.3 and is approached only as eps -> 0. REF-P6-0s eps = 0.3 entry 6.75 lies BELOW the exact minimum 6.8134 and is a float-cancellation artifact (a naive search over the lengths destroys T - L_k); it is withdrawn. The hypothesis cannot be weakened to the pair {k,k+1}: with only that pair weak the separation stays O(1) (min e^{Delta} = 8.07 at eps = 0.01, REF-P6-3). GENERAL ADMISSIBLE CASE (Cor 11.2): with s_j in [lambda_j, 2 lambda_j], zeta_j <= eps < 1 for all j >= k gives e^{Delta_k} >= 1/eps.

How to verify

rigor/g1a_separation.py (15 checks, all PASS, output a verbatim capture): the modular identities in 50000 random chains (max rel err 3.5e-10); e^{D_k} <= 1+2/zeta_k with 0 violations, the exact gap formula for k <= n-2, and EXACT equality at k = n-1 in all chains; the separation bound in 400000 random chains (min (eps/2)e^{D_k} = 0.999999996); the recursion and fixed point in 200000 chains; the admissible case; and the exact constrained minimum by backward recursion, reproducing 6.8134, 20.0499, 66.6817, 200.0050, 666.6682. Independently: rigor/ref_p6_3_separation.py (exact rationals, 60000 chains, 0 violations).

Evidence

Related claims

Review

Review record: passed 2026-09-23 by REF-DEP-CFT-B1.

The referee's report and the card's event log stay in the private knowledge base; only the verdict, the date and the referee are published here.

Documentation map · All claims by area · What is open · Symbols · Definitions