LocalizationFluctuationAncestor

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

The ancestor-cube transfer

The cu_m sub-mesh is a fraction 3^{-d(K-m)} of the cu_K mesh, so the boundary-strip bound (LocalizationFluctuationMeshTransfer.cubeFamilyAverage_le_add_sqrt_boundaryFraction) gives nothing here; and a descendant ellipticity display gated by a literal cap 2 gamma (Q.scale - k) <= 16 is violated at Q = originCube d Kc, where 2 gamma (Kc - n) >= 2 * 10^10.

What is proved

• ancestorAtDepth / ancestorAtScale -- the missing geometry. CoarseGraining supplies parentCube (Homogenization/Geometry/TriadicCube.lean) and the child/parent interface of Homogenization/Geometry/TriadicPartition.lean, but no iterated ancestor. ancestorAtDepth R k is parentCube iterated k times, and ancestorAtScale R m is the ancestor at absolute scale m. mem_descendantsAtScale_ancestorAtScale is the descendant relation the ellipticity display consumes.
• gaugedEllipticitySum_descendant_le_of_gap -- the descendant display at a free cap B on the scaled gap 2 gamma (Q.scale - k), in place of a literal 16. The printed constant is the case B = 16, and nothing in the proof depends on the numeral.
• gaugedEllipticitySum_le_ancestorAtScale and doubledPoincareEllipticityFactor_sq_le_ancestorAtScale_gaugedEllipticitySum -- the per-cell transfer: the ellipticity content of the mesoscopic cell R is controlled by the gauged ellipticity sum of R's own scale-m ancestor, at the exponent gamma.
• two_mul_gamma_mul_recurrenceGap_le and its numerical specialization ..._le_twentyTwo -- the gate really holds at the recurrence's own scales. LocalizationParams.recurrenceMesoScale_budget gives m - n <= (6 c_star + 2) gamma^{-1}, hence 2 gamma (m - n) <= 12 c_star + 4, and the proved Provider.Disorder.cstar_le_three_halves caps that at 22.

D against the printed constant

ABK26 quotes m - n <= 8 gamma^{-1}, i.e. 2 gamma (m - n) <= 16, which is the manuscript's c_star <= 1. This is why the display is restated at a free cap B: the constant 3^B is an absolute constant that the annealed Hoelder fold absorbs into its own C, and LocalizationFluctuationSplitFoldArithmetic.exists_gamma_threshold_regime_holder_fold accepts every nonnegative pair of constants. No sharpening of c_star is assumed anywhere below.

Binders

Geometry: hm : R.scale <= m (the ancestor exists). Ellipticity: the exponent window 0 < gamma < s, the gauge positivity 0 < sigmaBar, and the scale gap hgap -- all three are source data. Gate: the shell-width cap h <= 6 c_star gamma^{-1} and the coverage threshold hcover, which cover_of_gamma_le produces from gamma <= 1/1089; the latter is a produced gamma-threshold, the machine-checked form of "a sufficiently large choice of M in e.cgamma.constraints". No smallness, moment, measurability or integrability proposition occurs: everything below is cube combinatorics, deterministic ellipticity arithmetic, or real arithmetic.

Scope

There is no sorry.

References

• ABK26, l.approximate.recurrence.formula Step 2, display; e.ellipticities.monotone.ordered; e.bound.one.cube.by.lambdas; e.recurrence.params; for the 8 gamma^{-1} budget.

The iterated ancestor

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.ancestorAtDepth {d : ℕ} (R : HCPolySupport.TriadicCube d) : ℕ → HCPolySupport.TriadicCube d

The depth-k ancestor of a triadic cube: parentCube iterated k times. CoarseGraining supplies parentCube only.

Equations

• One or more equations did not get rendered due to their size.
• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.ancestorAtDepth R 0 = R

@[simp]

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.ancestorAtDepth_zero {d : ℕ} (R : HCPolySupport.TriadicCube d) : ancestorAtDepth R 0 = R

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.ancestorAtDepth_succ {d : ℕ} (R : HCPolySupport.TriadicCube d) (k : ℕ) : ancestorAtDepth R (k + 1) = ancestorAtDepth (HCPolySupport.parentCube R) k

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.ancestorAtDepth_scale {d : ℕ} (R : HCPolySupport.TriadicCube d) (k : ℕ) : (ancestorAtDepth R k).scale = R.scale + ↑k

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mem_childCubes_parentCube {d : ℕ} (R : HCPolySupport.TriadicCube d) : R ∈ HCPolySupport.childCubes (HCPolySupport.parentCube R)

Every triadic cube is a child of its parent. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mem_descendantsAtDepth_ancestorAtDepth {d : ℕ} (R : HCPolySupport.TriadicCube d) (k : ℕ) : R ∈ HCPolySupport.descendantsAtDepth (ancestorAtDepth R k) k

A cube is a depth-k descendant of its depth-k ancestor. Unconditional.

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.ancestorAtScale {d : ℕ} (R : HCPolySupport.TriadicCube d) (m : ℤ) : HCPolySupport.TriadicCube d

The scale-m ancestor of a triadic cube. For R.scale <= m this is the unique scale-m cube of which R is a descendant; for m < R.scale it is R itself and no statement below refers to that branch.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.ancestorAtScale R m = Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.ancestorAtDepth R (m - R.scale).toNat

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.ancestorAtScale_scale {d : ℕ} (R : HCPolySupport.TriadicCube d) {m : ℤ} (hm : R.scale ≤ m) : (ancestorAtScale R m).scale = m

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mem_descendantsAtScale_ancestorAtScale {d : ℕ} (R : HCPolySupport.TriadicCube d) {m : ℤ} (hm : R.scale ≤ m) : R ∈ HCPolySupport.descendantsAtScale (ancestorAtScale R m) R.scale

The descendant relation the ellipticity display consumes. Unconditional apart from the existence of the ancestor.

The ellipticity display at a free cap on the scale gap

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gaugedEllipticitySum_descendant_le_of_gap {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {gamma s sigmaBar B : ℝ} (hgamma : 0 < gamma) (hgs : gamma < s) (hsig : 0 < sigmaBar) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) (hgap : 2 * gamma * ↑(Q.scale - k) ≤ B) : gaugedEllipticitySum sigmaBar R s a ≤ Real.rpow 3 B * gaugedEllipticitySum sigmaBar Q gamma a

The ellipticity display of Step 2 at a free cap. The manuscript's literal 16 rests on c_star <= 1. Only c_star <= 3/2 is available here, so the cap is carried as a parameter B; the printed statement is the case B = 16 and nothing in the proof depends on the numeral.

The exponent drop s -> gamma is the s-monotonicity half of e.ellipticities.monotone.ordered; the cube step is e.bound.one.cube.by.lambdas; and the descendant weight 3^{2 gamma (Q.scale-k)} is capped by hgap.

The per-cell transfer

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gaugedEllipticitySum_le_ancestorAtScale {d : ℕ} [NeZero d] (R : HCPolySupport.TriadicCube d) {m : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {gamma s sigmaBar B : ℝ} (hgamma : 0 < gamma) (hgs : gamma < s) (hsig : 0 < sigmaBar) (hm : R.scale ≤ m) (hgap : 2 * gamma * ↑(m - R.scale) ≤ B) : gaugedEllipticitySum sigmaBar R s a ≤ Real.rpow 3 B * gaugedEllipticitySum sigmaBar (ancestorAtScale R m) gamma a

The ancestor transfer, at the gauged sum. The gauged ellipticity sum of a mesoscopic cell R at exponent s is controlled by that of R's own scale-m ancestor at exponent gamma, at the cost of 3^B with B any cap on the scaled gap 2 gamma (m - R.scale).

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.doubledPoincareEllipticityFactor_sq_le_ancestorAtScale_gaugedEllipticitySum {d : ℕ} [NeZero d] (R : HCPolySupport.TriadicCube d) {m : ℤ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {gamma s sig0 B : ℝ} (hgamma : 0 < gamma) (hgs : gamma < s) (hsig0 : 0 < sig0) (hm : R.scale ≤ m) (hgap : 2 * gamma * ↑(m - R.scale) ≤ B) : CoarseEllipticity.doubledPoincareEllipticityFactor sig0 R a s * CoarseEllipticity.doubledPoincareEllipticityFactor sig0 R a s ≤ 32 * (HCPolySupport.Book.Ch03.poincareDiscountFactor s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * HCPolySupport.Book.Ch03.poincareDiscountFactor s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2)) * (Real.rpow 3 B * gaugedEllipticitySum sig0 (ancestorAtScale R m) gamma a)

The composed Step-2 ellipticity input. The square of the per-cell Poincare ellipticity factor is bounded by an absolute constant times the gauged ellipticity sum of the cell's own scale-m ancestor at exponent gamma.

This is the shape the annealed Hoelder fold integrates once the stationarity transport has moved the ancestor's moment back to cu_m; that transport is a separate obligation and is not asserted here.

The gate really holds at the recurrence's own scales

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.two_mul_gamma_mul_recurrenceGap_le {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) (hcover : (↑recurrenceGapMultiplier + 1) ^ 2 ≤ M.gamma⁻¹) (hshell : ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹) : 2 * M.gamma * ↑(m - recurrenceMesoScale recurrenceGapMultiplier M.gamma m ↑h) ≤ 12 * Disorder.cstar M + 4

The scaled recurrence gap, in c_star-carrying form. From LocalizationParams.recurrenceMesoScale_budget, m - n <= (6 c_star + 2) gamma^{-1} at the corrected buffer n = m - h - 32 ceil|log_3 gamma|, hence 2 gamma (m - n) <= 12 c_star + 4.

Conditional on the source premise h <= 6 c_star gamma^{-1} and the coverage threshold hcover. gamma <= 1 is derived from the standing ShellLawPrefix.gamma_le_quarter and is not a binder.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.two_mul_gamma_mul_recurrenceGap_le_twentyTwo {d : ℕ} (M : ABKModel d) (m : ℤ) (h : ℕ) (hcover : (↑recurrenceGapMultiplier + 1) ^ 2 ≤ M.gamma⁻¹) (hshell : ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹) : 2 * M.gamma * ↑(m - recurrenceMesoScale recurrenceGapMultiplier M.gamma m ↑h) ≤ 22

The numerical gate of the ancestor transfer. With the proved Provider.Disorder.cstar_le_three_halves the scaled recurrence gap is at most 22.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.doubledPoincareEllipticityFactor_sq_le_recurrenceAncestor {d : ℕ} [NeZero d] (M : ABKModel d) (R : HCPolySupport.TriadicCube d) (m : ℤ) (h : ℕ) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) {s sig0 : ℝ} (hsc : R.scale = recurrenceMesoScale recurrenceGapMultiplier M.gamma m ↑h) (hgs : M.gamma < s) (hsig0 : 0 < sig0) (hcover : (↑recurrenceGapMultiplier + 1) ^ 2 ≤ M.gamma⁻¹) (hshell : ↑h ≤ 6 * Disorder.cstar M * M.gamma⁻¹) : CoarseEllipticity.doubledPoincareEllipticityFactor sig0 R a s * CoarseEllipticity.doubledPoincareEllipticityFactor sig0 R a s ≤ 32 * (HCPolySupport.Book.Ch03.poincareDiscountFactor s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) * HCPolySupport.Book.Ch03.poincareDiscountFactor s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2)) * (Real.rpow 3 22 * gaugedEllipticitySum sig0 (ancestorAtScale R m) M.gamma a)

The per-cell transfer at the recurrence's own carriers. On a mesoscopic cell R of the depth-j family of cu_{Kc} -- i.e. at the buffer scale n = recurrenceMesoScale 32 gamma m h -- the square of the Poincare ellipticity factor is 32 c_{s,2}^2 3^22 times the gauged ellipticity sum of R's own scale-m ancestor at exponent gamma.