FiniteQAggregateBridge

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

The exact finite-q lower aggregate at the cutoff field

This file keeps the lower coarse-ellipticity observable in its defining weighted ell^(q/2) aggregate. It first lifts lambdaSqFinite_inv_eq_rpow from a Chapter 2 triadic coefficient family to Chapter 4's totalized coefficient-field carrier. It then transports the identity to the Section 3 cutoff observable and moves a nonnegative scalar normalization inside the aggregate.

The bridge deliberately does not apply LambdaGridBridge.tsum_weighted_rpow_root_le. Linearizing the whole aggregate would reintroduce the q > 2 normalizer loss documented in LowerLegProfile.lean.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.lambdaSqCoeffField_inv_eq_rpow {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.RegCoeffField d) {s q : ℝ} (hsq : 0 ≤ s * q) (hq : 0 < q) : (HCPolySupport.Book.Ch04.lambdaSqCoeffField Q s (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) a)⁻¹ = (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s q n * HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale Q (Q.scale - ↑n) a ^ (q / 2)) ^ (2 / q)

Chapter 4's inverse finite-q lower ellipticity is exactly the defining weighted ell^(q/2) aggregate. The non-elliptic branch is included: both sides are zero there.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.cutoffLowerEllipticityInv_mul_eq_rpow {d : ℕ} (M : ABKModel d) (m L : ℤ) {s r : ℝ} (hs : 0 < s) {q : CoarseEllipticityExponent} (hqval : ↑q = HCPolySupport.Book.Ch02.MultiscaleExponent.finite r) (hr : 0 < r) {scaling : ℝ} (hscaling : 0 ≤ scaling) (omega : Cutoff.CutoffSample d) : Observable.cutoffLowerEllipticityInv M m L s hs q omega * scaling = (∑' (n : ℕ), HCPolySupport.Book.Ch02.geometricWeight s r n * (scaling * HCPolySupport.Book.Ch04.maxDescendantSigmaStarInvMatrixNormCoeffFieldAtScale (HCPolySupport.originCube d m) (m - ↑n) (Cutoff.coefficientCutoff M.nu L omega)) ^ (r / 2)) ^ (2 / r)

The exported cutoff lower observable, multiplied by a nonnegative scalar, is the same scalar moved inside every depth of its defining finite-q aggregate. This is the exact carrier needed to split deterministic and random profiles before taking the 2/q root.