SuperposedFluxCoordinateClosed

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

A local finite flux-coordinate superposed result

The lower coarse-ellipticity lane only needs the q-coordinates of the coarse block matrix. This file rebuilds that finite trace reduction directly, without passing through the combined potential-and-flux coordinate theorem. It then proves both local Sobolev trace conditions in the corrected superposed conclusion. The scale-separation and literal wave-envelope gates remain pointwise antecedents on the same cutoff sample.

theorem Algsuperdiff.Section3.Provider.Multiscale.mul_matrixNorm_sigmaStarInvCoarse_le_sum_abs_pureFluxCoordinateQuadratics {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) {sigma : ℝ} (hsigma : 0 < sigma) : sigma * HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a) ≤ ∑ j : Fin d, |HCPolySupport.blockVecDot (0, √sigma • HCPolySupport.basisVec j) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.coarseBlockMatrix U a) (0, √sigma • HCPolySupport.basisVec j))|

The weighted lower coarse-matrix norm is controlled by the finite sum of the pure flux-coordinate quadratic forms of the full coarse block matrix.

theorem Algsuperdiff.Section3.Provider.Multiscale.coarseInverseMatrixNorm_le_superposedFluxBasis_ae {d : ℕ} (hd : 2 ≤ d) (M : ABKModel d) {m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m0 E) (m : ℤ) {b : ℝ} (hb0 : 0 < b) (hb : b ≤ 1 / 8) {k₀ : ℕ} (hk₀ : 3 ≤ k₀) {i : ℤ} (hmi : m - 1 ≤ i) (hi : i ≤ m0) {L : ℤ} (hmL : m ≤ L) {eps : ℝ} (heps : 0 < eps) {t : ℝ} (ht0 : 0 ≤ t) {beta : ℝ} (hbeta0 : 0 < beta) (hbeta9 : 9 * beta ≤ 1) (hbetab : 2 * b + 2 * M.gamma + eps ≤ 2 * beta) (hgammaWin : 4 * (2 * M.gamma + eps) ≤ 1 - beta) {kp : ℕ} (hcap : 9 * 99 ^ d * (Real.exp (-(Percolation.siteRateBase d / 2 * ((↑E)⁻¹ ^ 2 * M.gamma⁻¹))) + 3 ^ (-(↑k₀ / 2))) ≤ Real.exp (-↑kp)) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), (Percolation.hsepSet M m (↑E) b omega).Nonempty → (∀ (n : ℕ), ∀ Q ∈ Whitney.whitneyLayer m (Whitney.whitneyScale M m (↑E) b k₀ omega) n, Stream.cubeSupBound Q Q.scale L ↑omega ≤ whitneyWaveLayerScale M m (Whitney.whitneyScale M m (↑E) b k₀ omega) n L * t) → ↑(Annealed.sigmaBar M i) * HCPolySupport.Book.Ch02.matrixNorm (HCPolySupport.Book.Ch02.sigmaStarInvCoarse (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m)) ((Cutoff.coefficientCutoffTriadicCoeffFamily M L omega).coeffOn (HCPolySupport.originCube d m))) ≤ ∑ j : Fin d, superposedConclusionPayload M m i L (↑E) b eps t beta k₀ kp omega 0 (HCPolySupport.basisVec j)

The finite flux-coordinate superposed conclusion after proving both Sobolev trace conditions for the full bad family. It is simultaneous only over j : Fin d; the separation and literal wave gates are unchanged.