Geometric per-stage bound for the cubic shell — #2965

[phasetr]

Part of #2965

Summary

Adds derivBoundTight_cubic_shell_le_card_pow (Phase B): for d ≥ 1, ferromagnetic h=0, high temperature (cf = contractionFactor … r₀ < 1), and r,s ∈ box_R (R ≤ k) on no cut edge of the box_k-slice,

derivBoundTight (inducedGraph (latticeGraph d) box_{k+1}) shell … ⟨r,_⟩ ⟨s,_⟩
  ≤ β·J·(shell.card • (2·cf^{(k+1-R)/(r₀+2)})).

How

Each straddle edge of the box_k-slice has a fresh endpoint ∈ box_{k+1}\box_k (straddle_fresh_vertex), whose ℓ¹ distance to r/s is ≥ k+1-R (latticeDistance_ge_of_mem_cubicBox_succ_not_mem), so its decay factor is ≤ cf^{(k+1-R)/(r₀+2)} (cf_pow_fresh_le, via pow_le_pow_of_le_one) and the partner factor ≤ 1. Summing the uniform per-edge bound over the shell (Finset.sum_le_card_nsmul) gives the geometric cf-power times the shell cardinality.

Why

With the shell cardinality polynomial in k and cf < 1, this is the geometric per-stage bound from which the c_n volume-convergence rate follows (combined with the tight per-stage increment #2996). It completes the core Phase B decay aggregation; the remaining step is summing the geometric increments over k.

Verification

• lake build of the new file — green, zero linter warnings.
• lake exe GKSTest — all pass.
• grep sorry — zero.
• docs/index.md + tex/proof-guide.tex synced; proof-guide compiles; no Japanese.

🤖 Generated with Claude Code