OneStepInterior

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

The interior one-step consumers, re-gated at the clause event

Strict additions. Nothing proved is edited: each theorem here is a new _regated sibling of a proved one-step consumer, stating the SAME conclusion from the SAME hypotheses except that the anchor display hharm is read on the frozen good event 𝒢(n-2+3, z; s/8, Cv⁻¹ s⁴) instead of the literal 𝒢(n-2+3, z; s/8, 1/2).

Why the re-gating is free

Every one of these consumers already carries hmem: the sample ω is in the printed good-scale event 𝒢(n-2+3, z; s/8, (s/8)√δ). As soon as that supply threshold sits below the display's threshold — the hypothesis hrep, priced by RebaseEpsilon.excessDecayDelta_repriced at δ ≤ 64 Cv⁻² s⁶ — both indicators collapse to the same value at ω, so a Cv⁻¹ s⁴-gated display and a (1/2)-gated one are interchangeable at that ω (indicator_goodEventAt_transfer). No analysis, no measurability, no constant moves.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.excessDecay_oneStep_interior_of_weaklyHarmonic_regated {d : ℕ} [NeZero d] (hd : d ≠ 0) {m n : ℤ} {k : ℕ} (hk : 3 ≤ k) {M : Section3.ABKModel d} {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) {delta : ℝ} (hdelta1 : delta ≤ 1) {x z : HCPolySupport.Vec d} (hx : x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) (hnm : n - 1 ≤ m) (hcube : (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) {u : HCPolySupport.Vec d → ℝ} (hu : MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (truncatedWindow x m n))) {w : HCPolySupport.H1Function ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2)))} (hw : Support.IsWeaklyHarmonicOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2))) w) {omega : Section3.Cutoff.CutoffSample d} (hmem : omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n - 2 + 3) z ⟨s / 8, ⋯⟩ (s / 8 * √delta)) {B : ENNReal} (hB : B ≠ ⊤) {Cv : ℝ} (hrep : s / 8 * √delta ≤ Cv⁻¹ * s ^ 4) (hharm : (Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n - 2 + 3) z ⟨s / 8, ⋯⟩ (Cv⁻¹ * s ^ 4)).indicator (fun (_omega' : Section3.Cutoff.CutoffSample d) => MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u y - w.toFun y) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => wellPlacedCentre x m (n - 2) + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n - 2))))) omega ≤ B) : Support.affineExcess (truncatedWindow x m (n - ↑k)) u ≤ taylorContractionConst d * Schauder.schauderWindowConst d * windowRatioConst d 2 * (3 ^ (-↑k)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m n) u + triangleRemainderConst d (Schauder.schauderWindowConst d) k * (3 ^ (-n) * (√((3 ^ 2) ^ d) * B.toReal)) + taylorContractionConst d * (3 ^ (n - ↑k)) ^ (1 / 2) * 0

The re-gated sibling of OneStepSchauderComposeInterior.excessDecay_oneStep_interior_of_weaklyHarmonic.

Statement transcribed byte-for-byte from the proved theorem, with the hharm display re-gated at the frozen threshold Cv⁻¹ s⁴ and the reachability hypothesis hrep inserted. The printed supply event 𝒢(n-2+3, z; s/8, (s/8)√δ) sits below both thresholds, so the two indicators agree at the witnessed ω and the re-gating is free.