HarmonicProviderFinalInterior

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

The frozen theorem's interior clause, in the frozen theorem's own shape

InteriorComposed.exists_interiorClause_honest is a real inequality between toReal values, at σ_{n+2}^{-1}, under the standing [NeZero d]. The frozen anchor's second (frontier-empty) clause is an ℝ≥0∞ inequality with an indicator on the left, at σ_n^{-1}, and quantifies over a bare (d : ℕ). This module closes that distance:

• the σ index move σ_{n+2}^{-1} ≤ 4 σ_n^{-1}, binder-free inside the anchor's own regime (SigmaBarIndex.exists_inv_sigmaBar_add_two_le);
• the ℝ≥0∞ shell (EnnrealShell): the indicator collapse, the finiteness of the anchor's left-hand side through its own H¹₀ witness, and the ofReal-product regrouping;
• the d = 0 branch: ABKModel d carries 2 ≤ d (ShellLawPrefix.dimension), so the universally quantified statement is vacuous there and [NeZero d] is not part of this export.

The conclusion is the frozen block's second conjunct verbatim: same gate, same indicator, same good event at (n+2, z, s/8, 1/2), same fluxCorrectedErrorRepresentative at the translated sample, same mean-subtracted parent norm, same normalizedGagliardo on the parent-intersected window, same two s-powers -4 and -19/2, same σ_n^{-1} and 3^{(1+s)n}. Nothing is weakened and no exponent is moved.

What is not here (disclosed)

The anchor's first clause (the unconditional general clause, force leg at s^{-7}, both ∇h legs) is not proved here and is not implied by this one: the two clauses are incomparable (s^{-19/2} ≥ s^{-7} on (0,1]), so the provider-final still needs the boundary lane.

References

• ABK26, l.harmonic.approximation.good.scales; the frozen block of Algsuperdiff/Frozen/Section4/HarmonicApproximation.lean.

1. The constant absorption, on abstract reals

2. The interior clause at the frozen theorem's own shape

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_interiorClause_anchorShape (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), ∀ s ∈ Set.Icc (64 * M.gamma) 1, M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → M.gamma * |Real.log M.gamma| ^ 2 ≤ (s / 8).rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * (1 / 2) → ∀ (hs : 0 < s) (L m n : ℤ), m ≤ L → n + 2 ≤ m → ∀ (x z : HCPolySupport.Vec d), x ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → (fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n) ⊆ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 1)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) u h g → MeasureTheory.MemLp g 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 g) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel s 2 h.grad) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → ∀ (v : HCPolySupport.H1Function ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))) (w : HCPolySupport.H10Function ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n))), Support.IsWeaklyHarmonicOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)) v → (∀ (y : HCPolySupport.Vec d), v.toFun y = u.toFun y - w.toFun y) → (∀ (y : HCPolySupport.Vec d), v.grad y = u.grad y - w.grad y) → (fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ frontier (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) = ∅ → (Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 2) z ⟨s / 8, ⋯⟩ (1 / 2)).indicator (fun (_omega' : Section3.Cutoff.CutoffSample d) => MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - v.toFun y) 2 (Support.normalizedVolumeMeasureOn ((fun (y : HCPolySupport.Vec d) => x + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d n)))) omega ≤ ENNReal.ofReal (C * s.rpow (-4) * Support.fluxCorrectedErrorRepresentative M L (n + 2) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega)) * MeasureTheory.eLpNorm (fun (y : HCPolySupport.Vec d) => u.toFun y - HCPolySupport.volumeAverage ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) u.toFun) 2 (Support.normalizedVolumeMeasureOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) + ENNReal.ofReal (C * s.rpow (-(19 / 2)) * (↑(Section3.Annealed.sigmaBar M n))⁻¹ * Real.rpow 3 ((1 + s) * ↑n)) * Support.normalizedGagliardoESeminormOn ((fun (y' : HCPolySupport.Vec d) => z + y') '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (n + 2)) ∩ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) s g

The anchor's second (frontier-empty) clause, verbatim.

Entered at the frozen theorem's own binders and concluded in the frozen theorem's own ℝ≥0∞ carriers, with the anchor's own two s-powers. This is the exact second conjunct of the frozen block, under a provider name and with no standing NeZero hypothesis.