High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FrozenWitnessGaugeCubeData

Imported from the Apache-2.0 HighContrastHomogenization development at commit 7a13dbcd8d6609264a713373f5c69ceeac870472.

the analytic inputs, parts (a) and (c): the gauge-cube data of the frozen witness's the analytic

inputs listed four "genuinely absent" analytic identifications. This module closes two of them and prepares the third.

• The gauge-cube pullbacks. exists_frozenWitnessGaugeCubePullbacks moves the physical boundary datum g₀ : H1Function U and the gauge solution uHat : H1Function (matImage S⁻¹ U) onto openCubeSet (originCube d j), with literal value and gradient identities. No declaration composes the matrix pullback with the translation for H1Function (only H10Function has one, E15:41); this supplies it, out of exists_h1Function_affinePullback, H1Function.restrict and H1Function.untranslate, exactly the way exists_observationCoeffFamily_and_forcedEquation does internally.

• (a) hBesov and hL2. forceBesov_and_memVectorL2_at_frozenWitness discharges module two regularity premises for the pulled-back boundary gradient, from the hole's own hsNormSq U s₀ g₀.grad ≠ ⊤ and nothing else. These were thought absent; every ingredient is in fact available, and the route is: H1Function.grad_memVectorL2 → Response.memVectorL2_affinePullback → memVectorL2_comp_addRight_of_memVectorL2_translateSet → memVectorL2_constMatrix_mul for the L² leg; hsNormSq_translateSet_add → hsNormSq_matImage_le_opNorm → hsNormSq_matVecMul_ne_top for the fractional leg; then E14's forceBesovRegularity_of_hsNormSq_ne_top, whose only consumer in the repository is this file.

• (c) hFrame. frozenWitnessFrameTransport is the one-line gauge identity that makes FTrans w := S (g₀.grad (S w)) satisfy last premise; hF is then the gradient identity of gObs read backwards.

The gauge carrier of the frozen witness

theorem HCPolySupport.HighContrast.RowSupply.matImage_matSqrtInv_witness_eq_translateSet {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} (hU : U = (fun (y : Vec d) => z + matVecMul (matSqrt (symmPart abar)) y) '' openCubeSet (originCube d j)) : matImage (matSqrt (symmPart abar))⁻¹ U = translateSet (matVecMul (matSqrt (symmPart abar))⁻¹ z) (openCubeSet (originCube d j))

The gauge image of the frozen witness domain is a translate of the origin cube of the witness generation.

theorem HCPolySupport.HighContrast.RowSupply.isOpen_witnessDomain {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} (hU : U = (fun (y : Vec d) => z + matVecMul (matSqrt (symmPart abar)) y) '' openCubeSet (originCube d j)) : IsOpen U

The frozen witness domain is open.

The gauge-cube pullbacks

theorem HCPolySupport.HighContrast.RowSupply.exists_frozenWitnessGaugeCubePullbacks {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} (hU : U = (fun (y : Vec d) => z + matVecMul (matSqrt (symmPart abar)) y) '' openCubeSet (originCube d j)) (g₀ : H1Function U) (uHat : H1Function (matImage (matSqrt (symmPart abar))⁻¹ U)) : ∃ (gObs : H1Function (openCubeSet (originCube d j))) (uObs : H1Function (openCubeSet (originCube d j))), (∀ (y : Vec d), gObs.toFun y = g₀.toFun (matVecMul (matSqrt (symmPart abar)) (y + matVecMul (matSqrt (symmPart abar))⁻¹ z))) ∧ (∀ (y : Vec d), gObs.grad y = matVecMul (matSqrt (symmPart abar)) (g₀.grad (matVecMul (matSqrt (symmPart abar)) (y + matVecMul (matSqrt (symmPart abar))⁻¹ z)))) ∧ (∀ (y : Vec d), uObs.toFun y = uHat.toFun (y + matVecMul (matSqrt (symmPart abar))⁻¹ z)) ∧ ∀ (y : Vec d), uObs.grad y = uHat.grad (y + matVecMul (matSqrt (symmPart abar))⁻¹ z)

The H¹ matrix-and-translation composite at the frozen witness. The physical boundary datum and the gauge solution both land on the origin cube of the witness generation, with literal value and gradient identities.

(c) The frame identity

theorem HCPolySupport.HighContrast.RowSupply.frozenWitnessFrameTransport {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) (g0grad : Vec d → Vec d) (w : Vec d) : matVecMul (matSqrt (symmPart abar)) (g0grad (matVecMul (matSqrt (symmPart abar)) (matVecMul (matSqrt (symmPart abar))⁻¹ w))) = matVecMul (matSqrt (symmPart abar)) (g0grad w)

the hFrame premise, for the canonical choice of FTrans. Gauging back and forth is the identity, so the transported field FTrans w = S (g₀grad (S w)) restricts to S ∘ g₀grad along S⁻¹.

(a) The two regularity premises

theorem HCPolySupport.HighContrast.RowSupply.forceBesov_and_memVectorL2_at_frozenWitness {d : ℕ} [NeZero d] {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {U : Set (Vec d)} {j : ℤ} {z : Vec d} (hU : U = (fun (y : Vec d) => z + matVecMul (matSqrt (symmPart abar)) y) '' openCubeSet (originCube d j)) (hinner : ellipsoid abar (1 / (3 * √↑d)) ⊆ U) {s₀ : ℝ} (hs : 0 < s₀) (hs1 : s₀ < 1) (g₀ : H1Function U) (hHs : hsNormSq U s₀ g₀.grad ≠ ⊤) (G : Vec d → Vec d) (hG : ∀ (y : Vec d), G y = matVecMul (matSqrt (symmPart abar)) (g₀.grad (matVecMul (matSqrt (symmPart abar)) (y + matVecMul (matSqrt (symmPart abar))⁻¹ z)))) : MemVectorL2 (openCubeSet (originCube d j)) G ∧ Book.Ch03.ForceBesovRegularity (originCube d j) s₀ G

the analytic inputs (a), closed. Module the hBesov premise and hL2 for the pulled-back boundary gradient, from the hole's own binders.