Coarse-graining support: Support.Sobolev.Foundations.CubeCalderonZygmund.InteriorParentGeometry

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

Stopping comparisons inside the half-radius reflected parent

The reflected parent construction produces its interior weak Hessian on the half-scaled open cube at scale m + 1. The standard stopping cutoff already keeps the comparison-parent radius below half the radius at scale m; this file records that the resulting closed ball, and hence its open axis-cube realization, lies strictly inside that Hessian domain.

theorem HCPolySupport.CubeCalderonZygmund.closedBall_subset_scaledOpenCubeSet_originCube_succ_one_div_two_of_mem {d : ℕ} {m : ℤ} {x : Vec d} {a : ℝ} (hx : x ∈ openCubeSet (originCube d m)) (ha_nonneg : 0 ≤ a) (ha : a ≤ cubeRadius (originCube d m) / 2) : Metric.closedBall x a ⊆ scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)

A closed ball of radius at most half the radius at scale m, centered at a point strictly inside the scale-m cube, lies in the half-scaled open cube at scale m + 1. Strictness at the target boundary comes from the strict source-cube membership, not from the closed-ball radius bound.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonParent_closedBall_subset_scaledOpenCubeSet_originCube_succ_one_div_two {d : ℕ} {m : ℤ} {x : Vec d} {r : ℝ} (depth : ℕ) (hx : x ∈ openCubeSet (originCube d m)) (hr_nonneg : 0 ≤ r) (hcutoff : r ≤ cubeRadius (originCube d m) / (10 * 3 ^ depth)) : Metric.closedBall x (stoppingComparisonParentMultiplier depth * r) ⊆ scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)

Under the standard cutoff, the closed stopping-comparison parent lies in the half-scaled open cube on which the reflected solution's weak Hessian is constructed.

theorem HCPolySupport.CubeCalderonZygmund.stoppingComparisonParent_axisCube_subset_scaledOpenCubeSet_originCube_succ_one_div_two {d : ℕ} {m : ℤ} {x : Vec d} {r : ℝ} (depth : ℕ) (hx : x ∈ openCubeSet (originCube d m)) (hr_pos : 0 < r) (hcutoff : r ≤ cubeRadius (originCube d m) / (10 * 3 ^ depth)) : axisCube (stoppingComparisonParentCorner x r depth) (stoppingComparisonParentSide r depth) ⊆ scaledOpenCubeSet (originCube d (m + 1)) (1 / 2)

Under the standard cutoff, the open axis-cube realization of the stopping comparison parent lies in the half-scaled reflected-parent Hessian domain.