High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.FoldedAnchoredResponseFrame

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

The folded-scale anchored residual frame provider

The formulaic anchored provider produces a physical flux frame at the certificate's own homogenization length, with a frame constant that still carries the homogenized matrix: through the filling coefficient, which is a truncation of a multiple of the absolute gauge scale, and through the frame exponent, which carries the certificate's activation length and hence the witness eccentricity.

This module assembles a parallel provider at the folded length. The original provider is consumed as a black box — it is neither re-proved nor edited — and only two things are re-derived from its exported package: the amplitude rate (HCPoly.Provider.PolynomialHomogenization.Root.Dirichlet.AmplitudeRate) and the arithmetic of the frame exponent (HCPoly.Provider.PolynomialHomogenization.Root.Dirichlet.FrameExponentFold). The result exports a frame constant built from the dimension, the printed orders, the rate, the flux constant, the outer sandwich radius, the normalization radius and the certificate's own amplitude alone, at the folded length x * eccentricityFoldFactor abar pEcc with the law-free exponent pEcc = printRowOrder g * max (responseWindowOrder g) kappaRate / (2 * kappaRate ^ 2).

No hypothesis outside the original provider's binder surface and the frozen normalization data is introduced.

The cross-grid coefficient at a general microscopic parameter

theorem HCPolySupport.HighContrast.RowSupply.crossGrid_gauge_eq {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {lambda : ℝ} (hlambda : 0 < lambda) : (epsilonAffineGrid lambda abar)⁻¹ * Selection.normalizedRoot (symmPart abar) = (lambda * √(specBound (symmPart abar)⁻¹)) • 1

The cross-grid matrix is a scalar. The affine grid at the microscopic parameter lambda and the exact normalized root differ by the scalar lambda * alpha, with alpha the absolute gauge scale of the homogenized matrix. No comparison matrix survives.

The law-free split of the filling coefficient

noncomputable def HCPolySupport.HighContrast.RowSupply.gaugeSplitFillingConstant (d : ℕ) : ℝ

The law-free truncation constant of the observation filling on the residual window.

Equations

• HCPolySupport.HighContrast.RowSupply.gaugeSplitFillingConstant d = max 1 (6 * ↑d * √↑d * (3 * ‖1‖))

theorem HCPolySupport.HighContrast.RowSupply.one_le_gaugeSplitFillingConstant (d : ℕ) : 1 ≤ gaugeSplitFillingConstant d

theorem HCPolySupport.HighContrast.RowSupply.observationFillingCoefficient_le_gaugeSplit {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {lambda : ℝ} (hlambda0 : 0 < lambda) (hlambda3 : lambda ≤ 3) : observationFillingCoefficient d lambda abar ≤ gaugeSplitFillingConstant d * max 1 √(specBound (symmPart abar)⁻¹)

The filling coefficient splits into a law-free constant and a truncated gauge scale. The cross-grid matrix is lambda * alpha times the identity, so the whole law dependence of the filling coefficient is the truncation at one of the absolute gauge scale.

noncomputable def HCPolySupport.HighContrast.RowSupply.foldedResponseFillingConstant (d : ℕ) (g : ℝ) : ℝ

The law-free filling constant of the folded provider, at the response order.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.foldedResponseFillingConstant_nonneg (d : ℕ) (g : ℝ) : 0 ≤ foldedResponseFillingConstant d g

theorem HCPolySupport.HighContrast.RowSupply.sqrt_observationFilling_le_gaugeSplit {d : ℕ} {abar : Mat d} (hS : Matrix.PosDef (symmPart abar)) {lambda g : ℝ} (hlambda0 : 0 < lambda) (hlambda3 : lambda ≤ 3) (hbHalf : responseWindowOrder g ≤ 1 / 2) : √(observationFillingCoefficient d lambda abar * (Book.Ch02.geometricDiscount (1 - 2 * responseWindowOrder g) 1)⁻¹) ≤ foldedResponseFillingConstant d g * max 1 (√(specBound (symmPart abar)⁻¹) ^ (1 / 2))

The response prefactor splits. The parent-anchored response prefactor is below a law-free constant times the truncated square root of the absolute gauge scale — exactly the truncated gauge power that the absorption of HCPoly.Provider.PolynomialHomogenization.Root.Dirichlet.GaugeMaxPowerFluxFrameAbsorption consumes.

The folded provider

noncomputable def HCPolySupport.HighContrast.RowSupply.foldedFrameEccentricityExponent (g kappaRate : ℝ) : ℝ

The law-free exponent of the eccentricity fold that the provider exports.

Equations

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

noncomputable def HCPolySupport.HighContrast.RowSupply.foldedAnchoredResponseConstant (d : ℕ) (g kappaRate delta J : ℝ) : ℝ

The law-free response constant of the folded provider.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.frameFoldConstant_nonneg (d : ℕ) (g kappaRate J : ℝ) : 0 ≤ frameFoldConstant d g kappaRate J

theorem HCPolySupport.HighContrast.RowSupply.foldedAnchoredResponseConstant_nonneg (d : ℕ) (g kappaRate delta J : ℝ) : 0 ≤ foldedAnchoredResponseConstant d g kappaRate delta J

theorem HCPolySupport.HighContrast.RowSupply.RowRetainingPrintOrderGoodScale.exists_foldedAnchoredResidualFrameResponseRate {d : ℕ} [NeZero d] {g c kappaRate : ℝ} {abar : Mat d} {a : CoeffSpace d} {x epsilon : ℝ} (h : RowRetainingPrintOrderGoodScale d g c kappaRate abar a x) (hS : Matrix.PosDef (symmPart abar)) (hg : g ∈ Set.Ico 0 1) (hkappa : 0 < kappaRate) (hx : 1 ≤ x) (hepsilon : 0 < epsilon) (hscale : x ≤ epsilon⁻¹) {U : Set (Vec d)} {rho Rad r Cflux : ℝ} (system : EnlargedMarginRuledTriadicWhitneySystem U rho Rad) (hU : IsOpenBoundedConvexDomain U) (hRad : 0 < Rad) (hGauge : U ⊆ {z : Vec d | vecNormSq z ≤ specBound (symmPart abar)⁻¹}) (hresponseOrder : responseWindowOrder g < r) (hrateOrder : kappaRate ≤ r) (hCflux : 0 ≤ Cflux) (aObs : system.CellIndex → Book.Ch03.CoeffFamily d) (hObs : ∀ (i : system.CellIndex), ((aObs i).coeffOn (ruledObservationCube system i)).toCoeffField =ᵐ[volumeMeasureOn (openCubeSet (ruledObservationCube system i))] fun (y : Vec d) => affineCoefficient (matSqrt (symmPart abar)) ⋯ (fun (z : Vec d) => scaledCoeff epsilon a z - skewPart abar) (y + ruledObservationCenter system i)) {Uphys : Set (Vec d)} {cnorm : ℝ} (hcnorm : 0 < cnorm) (hInner : ellipsoid abar cnorm ⊆ Uphys) (hSandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ Uphys) rho Rad) : ∃ (J : ℕ) (responseBound : system.CellIndex → ℝ), 2 * Rad ≤ 3 ^ ↑J ∧ 3 ^ ↑J ≤ 1 + 3 * (2 * Rad) ∧ (∀ (i : system.CellIndex), Book.Ch02.HomogenizationErrorOnCube (ruledObservationCube system i) (responseWindowOrder g) Book.Ch02.MultiscaleExponent.infinity (Book.Ch02.MultiscaleExponent.finite 2) (aObs i) (identityConstantCoeffMatrix d).matrix ≤ responseBound i) ∧ PhysicalFluxEpsilonFrameBound system (responseWindowOrder g) r Cflux responseBound epsilon (x * eccentricityFoldFactor abar (foldedFrameEccentricityExponent g kappaRate)) kappaRate (Real.rpow 3 (-responseWindowOrder g) * (2 * Rad).rpow (r - responseWindowOrder g) * Cflux * r⁻¹ * Book.Ch03.constantCoeffMatrixNormHalf (identityConstantCoeffMatrix d) * responseOneFromTwoGapFactor (responseWindowOrder g) r * (foldedAnchoredResponseConstant d g kappaRate h.delta ↑J * max 1 ((Rad / cnorm) ^ (1 / 2))))

The folded-scale anchored residual frame provider. A parallel provider: the formulaic anchored provider is consumed as a black box and its frame constant is replaced by a law-free one, at the homogenization length folded by the eccentricity factor at the law-free exponent printRowOrder g * max (responseWindowOrder g) kappaRate / (2 * kappaRate ^ 2).

Every hypothesis is one of the original provider's own binders together with the frozen normalization data (hcnorm, hInner, hSandwich), which the Dirichlet conjunct supplies at its witness.