StepSevenClampCaps

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

1. The two off-grid constants at the §4.4 pin

theorem Algsuperdiff.Section4.Provider.Regularity.offGridStabilityConst_stepSevenUpper_le (d : ℕ) : ExcessDecay.offGridStabilityConst d (1 / 8) (1 / 32) ≤ 96 * ↑d

The off-grid stability constant at the upper ratio index. 36 d (1/8) / ((1/8 − 1/32)(1 − 1/16)) = 51.2 d ≤ 96 d.

2. The pin's index identities

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCaccS_half_eq : stepSevenCaccS / 2 = 1 / 8

The Caccioppoli's first exponent, halved, is the upper ratio index 1/8.

theorem Algsuperdiff.Section4.Provider.Regularity.stepSevenCgS_half_eq : stepSevenCgS / 2 = 1 / 8

The hlambda slot's index is the upper ratio index: s₀/2 = 1/8.

theorem Algsuperdiff.Section4.Provider.Regularity.stepOneS_div_eight_eq : stepOneS / 8 = 1 / 32

The good-event slot, in numerals.