Bound cubic-shell derivBoundTight by a spatial-decay sum — #2965

[phasetr]

Part of #2965

Summary

Adds derivBoundTight_inducedGraph_cubic_le_decay_sum (Phase B): in the high-temperature regime contractionFactor d (cubicExhaustion d) p r₀ < 1, for r,s ∈ box_n on no E₀-edge,

derivBoundTight … E₀ … ⟨r,_⟩ ⟨s,_⟩
  ≤ β·J·∑_{⟨a,b⟩∈E₀}[cf^{d(r,a)/(r₀+2)}·cf^{d(s,b)/(r₀+2)} + cf^{d(r,b)/(r₀+2)}·cf^{d(s,a)/(r₀+2)}]

where cf = contractionFactor and d is the ℓ¹ lattice distance.

How

Applies the per-pair spatial decay correlationInfinite_latticeGraph_le_contractionFactor_pow_dist_pair termwise to the diagonal-free infinite-volume bound derivBoundTight_inducedGraph_cubic_le_infiniteVolume_sum (#2996). Distinctness r ≠ a.val etc. follows from r,s being on no E₀-edge (Sym2.mem_iff); products are monotone since correlations and cf-powers are nonnegative.

Why

The cross-product-only (tight) structure guarantees every factor genuinely decays — this is the diagonal-free decay-sum input from which a geometric per-stage rate is extracted. The remaining shell-edge distance/counting aggregation (relating d(r,a) to the stage k and summing over the shell) is the downstream step.

Verification

• lake build of the new file — green, zero linter warnings.
• grep sorry — zero.
• docs/index.md + tex/proof-guide.tex synced; proof-guide compiles (no new errors/undefined); no Japanese.

🤖 Generated with Claude Code