Coarse-graining support: Support.Deterministic.CoarseCaccioppoli.SingleCubeToRaw.Interior

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

theorem HCPolySupport.coarseCaccioppoli_interior_noteRawEstimate_of_radiusEnergyBridgeInputs_of_radiusAgreement {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hs0 : 0 < s) (hs1 : s < 1) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h G flux u g ξ energy Acirc1 AcircS B) (hctrl : CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl Q a s t C uL2Sq k h G) : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq h F

Interior note-shaped raw estimate from radius-indexed boundary-style energy bridge inputs, transported across the radius agreement used in the centering step.

theorem HCPolySupport.coarseCaccioppoli_interior_noteEstimate_of_radiusEnergyInputs_of_radiusAgreement {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hs0 : 0 < s) (hs1 : s < 1) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h G flux u g ξ energy Acirc1 AcircS B) (hloc : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq k h) : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq h F

Interior note raw estimate from radius-indexed energy bridge inputs and pure coefficient localization, transported across radius agreement.

theorem HCPolySupport.coarseCaccioppoli_interior_noteEstimate_of_radiusEnergyInputs_of_scale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs0 : 0 < s) (hs1 : s < 1) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h G flux u g ξ energy Acirc1 AcircS B) (hscaleLoc : CoarseCaccioppoliBoundarySingleCubeScaleLocalization s t k h) (helliptic : CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization Q a s t) : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq h F

Interior note raw estimate from the primitive scale and ellipticity localization inputs, transported across radius agreement.

theorem HCPolySupport.coarseCaccioppoli_interior_noteEstimate_of_radiusEnergyInputs {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) G flux u g ξ energy Acirc1 AcircS B) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F

Interior note raw estimate from radius-indexed energy bridge inputs using the localized explicit height and standard multiscale ellipticity data, transported across radius agreement.

theorem HCPolySupport.coarseCaccioppoli_interior_explicitHeightPreRecurrence_of_radiusEnergyInputs {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) G flux u g ξ energy Acirc1 AcircS B) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : CoarseCaccioppoliInteriorExplicitHeightPreRecurrence Q a s t C uL2Sq F

Interior explicit-height pre-recurrence from radius-indexed energy bridge inputs using the localized explicit height and standard multiscale ellipticity data, transported across radius agreement.

theorem HCPolySupport.coarseCaccioppoli_interior_noteEstimate_of_multiscaleEllipticity {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B U Xi D A1 AS : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) G flux u g ξ energy Acirc1 AcircS B U Xi D A1 AS) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F

Interior raw note estimate from canonical LambdaSq factor inputs using localized explicit height, radius agreement, and standard multiscale ellipticity data.

theorem HCPolySupport.coarseCaccioppoli_interior_explicitHeightPreRecurrence_of_radiusAgreement {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B U Xi D A1 AS : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeCanonicalFactorInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) G flux u g ξ energy Acirc1 AcircS B U Xi D A1 AS) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : CoarseCaccioppoliInteriorExplicitHeightPreRecurrence Q a s t C uL2Sq F

Interior explicit-height pre-recurrence from canonical LambdaSq factor inputs using localized explicit height, radius agreement, and standard multiscale ellipticity data.

theorem HCPolySupport.coarseCaccioppoli_interior_preRecurrence_of_radiusEnergyBridgeInputs_of_radiusAgreement {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h G flux u g ξ energy Acirc1 AcircS B) (hctrl : CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl Q a s t C uL2Sq k h G) (habs : CoarseCaccioppoliInteriorNoteAbsorptionCondition Q a s t C h) (hcross : CoarseCaccioppoliInteriorNoteCrossTermBound Q a s t C uL2Sq h) : CoarseCaccioppoliInteriorPreRecurrence Q a s t C uL2Sq F

Interior pre-recurrence from the radius-indexed energy bridge inputs after transporting the raw estimate across the centering radius agreement.

theorem HCPolySupport.coarseCaccioppoli_interior_preRecurrence_of_radiusEnergyInputs {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h G flux u g ξ energy Acirc1 AcircS B) (hloc : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq k h) (habs : CoarseCaccioppoliInteriorNoteAbsorptionCondition Q a s t C h) (hcross : CoarseCaccioppoliInteriorNoteCrossTermBound Q a s t C uL2Sq h) : CoarseCaccioppoliInteriorPreRecurrence Q a s t C uL2Sq F

Interior pre-recurrence from radius-indexed energy bridge inputs and pure coefficient localization, transported across radius agreement.

theorem HCPolySupport.coarseCaccioppoli_interior_preRecurrence_of_radiusEnergyInputs_of_scale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k h : ℝ → ℝ → ℝ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq k h G flux u g ξ energy Acirc1 AcircS B) (hscaleLoc : CoarseCaccioppoliBoundarySingleCubeScaleLocalization s t k h) (helliptic : CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization Q a s t) (habs : CoarseCaccioppoliInteriorNoteAbsorptionCondition Q a s t C h) (hcross : CoarseCaccioppoliInteriorNoteCrossTermBound Q a s t C uL2Sq h) : CoarseCaccioppoliInteriorPreRecurrence Q a s t C uL2Sq F

Interior pre-recurrence from the primitive scale and ellipticity localization inputs, transported across radius agreement.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_singleCubeEstimate_of_radiusAgreement {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F G : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hG_bounded : CoarseCaccioppoliRadiusBoundedAbove G) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hsingle : CoarseCaccioppoliBoundarySingleCubeRawEstimate Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) G) (hctrl : CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl Q a s t C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) G) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli from radius-indexed single-cube estimates, explicit-height choice, coefficient-localization controls, and the radius agreement that identifies the centered interior quantity with the boundary-style local quantity.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_radiusEnergyInputs_of_of_radiusAgreement {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hG_bounded : CoarseCaccioppoliRadiusBoundedAbove G) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) G flux u g ξ energy Acirc1 AcircS B) (hctrl : CoarseCaccioppoliBoundarySingleCubeToRawCoefficientControl Q a s t C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) G) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli directly from the radius-indexed energy bridge inputs, explicit-height choice, coefficient-localization controls, and the radius agreement used for centering.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_radiusEnergyInputs_of_radiusAgreement {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hG_bounded : CoarseCaccioppoliRadiusBoundedAbove G) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) G flux u g ξ energy Acirc1 AcircS B) (hloc : CoarseCaccioppoliBoundarySingleCubeCoefficientLocalization Q a s t C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k)) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli from radius-indexed energy bridge inputs and pure coefficient-localization data, transported across the centering radius agreement.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_radiusEnergyInputs_of_scale {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hG_bounded : CoarseCaccioppoliRadiusBoundedAbove G) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) G flux u g ξ energy Acirc1 AcircS B) (hscaleLoc : CoarseCaccioppoliBoundarySingleCubeScaleLocalization s t (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k)) (helliptic : CoarseCaccioppoliBoundarySingleCubeEllipticityLocalization Q a s t) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli from the two primitive localization inputs, after transporting the boundary-style local quantity across radius agreement.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_radiusEnergyInputs_of_of_radiusEnergyInputs {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hG_bounded : CoarseCaccioppoliRadiusBoundedAbove G) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hheight_const : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 4 / s ≤ coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k ρ₁ ρ₂) (hheight_cent : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → 4 / (s + t) ≤ coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) G flux u g ξ energy Acirc1 AcircS B) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli from radius-indexed energy bridge inputs and fully composed localization data, transported across radius agreement.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_radiusEnergyInputs_of_localizedHeight {d : ℕ} [NeZero d] (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {lam Lam : ℝ} (k : ℝ → ℝ → ℕ) {F G : ℝ → ℝ} (flux : ℝ → ℝ → Vec d → Vec d) (u g : ℝ → ℝ → Vec d → ℝ) (ξ : ℝ → ℝ → Vec d → Vec d) (energy : ℝ → ℝ → Vec d → ℝ) (Acirc1 AcircS B : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) (hG_bounded : CoarseCaccioppoliRadiusBoundedAbove G) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hinputs : CoarseCaccioppoliBoundaryRadiusEnergyBridgeInputs Q a s C uL2Sq (fun (ρ₁ ρ₂ : ℝ) => ↑(k ρ₁ ρ₂)) (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) G flux u g ξ energy Acirc1 AcircS B) (hEll : IsEllipticFieldOn lam Lam (openCubeSet Q) a) (hData : ∀ j ≤ Q.scale, ∀ R ∈ descendantsAtScale Q j, ∃ (sigmaR : Mat d) (sigmaStarR : Mat d) (kappaR : Mat d), IsCoarseBlockMatrix (openCubeSet R) a (deterministicCoarseBlockMatrix (openCubeSet R) a) ∧ IsSigmaStarCoarse (openCubeSet R) a sigmaStarR ∧ IsKappaCoarse (openCubeSet R) a sigmaStarR kappaR ∧ IsSigmaCoarse (openCubeSet R) a sigmaR sigmaStarR kappaR ∧ IsUnit (Matrix.det sigmaStarR)) (hBsum_s : Summable fun (n : ℕ) => geometricWeight s 1 n * (maxDescendantBBlockNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) (hSigmaSum_t : Summable fun (n : ℕ) => geometricWeight t 1 n * (maxDescendantSigmaStarInvNormAtScale Q (Q.scale - ↑n) a).rpow (1 / 2)) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli from radius-indexed energy bridge inputs using the localized explicit height and standard multiscale ellipticity data.