RootClauseBWellPlacedHgradChain

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

fine-scale dichotomy geometry

Nothing here imports any of them, nothing here claims an anchor, and nothing here is a frozen statement.

The two items

2. The dichotomy geometry, proved's machine-verified probe: the negation of the flush overhang at scale k IS the gate at scale k (no_overhang_iff_gate), and on the gated side the clamp is inactive (wellPlacedCentre_eq_self_of_gate). These make the split GATE(n') / flush(n') at the selected fine scale —'s corrected reading of option (i).

References

• ABK26, t.regularity Step 7.

1. The dichotomy geometry

theorem Algsuperdiff.Section4.Provider.Regularity.no_overhang_iff_gate {d : ℕ} {m k : ℤ} {z : HCPolySupport.Vec d} : (∀ (i : Fin d) (sigma : ℝ), sigma = 1 ∨ sigma = -1 → ¬ExcessDecay.wellPlacedHalfGap m k < sigma * z i) ↔ (fun (y : HCPolySupport.Vec d) => z + y) '' HCPolySupport.openCubeSet (HCPolySupport.originCube d k) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d m)

The negation of the flush overhang at scale k is exactly the gate at scale k — the fine-scale dichotomy is exhaustive ('s probe, proved).

2. The well-placed coarse chain from an abstract hgrad

theorem Algsuperdiff.Section4.Provider.Regularity.exists_stepSevenEnd_chain_wellPlaced_of_hgrad (d : ℕ) [NeZero d] : ∃ (Cch : ℝ), 0 < Cch ∧ ∀ (M : Section3.ABKModel d) (L : ℤ) {alpha : ℝ} {n m k : ℤ} {gsrc : HCPolySupport.Vec d → HCPolySupport.Vec d} {z : HCPolySupport.Vec d} (uglob hdat : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) (omega : Section3.Cutoff.CutoffSample d) {Cg Ccmp Kd Ks Ctr CB sigma shomNp shomM gradLoc dataG dataM W G H : ℝ}, z ∈ HCPolySupport.openCubeSet (HCPolySupport.originCube d m) → k ≤ m → 0 ≤ Cg → 0 ≤ CB → 0 ≤ Ks → 0 ≤ Ccmp → 0 < sigma → 0 < shomM → 0 ≤ dataG → 0 ≤ W → 0 ≤ G → 0 ≤ H → Support.IsDirichletSolutionOn (Section3.Cutoff.coefficientCutoff M.nu L omega).toCoeffField (HCPolySupport.originCube d m) uglob hdat gsrc → MeasureTheory.MemLp gsrc 2 (Support.normalizedVolumeMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → MeasureTheory.MemLp (HCPolySupport.Gagliardo.gagliardoKernel stepOneS 2 gsrc) 2 (Support.normalizedGagliardoMeasureOn (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))) → stepSevenCgLamInv (HCPolySupport.originCube d k) (ExcessDecay.parentRebasedFamily M L (k + 1) (ExcessDecay.wellPlacedCentre z m k) z omega) stepSevenCgS ≤ CB * sigma⁻¹ → (HCPolySupport.Book.Ch03.scaleNormalizedPositiveBesovVectorSeminormTwo (HCPolySupport.originCube d k) stepSevenCgS fun (x : HCPolySupport.Vec d) => -gsrc (x + ExcessDecay.wellPlacedCentre z m k)) ≤ Kd * dataG → sigma⁻¹ ≤ Ks * shomM⁻¹ → √Ks * rootClauseBTopKg d m k ≤ Ctr * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m) → Ks * Kd ≤ Ctr * Real.rpow 3 (1 / 4 * stepSixExponent alpha n m) → shomNp ≤ Ccmp * shomM → gradLoc ≤ Cg * √shomNp * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * ((HCPolySupport.cubeScaleFactor (HCPolySupport.originCube d k))⁻¹ * Support.normalizedL2On (ExcessDecay.truncatedWindow z m k) fun (x : HCPolySupport.Vec d) => uglob.toFun x - HCPolySupport.volumeAverage (ExcessDecay.truncatedWindow z m k) uglob.toFun) + Cg * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√shomNp * (W * (shomM⁻¹ * G + H)) + dataM) → gradLoc ≤ Cg * √Ccmp * (√(3 ^ d) * stepSevenEmbeddingConst d * stepSevenBridgeConst stepSevenCgS * (Cch * 64 * (√CB + CB)) * Ctr) * Real.rpow 3 (stepSixExponent alpha n m) * (stepSevenNuGradNorm M.nu (HCPolySupport.openCubeSet (HCPolySupport.originCube d m)) uglob.grad + √shomM⁻¹ * dataG) + Cg * Real.rpow 3 (3 / 4 * stepSixExponent alpha n m) * (√Ccmp * (W * ((√shomM)⁻¹ * G + √shomM * H)) + dataM)

The Step-7 coarse chain at the well-placed re-based frame, from hgrad.

StepSevenMean.exists_stepSevenEnd_chain_of_lambda_hmeanFree with every coarse slot discharged at c := wellPlacedCentre z m k on parentRebasedFamily M L (k+1) c z ω, and the fine side abstracted into the parent's own hgrad slot.