StepSevenClampLambdaAtCentre

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

1. The off-grid transport at the diagonal

theorem Algsuperdiff.Section4.Provider.Regularity.ae_coveringCubeError_le_representative_atCentre {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (L n m : ℤ) (z : HCPolySupport.Vec d) {s t : ℝ} (hs : 0 < s) (hst : s / 8 < t) (ht : t ≤ 1 / 2) : ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), n + 2 ≤ m → z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → HCPolySupport.Book.Ch02.HomogenizationErrorOnCube (HCPolySupport.originCube d (n + 2)) t HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) (ExcessDecay.parentRebasedFamily M L (n + 3) (ExcessDecay.wellPlacedCentre z m (n + 2)) z omega) (Section3.Observable.isotropicComparatorMatrix (Section3.Annealed.sigmaBar M (n + 3))) ≤ √(ExcessDecay.offGridStabilityConst d t (s / 8)) * (3 ^ (s / 8) * Support.fluxCorrectedErrorRepresentative M L (n + 3) ⟨s / 8, ⋯⟩ (Section3.Cutoff.translateCutoffSample z omega))

The covering cube's coarse-graining error against the anchor's representative, at the DIAGONAL. BoundaryCoveringSlot.ae_coveringCubeError_le_representative with the anchor-geometry binder replaced by z ∈ □_m: the half-open containment is ShellWindowEnergyCentre.translateSet_cubeSet_coveringCube_subset_anchorParent_self, and everything else is the parent's script verbatim.

2. The hlambda slot at the diagonal

theorem Algsuperdiff.Section4.Provider.Regularity.ae_stepSevenClampLambdaSlot_atCentre (d : ℕ) [NeZero d] : ∃ (C : ℝ) (K : ℝ), 0 < C ∧ 0 < K ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → ∀ delta ∈ Set.Ioc 0 (1 / 2), 8 * M.gamma ≤ stepOneSEighth → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp delta → ∀ (L m n : ℤ) (z : HCPolySupport.Vec d), ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), omega ∈ stepThreeGoodEvent M delta (n + 3) z → n + 2 ≤ m → n + 3 ≤ L → z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → stepSevenCgLamInv (HCPolySupport.originCube d (n + 2)) (ExcessDecay.parentRebasedFamily M L (n + 3) (ExcessDecay.wellPlacedCentre z m (n + 2)) z omega) stepSevenCgS ≤ K * (↑(Section3.Annealed.sigmaBar M (n + 3)))⁻¹

The seventh coarse slot, produced at the diagonal.

Almost surely, on the §4.4 good event 𝒢(n+3, z; s/8, (s/8)δ^{1/2}) centre z ∈ □_m — interior, boundary or flush — the Step-7 chain's hlambda quantity λ_{1/8,2}^{-1} of the (n+3)-re-based family on the covering cube □_{n+2} at the clamped centre wellPlacedCentre z m (n+2) is capped by one d-only constant against σ_{n+3}^{-1}. This is the print's e.lambda.stability.applied at the covering cube's own scale, in the presentation the well-placed Step-7 chain reads.

3. The countable merge

theorem Algsuperdiff.Section4.Provider.Regularity.ae_stepSevenClampLambdaSlot_merged (d : ℕ) [NeZero d] : ∃ (C : ℝ) (K : ℝ), 0 < C ∧ 0 < K ∧ ∀ (M : Section3.ABKModel d), M.gamma ≤ C⁻¹ * Section3.Disorder.cstar M ^ 10 → ∀ delta ∈ Set.Ioc 0 (1 / 2), 8 * M.gamma ≤ stepOneSEighth → M.gamma * |Real.log M.gamma| ^ 2 ≤ stepOneSEighth.rpow (3 / 2) * Section3.Disorder.cstar M ^ 2 * stepOneEp delta → ∀ᵐ (omega : Section3.Cutoff.CutoffSample d) ∂↑(Section3.Cutoff.cutoffSampleLaw M), ∀ (j nl : ℤ) (v : Fin d → ℤ), omega ∈ stepThreeGoodEvent M delta j (Support.triadicLatticePoint nl v) → ∀ (L m : ℤ), j ≤ L → j - 1 ≤ m → Support.triadicLatticePoint nl v ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → stepSevenCgLamInv (HCPolySupport.originCube d (j - 1)) (ExcessDecay.parentRebasedFamily M L j (ExcessDecay.wellPlacedCentre (Support.triadicLatticePoint nl v) m (j - 1)) (Support.triadicLatticePoint nl v) omega) stepSevenCgS ≤ K * (↑(Section3.Annealed.sigmaBar M j))⁻¹

The seventh slot, merged: one null set for every scale, every printed lattice centre, every truncation and every ambient scale. Mathlib's ae_all_iff through StepSevenAeMerge, over the countable index ℤ × ℤ × (Fin d → ℤ) × ℤ × ℤ. The event scale j reads the per-instance statement at n:= j - 3.