IterationLemmaProvider

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

The provider theorem for the frozen iteration anchor (both conclusions)

What is proved, and out of what

Both conclusions of l.iteration.lemma at the anchor's exact statement, with the explicit C(d) = iterConst d:

• Conclusion (i) (e.iteration.slope.lemma) in the exp product form: the proved deterministic engine IterationLemma.iterationSlopeBound applied to the capped window family, with all six interface slots discharged by the proved producers (hmono from QuasiMonotone.lean, hstab from SlopeStability.lean, hlo/hhi from SlopeStabilityEndpoints.lean, the two side conditions from the sandwich), then the normalizer bridges of IterationLemmaProviderGeometry.lean and the prefactor budget iterPrefactorOne_le.
• Conclusion (ii) (e.excess.decay.lemma) in the corrected shape: the θ-weighted good-run iterate and the decay-carrying run assembly (WeightedGoodRun*.lean) at the error scale Mp = M · Λ · (9 Ci · osc_m + ∑δ), where Λ is the e.combined.bound prefactor of the same engine. The middle slot's single power of M is exactly what the weighted iterate buys; the θ-power prefactor absorbs the division remainder and the crossings, and the leftover M ∑δ proves in the (1+M) ∑δ slot.

The conclusion-side ∀ M binder needs no 0 ≤ M hypothesis: M ≥ ε n ≥ 0 is derived from the anchor's own sign hypothesis at j = n (available because n < m).

Faithfulness

Every hypothesis of iteration_lemma_provider is a hypothesis of the frozen theorem, character for character. Attainment is not needed as a producer at all: the anchor supplies the minimizer family (c j, g j) as a source premise, which is the tex's own ℓ(u, U_j) (the standing frame). The j ≤ m cap is honoured: no window, minimizer, or sign datum is ever read above m, the capped family being constant there.

References

• ABK26, l.iteration.lemma; proof Steps 1--4.

Slot algebra (pure algebra over abstract reals)

The provider theorem

theorem Algsuperdiff.Section4.Provider.ExcessDecay.iteration_lemma_provider (d : ℕ) (hd : d ≠ 0) : ∃ (C : ℝ), 0 < C ∧ ∀ (h : ℕ), ∀ θ ∈ Set.Ioo 0 1, θ ^ h ∈ Set.Ioo 0 (3 / 5) → ∀ (n m : ℤ), n < m → ∀ (U : ℤ → Set (HCPolySupport.Vec d)), (∀ j ≤ m, MeasurableSet (U j)) → (∀ j ≤ m, U (j - 1) ⊆ U j) → (∀ j ≤ m, ∃ (x : HCPolySupport.Vec d) (y : HCPolySupport.Vec d), (fun (v : HCPolySupport.Vec d) => x + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d (j - 2)) ⊆ U j ∧ U j ⊆ (fun (v : HCPolySupport.Vec d) => y + v) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d j)) → ∀ (u : HCPolySupport.Vec d → ℝ), MeasureTheory.MemLp u 2 (MeasureTheory.volume.restrict (U m)) → ∀ B ⊆ Finset.Icc n m, ∀ (ε δ : ℤ → ℝ), (∀ (j : ℤ), n ≤ j → j ≤ m → 0 ≤ ε j) → (∀ (j : ℤ), n ≤ j → j ≤ m → 0 ≤ δ j) → ∀ (c : ℤ → ℝ) (g : ℤ → HCPolySupport.Vec d), (∀ j ≤ m, Support.IsAffineMinimizer (U j) u (c j) (g j)) → (∀ (j : ℤ), n ≤ j → j ≤ m → j ∉ B → Support.affineExcess (U (j - ↑h)) u ≤ θ ^ h * Support.affineExcess (U j) u + ε j * Support.slopeMagnitude (g j) + δ j) → (3 ^ (-n) * Support.normalizedL2On (U n) fun (x : HCPolySupport.Vec d) => u x - HCPolySupport.volumeAverage (U n) u) ≤ Real.exp (C * (↑h + 1) * (↑B.card + 1) + C * ∑ j ∈ Finset.Icc n m, ε j) * ((3 ^ (-m) * Support.normalizedL2On (U m) fun (x : HCPolySupport.Vec d) => u x - HCPolySupport.volumeAverage (U m) u) + ∑ j ∈ Finset.Icc n m, δ j) ∧ ∀ (M : ℝ), (∀ (j : ℤ), n ≤ j → j ≤ m → ε j ≤ M) → Support.affineExcess (U n) u ≤ θ.rpow (-(C * (↑h + 1) * (↑B.card + 1))) * Real.exp (C * (↑h + 1) * (↑B.card + 1) + C * ∑ j ∈ Finset.Icc n m, ε j) * (θ ^ (m - n) * Support.affineExcess (U m) u + M * (3 ^ (-m) * Support.normalizedL2On (U m) fun (x : HCPolySupport.Vec d) => u x - HCPolySupport.volumeAverage (U m) u) + (1 + M) * ∑ j ∈ Finset.Icc n m, δ j)

The provider for Algsuperdiff.Frozen.Section4.iteration_lemma.

The frozen theorem's statement verbatim, at the explicit witness C = iterConst d.