HomSpineSupFormMonotone

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

The sup-form clause: the three transport lemmas of the datum instantiation

What this file supplies

The producer route (HomSpineDepthBandInput → HomSpineSupFormClauseAt) delivers CoarseGrainingSupMultiscale at ITS OWN slots: the produced constant √d·CA·C(p,d), the error order s₁ = s/8, and the pinned representative Fgrad = ∇u − ∇v. The lane's carrier (HomSeamSupClauseCcgFree.RecutCoreSupplyFluxSupClauseAt) asks for the clause at the slot triple (CcgF M, s/4, ∀ G agreeing on the open cube). Three transports close the gap, each in the favorable direction:

• Ccg monotonicity (mono_ccg). The clause constant occurs only inside coarseGrainingFinitePRHS, which is monotone UP in Ccg at the clause's own sign data (HomSeamFluxFreeCcg.coarseGrainingFinitePRHS_mono_ccg); the needed 0 ≤ S is forced by the clause's own energy premise. So the produced clause may be raised to max (recutPinnedCcgFlux d p) (produced M).

• The s₁-slot decoupling (mono_s1). s₁ occurs in the clause ONLY through the weight s − s₁ of coarseGrainingEnergyPartial (verified against the definition: neither negBesovSupPartialNorm nor coarseGrainingFinitePRHS mentions s₁). The energy partial is ANTITONE in its weight (coarseGrainingEnergyPartial_anti_weight: the weights 3^{-(wp)i} decrease in w on nonnegative cell data), and s/8 ≤ s/4 means s − s/8 ≥ s − s/4; hence the clause at s₁ = s/8 IMPLIES the clause at s₁ = s/4: any S dominating the s/4-weighted partials dominates the s/8-weighted ones.

• The Fgrad congruence (congr_grad_of_eqOn). negBesovSupPartialNorm is a Finset.sup' of negBesovLpDepthSeminorm, and the HomSeamGaugeCongruence.negBesovLpDepthSeminorm_congr_of_eqOn makes each depth term blind to the representative on the open cube; Finset.sup'_congr lifts this to the sup, so the clause at the pinned representative serves the carrier's ∀ G slot.

1. The energy partial: nonnegativity and weight antitonicity

theorem Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingEnergyPartial_nonneg {d : ℕ} (Q : HCPolySupport.TriadicCube d) (p w : ℝ) (jn N : ℕ) {Gen : HCPolySupport.TriadicCube d → ℝ} (hGen0 : ∀ (R : HCPolySupport.TriadicCube d), 0 ≤ Gen R) : 0 ≤ coarseGrainingEnergyPartial Q p w jn N Gen

The printed energy partial is nonnegative on nonnegative cell data.

theorem Algsuperdiff.Section4.Provider.Homogenization.coarseGrainingEnergyPartial_anti_weight {d : ℕ} (Q : HCPolySupport.TriadicCube d) {p w w' : ℝ} (hp : 0 ≤ p) (hww' : w ≤ w') (jn N : ℕ) {Gen : HCPolySupport.TriadicCube d → ℝ} (hGen0 : ∀ (R : HCPolySupport.TriadicCube d), 0 ≤ Gen R) : coarseGrainingEnergyPartial Q p w' jn N Gen ≤ coarseGrainingEnergyPartial Q p w jn N Gen

The energy partial is ANTITONE in its weight on nonnegative cell data: the depth weights 3^{-(wp)i} decrease in w.

2. The s₁-slot decoupling

theorem Algsuperdiff.Section4.Provider.Homogenization.CoarseGrainingSupMultiscale.mono_s1 {d : ℕ} {Q : HCPolySupport.TriadicCube d} {jn : ℕ} {Ccg s s1 s1' s2 p sigma E1 E2 Dg : ℝ} {Gen : HCPolySupport.TriadicCube d → ℝ} {Fgrad Fflux : HCPolySupport.Vec d → HCPolySupport.Vec d} (hp : 0 ≤ p) (hGen0 : ∀ (R : HCPolySupport.TriadicCube d), 0 ≤ Gen R) (hs1 : s1 ≤ s1') (h : CoarseGrainingSupMultiscale Q jn Ccg s s1 s2 p sigma E1 E2 Dg Gen Fgrad Fflux) : CoarseGrainingSupMultiscale Q jn Ccg s s1' s2 p sigma E1 E2 Dg Gen Fgrad Fflux

The sup-form clause moves UP in the s₁ slot. s₁ occurs only through the weight s − s₁, and lowering the weight only strengthens the energy premise; the conclusion never sees s₁.

3. The Ccg monotonicity

theorem Algsuperdiff.Section4.Provider.Homogenization.CoarseGrainingSupMultiscale.mono_ccg {d : ℕ} {Q : HCPolySupport.TriadicCube d} {jn : ℕ} {Ccg Ccg' s s1 s2 p sigma E1 E2 Dg : ℝ} {Gen : HCPolySupport.TriadicCube d → ℝ} {Fgrad Fflux : HCPolySupport.Vec d → HCPolySupport.Vec d} (hCcg : Ccg ≤ Ccg') (hs : 0 < s) (hss2 : s < s2) (hE1 : 0 ≤ E1) (hDg : 0 ≤ Dg) (hGen0 : ∀ (R : HCPolySupport.TriadicCube d), 0 ≤ Gen R) (h : CoarseGrainingSupMultiscale Q jn Ccg s s1 s2 p sigma E1 E2 Dg Gen Fgrad Fflux) : CoarseGrainingSupMultiscale Q jn Ccg' s s1 s2 p sigma E1 E2 Dg Gen Fgrad Fflux

The sup-form clause moves UP in the clause constant, at the sign data the lane's slots carry; the needed 0 ≤ S is forced by the clause's own energy premise.

4. The Fgrad congruence

theorem Algsuperdiff.Section4.Provider.Homogenization.negBesovSupPartialNorm_congr_of_eqOn {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s p : ℝ) (N : ℕ) {G G' : HCPolySupport.Vec d → HCPolySupport.Vec d} (hG : ∀ x ∈ HCPolySupport.openCubeSet Q, G x = G' x) : negBesovSupPartialNorm Q s p N G = negBesovSupPartialNorm Q s p N G'

The sup-over-depths partial gauge is blind to the representative on the open cube: the Finset.sup' lift of the depth congruence.

theorem Algsuperdiff.Section4.Provider.Homogenization.CoarseGrainingSupMultiscale.congr_grad_of_eqOn {d : ℕ} {Q : HCPolySupport.TriadicCube d} {jn : ℕ} {Ccg s s1 s2 p sigma E1 E2 Dg : ℝ} {Gen : HCPolySupport.TriadicCube d → ℝ} {G G' Fflux : HCPolySupport.Vec d → HCPolySupport.Vec d} (h : CoarseGrainingSupMultiscale Q jn Ccg s s1 s2 p sigma E1 E2 Dg Gen G Fflux) (hG : ∀ x ∈ HCPolySupport.openCubeSet Q, G x = G' x) : CoarseGrainingSupMultiscale Q jn Ccg s s1 s2 p sigma E1 E2 Dg Gen G' Fflux

The sup-form clause transports along any representative agreeing on the open cube — the shape the carrier's ∀ G slot asks for.