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

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

theorem HCPolySupport.coarseCaccioppoli_nonneg_of_radiusAgreement {F G : ℝ → ℝ} (hagree : CoarseCaccioppoliRadiusAgreement F G) (hG_nonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ G ρ) ⦃ρ : ℝ⦄ : 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ

theorem HCPolySupport.coarseCaccioppoli_radiusBoundedAbove_of_radiusAgreement {F G : ℝ → ℝ} (hagree : CoarseCaccioppoliRadiusAgreement F G) (hbounded : CoarseCaccioppoliRadiusBoundedAbove G) : CoarseCaccioppoliRadiusBoundedAbove F

Agreement of radius quantities also transfers the boundedness hypothesis needed by the deterministic radius iteration.

theorem HCPolySupport.coarseCaccioppoli_boundary_noteRawEstimate_of_radiusAgreement {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F G : ℝ → ℝ} (hagree : CoarseCaccioppoliRadiusAgreement F G) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h G) : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h F

A boundary note-shaped raw estimate for G can be reused for F whenever the two radius quantities agree on the deterministic interval.

theorem HCPolySupport.coarseCaccioppoli_interior_noteRawEstimate_of_boundary_noteEstimate_of_radiusAgreement {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F G : ℝ → ℝ} (hagree : CoarseCaccioppoliRadiusAgreement F G) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h G) : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq h F

The interior middle layer can consume the same local note-shaped estimate as the boundary proof, provided the underlying radius quantity is unchanged by centering.

theorem HCPolySupport.coarseCaccioppoli_interior_preRecurrence_of_boundary_noteEstimate_of_radiusAgreement {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F G : ℝ → ℝ} (hagree : CoarseCaccioppoliRadiusAgreement F G) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h G) (hctrl : CoarseCaccioppoliInteriorNoteCoefficientControl Q a s t C uL2Sq h) : CoarseCaccioppoliInteriorPreRecurrence Q a s t C uL2Sq F

The centered interior proof packages into the same pre-recurrence middle layer once the raw estimate is transported across a radius agreement F = G.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_boundary_noteEstimate_of_of_radiusAgreement {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {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) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq h G) (hheight : CoarseCaccioppoliInteriorHeightChoice Q a s t C h) (hcrossscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∃ (k : ℕ), CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂ ∧ C * Real.rpow 3 (2 * s * h ρ₁ ρ₂) ≤ (C / (s * (1 - s)) * (ThetaRatio Q s t a).rpow (1 / 2)).rpow (coarseCaccioppoliPower s t) * (3 ^ k / 81).rpow (coarseCaccioppoliPower s t)) : F (1 / 3) ≤ coarseCaccioppoliInteriorBound Q a s t C uL2Sq

Interior coarse Caccioppoli from the same note-shaped local estimate as the boundary proof, together with an abstract radius agreement encoding the centering step v := u - (u)_Q.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_boundary_noteEstimate_of_explicitHeight {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 ρ₁ ρ₂) ρ₁ ρ₂) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) G) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli in the completed pre-Besov form: the same boundary-style local estimate as above, transported across the centering agreement F = G, now combines with the note's actual explicit height choice without any extra cross-scale hypothesis.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_boundary_noteEstimate_of_localizedHeight {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 ρ₁ ρ₂) ρ₁ ρ₂) (hraw : CoarseCaccioppoliBoundaryNoteRawEstimate Q a s t C uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) G) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli with the localized explicit height, transported from a boundary-style note estimate across the radius agreement.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_radiusAgreement_of_heightChoice {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 ρ₁ ρ₂) ρ₁ ρ₂) (hraw : ∀ (n : ℕ), G (coarseCaccioppoliRadiusSequence n) ≤ coarseCaccioppoliBoundaryAlphaOfHeight Q a s t C (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) (coarseCaccioppoliRadiusSequence n) (coarseCaccioppoliRadiusSequence (n + 1)) * G (coarseCaccioppoliRadiusSequence (n + 1)) + coarseCaccioppoliBoundaryCrossCoeffOfHeight Q a s C uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) (coarseCaccioppoliRadiusSequence n) (coarseCaccioppoliRadiusSequence (n + 1)) * √(G (coarseCaccioppoliRadiusSequence (n + 1)))) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli with the localized explicit height, transported from a boundary-style note estimate available only on the deterministic Chapter-3 radius sequence.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_noteEstimate_of_explicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hraw : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq (coarseCaccioppoliBoundaryExplicitHeightOfScaleChoice Q a s t C k) F) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli in the same pre-Besov explicit-height form, when the caller already supplies the interior local estimate directly rather than transporting it from the boundary proof.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_noteEstimate_of_localizedExplicitHeightOfScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (k : ℝ → ℝ → ℕ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → CoarseCaccioppoliTriadicGapScaleChoice (k ρ₁ ρ₂) ρ₁ ρ₂) (hraw : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq (coarseCaccioppoliBoundaryLocalizedExplicitHeightOfScaleChoice Q a s t C k) F) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli with the localized explicit height, when the caller supplies the interior note estimate directly.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_radius_recurrence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hrec : CoarseCaccioppoliRadiusRecurrence F (coarseCaccioppoliBoundaryRecursionRhs Q a s t C uL2Sq) (coarseCaccioppoliBeta s t)) : F (1 / 3) ≤ coarseCaccioppoliInteriorBound Q a s t C uL2Sq

Interior coarse Caccioppoli currently reuses the same radius-iteration backbone as the boundary version, provided the caller supplies the interior radius-recursion explicitly.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_preRecurrence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hpre : CoarseCaccioppoliInteriorPreRecurrence Q a s t C uL2Sq F) : F (1 / 3) ≤ coarseCaccioppoliInteriorBound Q a s t C uL2Sq

Interior coarse Caccioppoli from the same already-absorbed pre-recurrence surface as the boundary version.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_explicitHeightPreRecurrence {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hpre : CoarseCaccioppoliInteriorExplicitHeightPreRecurrence Q a s t C uL2Sq F) : F (1 / 3) ≤ coarseCaccioppoliInteriorExplicitHeightBound Q a s t C uL2Sq

Interior coarse Caccioppoli from the explicit-height pre-recurrence middle layer.

theorem HCPolySupport.coarseCaccioppoli_interior_preRecurrence_of_noteEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (hraw : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq h F) (hctrl : CoarseCaccioppoliInteriorNoteCoefficientControl Q a s t C uL2Sq h) : CoarseCaccioppoliInteriorPreRecurrence Q a s t C uL2Sq F

Interior pre-recurrence from the same note-shaped raw estimate and note-shaped coefficient-control surface as the boundary version.

theorem HCPolySupport.coarseCaccioppoli_interior_preRecurrence_of_absorbedCrossTerm {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hraw : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq h F) (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 note-shaped raw estimate plus the two remaining note-specific bookkeeping obligations.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_rawEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) {F : ℝ → ℝ} {α B : ℝ → ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hraw : CoarseCaccioppoliInteriorRawEstimate F α B) (hctrl : CoarseCaccioppoliInteriorCoefficientControl Q a s t C uL2Sq α B) : F (1 / 3) ≤ coarseCaccioppoliInteriorBound Q a s t C uL2Sq

Interior coarse Caccioppoli from the same raw local-estimate plus coefficient-control surface as the boundary version.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_noteEstimate {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hraw : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq h F) (hctrl : CoarseCaccioppoliInteriorNoteCoefficientControl Q a s t C uL2Sq h) : F (1 / 3) ≤ coarseCaccioppoliInteriorBound Q a s t C uL2Sq

Interior coarse Caccioppoli from the same note-shaped raw estimate and note-shaped coefficient-control surface as the boundary version.

theorem HCPolySupport.coarseCaccioppoli_interior_noteCoefficientControl_of_absorptionCondition_of_crossTermBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (habs : CoarseCaccioppoliInteriorNoteAbsorptionCondition Q a s t C h) (hcross : CoarseCaccioppoliInteriorNoteCrossTermBound Q a s t C uL2Sq h) : CoarseCaccioppoliInteriorNoteCoefficientControl Q a s t C uL2Sq h

The split interior note-specific bookkeeping conditions imply the packaged note-shaped coefficient-control surface.

theorem HCPolySupport.coarseCaccioppoli_interior_noteCoefficientControl_of_heightChoice_of_triadicGapScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hheight : CoarseCaccioppoliInteriorHeightChoice Q a s t C h) (hcrossscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∃ (k : ℕ), CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂ ∧ C * Real.rpow 3 (2 * s * h ρ₁ ρ₂) ≤ (C / (s * (1 - s)) * (ThetaRatio Q s t a).rpow (1 / 2)).rpow (coarseCaccioppoliPower s t) * (3 ^ k / 81).rpow (coarseCaccioppoliPower s t)) : CoarseCaccioppoliInteriorNoteCoefficientControl Q a s t C uL2Sq h

The same explicit h-choice bookkeeping and stronger triadic-scale cross estimate also recover the packaged interior coefficient-control surface.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_noteEstimate_of_absorptionCondition_of_crossTermBound {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hraw : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq h F) (habs : CoarseCaccioppoliInteriorNoteAbsorptionCondition Q a s t C h) (hcross : CoarseCaccioppoliInteriorNoteCrossTermBound Q a s t C uL2Sq h) : F (1 / 3) ≤ coarseCaccioppoliInteriorBound Q a s t C uL2Sq

Interior coarse Caccioppoli from the note-shaped raw estimate plus the two remaining note-specific bookkeeping obligations.

theorem HCPolySupport.coarseCaccioppoli_interior_qone_of_noteEstimate_of_heightChoice_of_triadicGapScaleChoice {d : ℕ} (Q : TriadicCube d) (a : CoeffField d) (s t C uL2Sq : ℝ) (h : ℝ → ℝ → ℝ) {F : ℝ → ℝ} (hC : 0 ≤ C) (hs : 0 < s) (ht : 0 < t) (hst : s + t < 1) (hu : 0 ≤ uL2Sq) (hnonneg : ∀ ⦃ρ : ℝ⦄, 1 / 3 ≤ ρ → ρ ≤ 1 → 0 ≤ F ρ) (hbounded : CoarseCaccioppoliRadiusBoundedAbove F) (hraw : CoarseCaccioppoliInteriorNoteRawEstimate Q a s t C uL2Sq h F) (hheight : CoarseCaccioppoliInteriorHeightChoice Q a s t C h) (hcrossscale : ∀ ⦃ρ₁ ρ₂ : ℝ⦄, 1 / 3 ≤ ρ₁ → ρ₁ < ρ₂ → ρ₂ ≤ 1 → ∃ (k : ℕ), CoarseCaccioppoliTriadicGapScaleChoice k ρ₁ ρ₂ ∧ C * Real.rpow 3 (2 * s * h ρ₁ ρ₂) ≤ (C / (s * (1 - s)) * (ThetaRatio Q s t a).rpow (1 / 2)).rpow (coarseCaccioppoliPower s t) * (3 ^ k / 81).rpow (coarseCaccioppoliPower s t)) : F (1 / 3) ≤ coarseCaccioppoliInteriorBound Q a s t C uL2Sq

Interior coarse Caccioppoli from the note-shaped local estimate, the explicit note-facing h choice, and the remaining stronger triadic-scale cross-term inequality.