SignLowDischarge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
The relaxed σ display, discharged, and the four-slot endpoint #
ABK26, Section 4.1, p.mathcalE.annular.decomp Step 2.
The ugly chain reads the running-diffusivity lower bound at the shifted index
n − 2 but writes it at the exponent 3^{γn}:
½ κ 3^{γn} ≤ σ_{n−2} , κ = √c⋆ γ^{−1/2} .
That is not what the Frozen.Section3.inductionState delivers. The state
gives σ_k² ≥ ¼ max(c⋆ γ^{−1} 3^{2γk}, ν²), hence at k = n − 2
σ_{n−2} ≥ ½ κ 3^{γ(n−2)} = 3^{−2γ} · (½ κ 3^{γn}) ,
short of the printed display by exactly the factor 3^{2γ} — which is at most
3^{1/16} ≈ 1.072 on the printed window 8γ ≤ s ≤ 1/4, and at most 2 under
the standing γ ≤ 1/4 alone.
The chain's hsignlow binder has been relaxed to ¼ throughout
(Ugly → UglyChain → GradNormalization → UglyLatticeChain →
FinalStitch → ClauseOneFinal), at the cost of doubling two output-constant
coefficients and nothing else. This module closes the loop:
sigmaBar_sub_two_lower_quarter_of_inductionState proves the relaxed display
outright from the induction state and the standing γ ≤ 1/4, so that a clause-(i)
endpoint can be run with the hsignlow binder discharged in place rather than
carried. The two private 3^x helpers are re-derived here because their
upstream twins are private.
Part A -- the index-shift cost 3^{2γ} ≤ 2 #
Part B -- the relaxed display, discharged #
The relaxed hsignlow display, proved.
On the Section 3 induction state, at the honest clause-(i) amplitude κ = √c⋆ γ^{−1/2} and at any index with n − 2 ≤ m₀,
¼ κ 3^{γn} ≤ σ_{n−2} .
The printed constant is ½; the gap is the index shift 3^{2γ} ≤ 2, which the
standing γ ≤ 1/4 (ABKModel.shellPrefix.gamma_le_quarter) supplies with no
regime input. This is the exact binder the relaxed ugly chain carries.