ReindexSlot

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

The slot ingredients: the caps, the off-grid cap and the σ gap, at n+3

The frozen statement reads the general clause's good-event slot and its flux-corrected error index at n+3 rather than n+2, and carries the binder n + 3 ≤ m rather than n + 2 ≤ m. Everything the proved interior chain reads at the slot therefore has to be re-instantiated one scale up. This module collects the four re-instantiations, all mechanical:

1. the caps — GoodEventCaps.ae_errorRepresentative_le_of_mem_goodEventAt and ae_boundLambdasByEs are m-generic, so the (n+3) slot is a plain re-instantiation, at no cost;
2. the centre-child transport — the chain's own cube is □_{n+2}, which is the centre child of □_{n+3}, i.e. its triadic descendant at depth 1; SlotTransportChildCube's descendant transport then reads the (n+3) caps on □_{n+2} at the explicit factor 3^{(s/8)·1} ≤ 3^{1/8} < 1.15;
3. the off-grid cap at one extra depth — the proved root transport (OffGridErrorFluxCorrected) is generic in the root cube, so the anchor's child window x+□_n is capped against the (n+3) representative at the depth factor 3^{3·(s/8)} = 3^{3s/8} ≤ 3^{3/8} < 1.53 (the proved (n+2) value is 3^{2·(s/8)} = 3^{s/4}, so the re-index costs exactly one more 3^{s/8});
4. the σ gap-3 conversion — Annular.SigmaBarBudget.sigmaBar_ratio_le_four is gap-generic (its hypothesis is n - 2 ≤ m, not n - 2 = m), so σ_{n+3}^{-1} ≤ 4 σ_n^{-1} at the same constant 4 as the proved two-scale conversion; the induction-state binder is discharged internally exactly as in SigmaBarIndex.

References

• ABK26, e.good.set.giveth.v2, e.bound.Lambdas.by.Es.v2; e.mathcalE.stability.applied.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_clause_absorption_constant {CI CS Cfin K : ℝ} (hCI : 0 < CI) (hCfin : 0 ≤ Cfin) (hK : 0 ≤ K) : ∃ (C : ℝ), 0 < C ∧ CI ≤ C ∧ CS ≤ C ∧ K * Cfin ≤ C ∧ 4 * K * Cfin ≤ C

A common threshold for a source clause, the sigma conversion, and absorption.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.inverse_mul_le_of_constant_le {a b x : ℝ} (ha : 0 < a) (hab : a ≤ b) (hx : 0 ≤ x) : b⁻¹ * x ≤ a⁻¹ * x

Decreasing the positive threshold constant relaxes an inverse-scaled bound.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.sigma_leg_move {p q X a b : ℝ} (hp : 0 ≤ p) (hq : 0 ≤ q) (hX : 0 ≤ X) (hratio : a ≤ 4 * b) : p * a * q * X ≤ 4 * (p * b * q * X)

Transport a nonnegative sigma leg across the gap-three ratio.

1. The centre child, and the two geometric consequences

theorem Algsuperdiff.Section4.Provider.ExcessDecay.centreChild_mem_childCubes (d : ℕ) (k : ℤ) : HCPolySupport.originCube d (k - 1) ∈ HCPolySupport.childCubes (HCPolySupport.originCube d k)

The centre child. The centred cube of scale k - 1 is the middle child of the centred cube of scale k.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.centreChild_mem_descendantsAtScale (d : ℕ) (k : ℤ) : HCPolySupport.originCube d (k - 1) ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d k) (k - 1)

The centre child is the depth-1 triadic descendant.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.originCube_add_two_mem_descendantsAtScale (d : ℕ) (n : ℤ) : HCPolySupport.originCube d (n + 2) ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d (n + 3)) (n + 2)

□_{n+2} is the centre child of □_{n+3}: the n+3 re-index's own depth-1 descent.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.cubeSet_originCube_add_two_subset (d : ℕ) (n : ℤ) : HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 2)) ⊆ HCPolySupport.cubeSet (HCPolySupport.originCube d (n + 3))

The half-open realizations nest: □_{n+2} ⊆ □_{n+3}.

2. The caps at the slot n+3

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_errorRepresentative_le_harmonicSlot_addThree (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) (n : ℤ) (z : HCPolySupport.Vec d), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (1 / 2) → ∀ (L : ℤ), n + 3 ≤ L → Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega) ≤ C * (1 / 2)

The caps step at the n+3 slot. GoodEventCaps's m-generic caps read at m := n+3: on the good event 𝒢(n+3, z; s/8, 1/2) and for every L ≥ n+3, the flux-corrected (∞,2) representative at index n+3 is ≤ C/2.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_errorOn_centreChild_le_harmonicSlot (d : ℕ) [NeZero 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) (n : ℤ) (z : HCPolySupport.Vec d), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (1 / 2) → ∀ (L : ℤ), n + 3 ≤ L → ∀ (u : ℝ), s / 8 ≤ u → fluxCorrectedErrorOn M L (n + 3) (HCPolySupport.originCube d (n + 2)) u (Section3.Cutoff.translateCutoffSample z omega) ≤ Real.rpow 3 (1 / 8) * (C * (1 / 2))

The q = 2 cap read on the chain's own cube.

The (n+3) caps, transported to the centre child □_{n+2} by the proved descendant transport: the cost is the explicit depth-1 factor 3^{s/8}, at most 3^{1/8}.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_boundLambdasByEs_centreChild (d : ℕ) [NeZero d] : ∃ (C : ℝ) (K : ℝ), 0 < C ∧ 0 < K ∧ ∀ (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) (n : ℤ) (z : HCPolySupport.Vec d), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ Frozen.Section4.goodEventAt M (Support.cgEllipLowerConstant d) (n + 3) z ⟨s / 8, ⋯⟩ (1 / 2) → ∀ (L : ℤ), n + 3 ≤ L → ∀ (u : ℝ), s / 8 ≤ u → fluxCorrectedEllipticityRatioMaxOn M L (n + 3) (HCPolySupport.originCube d (n + 2)) u (Section3.Cutoff.translateCutoffSample z omega) ≤ K

e.bound.Lambdas.by.Es.v2 at the n+3 slot, read on the chain's own cube.

On the good event 𝒢(n+3, z; s/8, 1/2), for every L ≥ n+3 and every index u ≥ s/8, the coarse-grained ellipticity ratios of the (n+3) flux-corrected field on □_{n+2}, against the comparator σ_{n+3}, are bounded by the constant K = 2d((3^{1/8} C/2)² + 1).

3. The off-grid cap at one extra depth

theorem Algsuperdiff.Section4.Provider.ExcessDecay.ae_offGridChildError_le_representative_harmonicSlot_addThree {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n : ℤ) (z : HCPolySupport.Vec d) {s : ℝ} (hs : 0 < s) (hs1 : s ≤ 1) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (x : HCPolySupport.Vec 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) → offGridErrorFunctional (x - z) (HCPolySupport.originCube d n) (s / 6) (Support.fluxCorrectedRegField M L (n + 3) (HCPolySupport.originCube d (n + 3)) (Section3.Cutoff.translateCutoffSample z omega)).toFun (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (n + 3))) ≤ √(offGridStabilityConst d (s / 6) (s / 8)) * (3 ^ (3 * (s / 8)) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))

The off-grid child error against the (n+3) representative.

The proved root transport is generic in the root cube, so the anchor's own child window x+□_n, read in the parent's z-frame at the translate w = x − z, is bounded by the n+3 slot's own representative fluxCorrectedErrorRepresentative M L (n+3) ⟨s/8⟩, with the depth factor 3^{3s/8} (at most 3^{3/8} < 1.53) — exactly one more 3^{s/8} than the proved (n+2) value 3^{s/4}.

4. The σ gap-3 conversion, binder-free

theorem Algsuperdiff.Section4.Provider.ExcessDecay.inv_sigmaBar_add_three_le_of_inductionState {d : ℕ} (M : Section3.ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) {n : ℤ} (hn : n + 3 ≤ m0) : (↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ ≤ 4 * (↑(Section3.Annealed.sigmaBar M n))⁻¹

σ is almost increasing across a three-scale gap, at the same 4. Annular.SigmaBarBudget.sigmaBar_ratio_le_four asks only n - 2 ≤ m, so the gap is free: σ_{n+3}^{-1} ≤ 4 σ_n^{-1}.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.exists_inv_sigmaBar_add_three_le (d : ℕ) : ∃ (C : ℝ), 0 < C ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → ∀ (n : ℤ), (↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹ ≤ 4 * (↑(Section3.Annealed.sigmaBar M n))⁻¹

The force leg's σ index conversion, binder-free: σ_{n+3}^{-1} ≤ 4 σ_n^{-1} inside the anchor's own regime.