HomCGFinalLegs

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

The two duality legs, produced from the display at the lower order

What this file supplies

The last link of the order-loss route: the display, read at the LOWER order s′, produces BOTH WeakNegDualBoundOn legs at the DATA order s.

Input: 3^{-s′m}(σ₀‖∇u-∇v‖ + ‖𝐚∇u-σ₀∇v‖)_{smooth dual at s′} ≤ R, i.e. HomCGDischargeTestClass.smoothDual_legs_of_display applied at s′.

Output, with K = cgTestConst d □_m s s′ p′:

  WeakNegDualBoundOn □_m s (K · σ₀⁻¹ · 3^{s′m} R) (∇u - ∇v)   and
  WeakNegDualBoundOn □_m s (K ·        3^{s′m} R) (𝐚∇u - σ₀∇v).

Since K = d·3^{m(s-s′)}·(1 + C(d,β)^{1/p′}), the produced levels are

  d(1+C)·3^{sm}·σ₀⁻¹·R      and      d(1+C)·3^{sm}·R,

which is EXACTLY the shape of the finite-p coarse-graining hypothesis's two duality clauses, 3^{s·scale}σ⁻¹·RHS and 3^{s·scale}·RHS, with the dimensional factor d(1 + C(d,β)^{1/p′}) absorbed into the printed constant C_cg — which the spine's bundle quantifies existentially. The order loss has vanished from the LEVEL; it survives only inside R, where the printed s^{-1}, s^{-9/2} and (s₂-s)^{-1} are read at s′.

1. The scale weight, moved to the real side

2. The two legs

theorem Algsuperdiff.Section4.Provider.Homogenization.weakNegDualBounds_of_smoothDualDisplay {d : ℕ} {m : ℤ} {a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))} {sigma0 : ℝ} (hsigma0 : 0 < sigma0) {u v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))} (s' s : ↑HCPolySupport.FractionalOrder) (p : HCPolySupport.FiniteLpExponent) (hlo : 0 < (↑s - ↑s') * p.conjugate.exponent.toReal) (hhi : (↑s - ↑s') * p.conjugate.exponent.toReal < ↑d) {R : ENNReal} (hRtop : R ≠ ⊤) (hdisp : ENNReal.ofReal (Real.rpow 3 (-↑s' * ↑m)) * HCPolySupport.Book.Ch03.ABK26.centeredCubeFluxComparisonSmoothDualLHS m a sigma0 u v s' p ≤ R) : WeakNegDualBoundOn (HCPolySupport.originCube d m) (↑s) (cgTestConst d (HCPolySupport.originCube d m) (↑s) (↑s') p.conjugate.exponent.toReal * (sigma0⁻¹ * (Real.rpow 3 (↑s' * ↑m) * R.toReal))) (HCPolySupport.Book.Ch03.ABK26.centeredCubeGradientDifferenceL2Field m u v).toField ∧ WeakNegDualBoundOn (HCPolySupport.originCube d m) (↑s) (cgTestConst d (HCPolySupport.originCube d m) (↑s) (↑s') p.conjugate.exponent.toReal * (Real.rpow 3 (↑s' * ↑m) * R.toReal)) (HCPolySupport.Book.Ch03.ABK26.centeredCubeFluxDifferenceL2Field m a sigma0 u v).toField

BOTH Step-4 duality legs, produced from the display at s′ < s.