EdAssemblyOneStep

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Monotonicity of the interior one-step remainder slot

The interior one-step contraction carries its remainder as C_r(d,C,k) · 3^{-n} · √((3²)^d) · R, with R the abstract real produced by the harmonic-approximation anchor's B.toReal expansion. Raising R raises the remainder, which is what lets a caller substitute a larger bound for B.toReal in a single add_le_add. That monotonicity is this file.

The K_h leg

The interior branch has no boundary-datum leg: the proved sibling's third summand is C_t (3^{n-k})^{1/2} · 0, collapsed here. That matches the printed lemma, whose two 𝟙_{{(x+□_n)∩∂□_m ≠ ∅}}-gated summands vanish on the interior branch.

References

• ABK26, l.excess.decay.good.scales, statement and proof; l.harmonic.approximation.good.scales.

1. The two abstract-real moves of the one-step conclusion

theorem Algsuperdiff.Section4.Provider.ExcessDecay.oneStepRemainder_mono (d : ℕ) {C : ℝ} (hC : 0 ≤ C) (k : ℕ) (n : ℤ) {R R' : ℝ} (hRR' : R ≤ R') : triangleRemainderConst d C k * (3 ^ (-n) * (√((3 ^ 2) ^ d) * R)) ≤ triangleRemainderConst d C k * (3 ^ (-n) * (√((3 ^ 2) ^ d) * R'))

Monotonicity of the one-step remainder slot. The remainder is C_r(d,C,k) · 3^{-n} · √((3²)^d) · R, increasing in R because triangleRemainderConst is nonnegative.