Coarse-graining support: Support.CoarseGraining.OriginCubeEllipticRecovery.Existence

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Origin-cube elliptic recovery -- uniform existence hypothesis

Formulates OpenCubeOriginEllipticRecoveryExistence, carries the long translate- coefficient-field ellipticity helper, and derives origin-cube recovery data from a potentialZeroTraceClosureRealization input under IsEllipticFieldOn.

def HCPolySupport.OpenCubeOriginEllipticRecoveryExistence {d : ℕ} (lam Lam : ℝ) : Prop

Uniform origin-cube recovery existence for elliptic coefficient fields.

This is the remaining upstream existence hypothesis needed to remove the explicit descendant-family burden from the public deterministic coarse Poincare theorems. Once this is available, the descendant family is produced automatically by translation.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.openCubeOriginEllipticRecoveryExistence_of_exists_recoveryData_of_mu_eq_muCandidate {d : ℕ} {lam Lam : ℝ} (hMu : ∀ (n : ℤ) (a : CoeffField d) (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a), ∃ (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))), ∀ (P : BlockVec d), Mu (openCubeSet (originCube d n)) P a = (R.toMuHilbertRealization (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll ⋯)).muCandidate P) : OpenCubeOriginEllipticRecoveryExistence lam Lam

Reduce origin-cube recovery existence to the single hard compatibility field Mu = muCandidate.

After muRecoveryCompatibilityData_of_isEllipticFieldOn_of_mu_eq_muCandidate, the pairing-integrability side of HasOpenCubeEllipticRecoveryData is automatic. So the genuine remaining upstream task is exactly to produce a representative-level recovery package whose Hilbert minimizer value agrees with Mu.

theorem HCPolySupport.openCubeDescendantEllipticRecoveryFamily_of_isEllipticFieldOn_of_originCubeRecoveryExistence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (cubeSet Q) a) (hOrigin : OpenCubeOriginEllipticRecoveryExistence lam Lam) : OpenCubeDescendantEllipticRecoveryFamily Q a

Reduce the descendant recovery-family burden for coarse Poincare to one origin-cube existence theorem.

This is the first cleanup bridge toward removing OpenCubeDescendantEllipticRecoveryFamily from the public cube-level Poincare theorems: once recovery existence is proved on each origin open cube, this theorem automatically produces the descendant family needed downstream.

theorem HCPolySupport.openCubeDescendantEllipticRecoveryFamily_of_ellipticField_openCubeSet {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hOrigin : OpenCubeOriginEllipticRecoveryExistence lam Lam) : OpenCubeDescendantEllipticRecoveryFamily Q a

Open-cube variant of the descendant recovery-family constructor.

This is the a.e.-ellipticity-facing form used downstream in Chapter 5: the law data gives ellipticity on the open target cube almost surely, and every open descendant lies inside that open target cube.

theorem HCPolySupport.exists_recoveryData_of_ellipticField_of_potentialZeroTraceClosureRealization {d : ℕ} (n : ℤ) {lam Lam : ℝ} {a : CoeffField d} (hEll : IsEllipticFieldOn lam Lam (openCubeSet (originCube d n)) a) (hRealize : PotentialSolenoidalL2Data.HasPotentialZeroTraceClosureRealization (openCubeSet (originCube d n))) : ∃ (R : PotentialSolenoidalL2RecoveryData (openCubeSet (originCube d n))), ∀ (P : BlockVec d), Mu (openCubeSet (originCube d n)) P a = (R.toMuHilbertRealization (R.toMuOperatorSystemDataOfIsEllipticFieldOn hEll ⋯)).muCandidate P

On the centered open cube, the canonical closure-based recovery package realizes the Hilbert minimizer value muCandidate, provided we can upgrade closed potential-zero-trace membership to honest zero-trace representatives.

This isolates the remaining upstream Sobolev burden behind the exact closed zero-trace potential realization needed by the recovery construction, rather than the more opaque packaged assumption OpenCubeOriginEllipticRecoveryExistence.

def HCPolySupport.OpenCubePotentialZeroTraceClosureRealization (d : ℕ) : Prop

Origin-cube zero-trace potential closure realization.

This is the remaining Sobolev/closed-range input needed by the origin-cube elliptic recovery theorem: every vector field in the closed zero-trace potential subspace on a centered open cube has an actual H¹₀ potential.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.openCubeOriginEllipticRecoveryExistence_of_potentialZeroTraceClosureRealization {d : ℕ} {lam Lam : ℝ} (hRealize : OpenCubePotentialZeroTraceClosureRealization d) : OpenCubeOriginEllipticRecoveryExistence lam Lam

The packaged origin-cube recovery existence hypothesis follows from the explicit zero-trace potential closure-realization theorem on each centered open cube.

This re-expresses the remaining Chapter 3 cleanup burden in the precise Sobolev language: once the canonical closed zero-trace potential space is known to have actual H¹₀ representatives on origin cubes, the public coarse Poincare theorem surface no longer needs to mention OpenCubeOriginEllipticRecoveryExistence as an independent package.

theorem HCPolySupport.openCubePotentialZeroTraceClosureRealization {d : ℕ} [NeZero d] : OpenCubePotentialZeroTraceClosureRealization d

The origin-cube zero-trace potential closure realization hypothesis is a theorem on every positive dimension, discharged by PotentialSolenoidalL2Data.hasPotentialZeroTraceClosureRealization_of_isOpenBoundedConvexDomain.

theorem HCPolySupport.openCubeOriginEllipticRecoveryExistence {d : ℕ} [NeZero d] {lam Lam : ℝ} : OpenCubeOriginEllipticRecoveryExistence lam Lam

Unconditional origin-cube elliptic recovery existence on every positive dimension.