HomSpineSupFormClauseAt

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

The sup-form clause producer with its constant DISPLAYED

Why the constant has to come out of the ∃

HomSpineSupFormClause's single-depth clause production hides its constant √d · CA · C(p,d) inside an existential. That is harmless when CA is model-free, and USELESS when it is not: the frozen budget (K_abs ≤ C_abs·|log γ|) is a QUANTITATIVE statement about the constant, and the Step-3 realization at the fixed exponent p = 4d has CA ≍ |log γ|^{1-1/(4d)}.

This file re-states the same theorem with the C(p,d) factor hoisted OUT of the existential and CA universally quantified INSIDE it, so that the produced constant is the displayed term (ofReal √d · CA · C).toReal and its CA-dependence is visible to the budget.

The proof is unchanged; the ONLY change is the order of the two binders C (hoisted) and CA (pushed in). C(p,d) never depended on CA: it comes from exists_printedCoarseGrainingFiniteP_smoothDual, which is fixed before the cube, the orders, the coefficient field, the forcing and the solutions.

exists_coarseGrainingSupMultiscale_of_depthConverseOn_of_at is the REGRESSION certificate: the statement follows from this one immediately.

1. The producer, with C(p,d) hoisted

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_coarseGrainingSupMultiscale_of_depthConverseOn_at (d : ℕ) (hd : 2 ≤ d) (p : HCPolySupport.FiniteLpExponent) (hp : 2 ≤ p.exponent) : ∃ (C : ENNReal), C ≠ ⊤ ∧ ∀ (CA : ENNReal), CA ≠ ⊤ → ∀ (Pred : ↑HCPolySupport.FractionalOrder → Prop), (∀ (m : ℤ) (j : ℕ) (s : ↑HCPolySupport.FractionalOrder), Pred s → NegativeBesovGridSmoothDualConverseAtDepth (HCPolySupport.originCube d m) s p j CA) → ∀ (m : ℤ) (jn : ℕ), 0 < jn → ∀ (s1 s s2 : ↑HCPolySupport.FractionalOrder), ↑s1 < ↑s → ↑s < ↑s2 → Pred s → ∀ (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (g : HCPolySupport.Vec d → HCPolySupport.Vec d) (u v : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))), HCPolySupport.Book.Ch03.ABK26.MemCubeEuclideanFullWsp (HCPolySupport.originCube d m) s2 p g → HCPolySupport.Book.Ch03.ABK26.IsForcedEquation (HCPolySupport.originCube d m) a u g → HCPolySupport.Book.Ch03.ABK26.IsScalarForcedEquation (HCPolySupport.originCube d m) sigma0 v g → HCPolySupport.Book.Ch03.ABK26.HasH10Difference (HCPolySupport.originCube d m) u v → ∀ (E1 E2 Dg : ℝ) (Gen : HCPolySupport.TriadicCube d → ℝ) (Fgrad Fflux : HCPolySupport.Vec d → HCPolySupport.Vec d), 0 ≤ E1 → 0 ≤ E2 → 0 ≤ Dg → (∀ (R : HCPolySupport.TriadicCube d), 0 ≤ Gen R) → (∀ (R : HCPolySupport.TriadicCube d), printedLocalEnergy a u R ≤ Gen R) → HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityOneScalar (HCPolySupport.originCube d m) ((HCPolySupport.originCube d m).scale - ↑jn) ⋯ a sigma0 hsigma0 s1 ≤ ENNReal.ofReal E1 → HCPolySupport.Book.Ch02.parentTruncatedHomogenizationErrorInfinityTwoScalar (HCPolySupport.originCube d m) ((HCPolySupport.originCube d m).scale - ↑jn) ⋯ a sigma0 hsigma0 (HCPolySupport.fractionalOrderHalf s1) ≤ ENNReal.ofReal E2 → HCPolySupport.Book.Ch03.ABK26.cubeEuclideanPositiveBesovOverlapESeminorm (HCPolySupport.originCube d m) s2 p g ≤ ENNReal.ofReal Dg → Fgrad = (HCPolySupport.Book.Ch03.ABK26.centeredCubeGradientDifferenceL2Field m u v).toField → Fflux = (HCPolySupport.Book.Ch03.ABK26.centeredCubeFluxDifferenceL2Field m a sigma0 u v).toField → CoarseGrainingSupMultiscale (HCPolySupport.originCube d m) jn (ENNReal.ofReal √↑d * CA * C).toReal (↑s) (↑s1) (↑s2) p.exponent.toReal sigma0 E1 E2 Dg Gen Fgrad Fflux

THE SUP-FORM CLAUSE, AT A DISPLAYED CONSTANT.

HomSpineSupFormClause's single-depth clause production with C(p,d) hoisted out of the existential and CA quantified inside: the produced clause constant is the DISPLAYED term (ofReal √d · CA · C).toReal, so a consumer can bound it.