OneStepBoundaryHonestRegated

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

The re-gated sibling of the re-cut boundary one-step

OneStepBoundaryHonest.excessDecay_oneStep_boundary_metSet_datumSplit re-gated at the frozen threshold C_v⁻¹ s⁴, exactly as the re-gated sibling of the proved boundary endpoint re-gates it. This is the shape the anchored join consumes on the boundary branch, so it is the interface an honest join must be built against.

The statement is transcribed byte-for-byte from the re-cut endpoint, with _hharm re-gated and the reachability hypothesis _hrep inserted; the conclusion — including the printed K_h leg — is unchanged. The printed supply event sits below both thresholds, so the re-gating is free (RebaseEpsilon.indicator_goodEventAt_transfer).

theorem Algsuperdiff.Section4.Provider.ExcessDecay.excessDecay_oneStep_boundary_metSet_datumSplit_regated (d : ℕ) [NeZero d] (hd : d ≠ 0) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ {m n : ℤ} {k : ℕ}, 3 ≤ k → ∀ {M : Section3.ABKModel d} {s : ℝ} (hs : 0 < s), s ≤ 1 → ∀ {delta : ℝ}, delta ≤ 1 → ∀ {x z : HCPolySupport.Vec d} {i : Fin d}, x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → n - 1 ≤ m → n - 2 < m → MeetsUpperFace x m (n - 2) i ∨ MeetsLowerFace x m (n - 2) i → ∀ {u v v₁ V : HCPolySupport.Vec d → ℝ} {cl : ℝ} {Al : HCPolySupport.Vec d} {Kh : ℝ}, 0 ≤ Kh → MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (truncatedWindow x m n)) → MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict (truncatedWindow x m n)) → MeasureTheory.MemLp V 2 (MeasureTheory.volume.restrict (reflectedWindow x m (n - 2))) → MeasureTheory.MemLp (fun (y : HCPolySupport.Vec d) => u y - v y) 2 (MeasureTheory.volume.restrict (movedReplacementCube x m n)) → (V =ᵐ[MeasureTheory.volume.restrict (truncatedWindow x m (n - 2))] fun (y : HCPolySupport.Vec d) => v y - affineLift x cl Al y - v₁ y) → (∀ᵐ (y : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (truncatedWindow x m (n - 2)), |v₁ y| ≤ datumResidualBound d n Kh) → (∀ (l : Fin d), MeetsUpperFace x m (n - 2) l → ∀ y ∈ reflectedWindow x m (n - 2), V (HCPolySupport.coordFaceReflection (1 / 2 * 3 ^ m) l y) = -V y) → (∀ (l : Fin d), MeetsLowerFace x m (n - 2) l → ∀ y ∈ reflectedWindow x m (n - 2), V (HCPolySupport.coordFaceReflection (-(1 / 2) * 3 ^ m) l y) = -V y) → InnerProductSpace.HarmonicOnNhd (V ∘ ⇑Schauder.toEuc.symm) (⇑Schauder.toEuc '' reflectedWindow x m (n - 2)) → ∀ {omega : Section3.Cutoff.CutoffSample d}, omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n - 2 + 3) z ⟨s / 8, ⋯⟩ (s / 8 * √delta) → ∀ {B : ENNReal}, B ≠ ⊤ → ∀ {Cv : ℝ}, s / 8 * √delta ≤ Cv⁻¹ * s ^ 4 → (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 - v 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 * C * windowRatioConst d 2 * (3 ^ (-↑k)) ^ (1 / 2) * Support.affineExcess (truncatedWindow x m n) u + triangleRemainderConst d C k * (3 ^ (-n) * (√((3 ^ 2) ^ d) * B.toReal)) + taylorContractionConst d * (3 ^ (n - ↑k)) ^ (1 / 2) * (boundaryDatumLegConst d C k * Kh)

The re-gated sibling of the re-cut boundary one-step.