HomSpineCloseUnique

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

Theorem B, §4.5, Step 4: the comparator is UNIQUE (∀ v from ∃ v)

The gap this closes

HomSpineFinalStepFour discloses one deviation from the frozen root's shape: the root quantifies ∀ v over comparators solving

  v ∈ H¹(□_m),   -∇·(σ_m ∇v) = ∇·g  in □_m,   v = h  on ∂□_m,

while the Schauder package PRODUCES a comparator, so the conclusion is ∃ v. The two differ by exactly the uniqueness of the Dirichlet comparator, and that is proved here, unconditionally:

1. gradient uniqueness (dirichletComparator_grad_ae_eq) — both equations are tested against the SAME H¹₀(□_m) element w = v₁ - v₂ (produced by HomStepFourIdentity.exists_h10Function_grad_eq_sub from the two zero-trace witnesses at the shared datum h); the two forcing functionals are the same functional of the same g and cancel, leaving σ_m ∫_{□_m} |∇w|² = 0. Since σ_m > 0 and the integrand is nonnegative and integrable (the H¹ membership of both gradients, integrableOn_vecDot_of_memVectorL2), ∇w = 0 a.e.
2. function uniqueness — w ∈ H¹₀(□_m) with vanishing gradient, so the zero-trace Poincaré inequality at the cube's own scale (Schauder.eLpNorm_le_schauderDirichletPoincare, Frozen-free, read at the inscribing cube 0 + □_m) forces ‖w‖_{L²(□_m)} = 0. The L² finiteness that the .toReal step needs is the H¹ structure's own memL2 field, not a new hypothesis.

Both ingredients were already in the repository and nothing analytic is added here: the testing mechanism is HomStepFourIdentity's and the Poincaré inequality is the Schauder cone's eLpNorm_le_schauderDirichletPoincare, used at W = openCubeSet (originCube d m), c = 0, n = m exactly as CubeSchauderTopScale uses it. No fresh analysis was needed and the boundary chain was not required.

The payoff

dirichletComparator_grad_ae_eq and dirichletComparator_energyAverage_eq are what moves the root's two clause bodies from the produced comparator v' to an ARBITRARY comparator v: the (C3) display because v =ᵐ v', the (C4) display because ∇v =ᵐ ∇v' and volumeAverage is an integral. So a producer that delivers the clauses at ∃ v delivers them at ∀ v, which is the root's own quantifier.

1. The H¹₀ difference, at the level of values as well as gradients

theorem Algsuperdiff.Section4.Provider.Homogenization.exists_h10Function_sub_of_hasZeroTrace {d : ℕ} {U : Set (HCPolySupport.Vec d)} {u v h : HCPolySupport.H1Function U} (hu : Support.HasZeroTraceDifferenceOn U u h) (hv : Support.HasZeroTraceDifferenceOn U v h) : ∃ (w : HCPolySupport.H10Function U), (∀ (x : HCPolySupport.Vec d), w.toFun x = u.toFun x - v.toFun x) ∧ ∀ (x : HCPolySupport.Vec d), w.grad x = u.grad x - v.grad x

The H¹₀ difference of two solutions with the same boundary datum, with BOTH pointwise identities. HomStepFourIdentity.exists_h10Function_grad_eq_sub records the gradient half; the value half is what the L² Poincaré step consumes.

2. Gradient uniqueness

theorem Algsuperdiff.Section4.Provider.Homogenization.dirichletComparator_grad_ae_eq {d : ℕ} {Q : HCPolySupport.TriadicCube d} {sigmaBarM : ℝ} (hsig : 0 < sigmaBarM) {v v' h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hv : Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBarM • 1) Q v h g) (hv' : Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBarM • 1) Q v' h g) : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict (HCPolySupport.openCubeSet Q), v.grad x = v'.grad x

The comparator's gradient is unique.

Two solutions of the SAME scalar Dirichlet problem -∇·(σ∇v) = ∇·g, v = h on ∂□_m, have a.e. equal gradients. Both weak equations are tested against their own difference; the forcing terms cancel and the resulting Dirichlet energy of the difference vanishes.

4. ∀ v from ∃ v: the clause transfer

theorem Algsuperdiff.Section4.Provider.Homogenization.dirichletComparator_energyAverage_eq {d : ℕ} {Q : HCPolySupport.TriadicCube d} {sigmaBarM : ℝ} (hsig : 0 < sigmaBarM) {v v' h : HCPolySupport.H1Function (HCPolySupport.openCubeSet Q)} {g : HCPolySupport.Vec d → HCPolySupport.Vec d} (hv : Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBarM • 1) Q v h g) (hv' : Support.IsDirichletSolutionOn (fun (x : HCPolySupport.Vec d) => sigmaBarM • 1) Q v' h g) : (HCPolySupport.volumeAverage (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => sigmaBarM * HCPolySupport.vecNormSq (v.grad y)) = HCPolySupport.volumeAverage (HCPolySupport.openCubeSet Q) fun (y : HCPolySupport.Vec d) => sigmaBarM * HCPolySupport.vecNormSq (v'.grad y)

The comparator's energy average is comparator-independent.

⨍_{□} σ|∇v|² is the same number for every solution of the comparator problem, because volumeAverage is an integral and the gradients agree a.e. This is the (C4) half of the ∀ v-from-∃ v transfer.