Build two-box per-stage increment for cubic exhaustion stages — #2965

[phasetr]

Part of #2965

Summary

Builds the two-box per-stage correlation increment correlation_pair_two_box_le_derivBound, the form directly instantiated on cubic exhaustion stages box_k ⊆ box_{k+1} to bound the per-stage difference c_{k+1} − c_k (Issue #2965, Phase A).

For nested finsets T₁ ⊆ T₂, a pair r, s ∈ T₁ (r ≠ s), ferromagnetic at h = 0, with r, s on no cut edge of the T₁-slice:

correlation (inducedGraph G T₂) p {⟨r,_⟩,⟨s,_⟩}
  − correlation (inducedGraph G T₁) p {⟨r,_⟩,⟨s,_⟩}
≤ derivBound (inducedGraph G T₂) (filter straddle) p ⟨r,_⟩ ⟨s,_⟩

Declarations

• nestedFinsetEquiv — the double-subtype relabeling ↥(T₁.subtype (· ∈ T₂)) ≃ ↥T₁.
• correlation_inducedGraph_nested_finset — concrete-layer companion of correlation_inducedGraph_induce_preimage (feat: nested-induce correlation transport (whnf wall bypassed) — #2965 #2991), using the Finset.subtype slice instead of a Set-predicate so it matches the S : Finset ↥T₂ region of the single-box increment directly (avoiding the ↥S vs {x // x.val ∈ T₁} subtype-type mismatch). Same correlation_map_equiv-on-the-direct-graph proof scheme.
• correlation_pair_two_box_le_derivBound — composes the single-box increment correlation_pair_sub_inducedGraph_le_derivBound (feat: numeric per-stage correlation increment (Phase A) — #2965 #2989) on G' = inducedGraph G T₂ with the double-induce identification, recovering inducedGraph G T₁ on the inner box.

Verification

• lake build IsingModel.AmbientLatticeSum.PerStageIncrement — green, zero linter warnings.
• grep sorry — zero.
• docs/index.md + tex/proof-guide.tex synced; proof-guide compiles (no new overfull/undefined); no Japanese.

🤖 Generated with Claude Code