HomCGDischargeInstantiation

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

The spine's own binders feed the printed coarse-graining display

What is established

HomCGDischargeAssembly proves the printed finite-p display at the smooth-dual reading under CoarseGraining's own hypothesis spelling (IsForcedEquation, IsScalarForcedEquation, HasH10Difference). The spine's bundle (SpineDatumCoarseGrainingGauge of HomSpineRepClose) instead carries two IsDirichletSolutionOn binders against a common boundary datum h and a common forcing g:

  hsol: IsDirichletSolutionOn (coefficientCutoff M.nu L ω).toCoeffField □_m u h g
  hcomp: IsDirichletSolutionOn (fun _ => σ_m • 1)                     □_m v h g

This file shows that these two binders ARE the printed pair, with nothing added:

• isForcedEquation_of_dirichletSolutionOn — hsol is -∇·𝐚∇u = ∇·𝐠;
• isScalarForcedEquation_of_dirichletSolutionOn — hcomp is -∇·σ₀∇v = ∇·𝐠 (scalarMatrix σ₀ is by definition σ₀ • 1, so the two spellings are the same function);
• hasH10Difference_of_dirichletPair — the two zero-trace-difference clauses against the SAME h give u - v ∈ H¹₀(□_m), because (u - h) - (v - h) = u - v and H¹₀ is closed under subtraction.

Then exists_printedCoarseGraining_of_dirichletPair restates the display with exactly those binders.

The itemized spine-side feed

For the CoarseGraining display at (m, n, s₁, s, s₂, p, 𝐚, σ₀, 𝐠, u, v) one needs, and only needs:

CoarseGraining hypothesis	spine-side source
2 ≤ d	standing
2 ≤ p.exponent	the bundle's own p (it also carries s + d/p ≤ 1/2)
n < m	the bundle's mesoscale depth jn, at n = m - jn, jn ≥ 1
s₁.1 < s.1 < s₂.1	the s₁ = s/4 pin plus s < s₂
𝐚: CoeffOn (cubeDomain □_m)	coefficientCutoffCoeffOn M L ω □_m
0 < σ₀	hsig: 0 < σ_m
𝐠 ∈ W^{s₂,p}(□_m)	NOT a spine binder — see the residue below
-∇·𝐚∇u = ∇·𝐠	hsol.isDivFormWeakSolutionOn
-∇·σ₀∇v = ∇·𝐠	hcomp.isDivFormWeakSolutionOn
u - v ∈ H¹₀(□_m)	hsol.hasZeroTraceDifferenceOn + hcomp.…

The single item the spine does not supply is the forcing regularity MemCubeEuclideanFullWsp □_m s₂ p 𝐠: the bundle only carries 𝐠's Hölder seminorm hKg. That is the honest residue of the instantiation layer, and it is a hypothesis of the printed proposition itself (𝐠 ∈ W^{s₂,p}(□_m)), not an artifact.

1. The three hypothesis bridges

theorem Algsuperdiff.Section4.Provider.Homogenization.isForcedEquation_of_dirichletSolutionOn {d : ℕ} {Q : HCPolySupport.TriadicCube d} (A : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain Q)) {u h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : Support.IsDirichletSolutionOn A.toCoeffField Q u h g) : HCPolySupport.Book.Ch03.ABK26.IsForcedEquation Q A u g

The spine's Dirichlet binder IS the printed heterogeneous equation.

theorem Algsuperdiff.Section4.Provider.Homogenization.isScalarForcedEquation_of_dirichletSolutionOn {d : ℕ} {Q : HCPolySupport.TriadicCube d} {sigma0 : ℝ} {v h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hv : Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigma0 • 1) Q v h g) : HCPolySupport.Book.Ch03.ABK26.IsScalarForcedEquation Q sigma0 v g

The spine's comparator binder IS the printed scalar equation. No bridging occurs: scalarMatrix σ₀ unfolds to σ₀ • 1, which is the spine's spelling.

theorem Algsuperdiff.Section4.Provider.Homogenization.hasH10Difference_of_dirichletPair {d : ℕ} {Q : HCPolySupport.TriadicCube d} {A B : HCPolySupport.CoeffField d} {u v h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g g' : HCPolySupport.Vec d → HCPolySupport.Vec d} (hu : Support.IsDirichletSolutionOn A Q u h g) (hv : Support.IsDirichletSolutionOn B Q v h g') : HCPolySupport.Book.Ch03.ABK26.HasH10Difference Q u v

Two Dirichlet solutions with a COMMON boundary datum differ by an H¹₀ function. This is the printed u - v ∈ H¹₀(□_m), produced from the spine's two binders and nothing else.

2. The printed display at the spine's binder shape

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_printedCoarseGraining_of_dirichletPair (d : ℕ) (hd : 2 ≤ d) (p : HCPolySupport.FiniteLpExponent) (hp : 2 ≤ p.exponent) : ∃ C < ⊤, ∀ (m n : ℤ) (hnm : n < m) (s1 s s2 : ↑HCPolySupport.FractionalOrder), ↑s1 < ↑s → ↑s < ↑s2 → ∀ (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d m))) (sigma0 : ℝ) (hsigma0 : 0 < sigma0) (g : HCPolySupport.Vec d → HCPolySupport.Vec d), HCPolySupport.Book.Ch03.ABK26.MemCubeEuclideanFullWsp (HCPolySupport.originCube d m) s2 p g → ∀ (u v h : HCPolySupport.H1Function (HCPolySupport.openCubeSet (HCPolySupport.originCube d m))), Support.IsDirichletSolutionOn a.toCoeffField (HCPolySupport.originCube d m) u h g → Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigma0 • 1) (HCPolySupport.originCube d m) v h g → ENNReal.ofReal (Real.rpow 3 (-↑s * ↑m)) * HCPolySupport.Book.Ch03.ABK26.centeredCubeFluxComparisonSmoothDualLHS m a sigma0 u v s p ≤ HCPolySupport.Book.Ch03.ABK26.localCoarseGrainingLpRHS C (HCPolySupport.originCube d m) n ⋯ a sigma0 hsigma0 g u s1 s s2 p

The printed finite-p display, entered at the spine's own binders.

Same conclusion as exists_printedCoarseGrainingFiniteP_smoothDual, but the elliptic pair is presented as the spine presents it: two Dirichlet solutions on □_m against a common boundary datum h and a common forcing 𝐠.