High-contrast homogenization: #
Provider.PolynomialHomogenization.Root.RowSupply.FormulaicAnchoredResidualFrameRate
Imported from the Apache-2.0 HighContrastHomogenization development at commit
7a13dbcd8d6609264a713373f5c69ceeac870472.
Row-level residual-frame rate provider #
The physical block row is transported through the exact triadic dilation and converted to the response-window order before the all-depth sum. One common normalized-reference parent is then used for every ruled observation cell.
theorem
HCPolySupport.HighContrast.RowSupply.RowRetainingPrintOrderGoodScale.exists_formulaicAnchoredResidualFrameResponseRate
{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))
:
∃ (N : ℕ) (G : ℕ) (J : ℕ) (lambda : ℝ) (deltaScaled : ℝ) (aScaled : CoeffSpace d) (aRef : Book.Ch03.CoeffFamily d) (L :
ℕ) (M : ℤ) (responseBound : system.CellIndex → ℝ) (Kframe : ℝ),
lambda = epsilon * 3 ^ N ∧ lambda ∈ Set.Icc 1 3 ∧ aScaled = Quenched.physicalScaleCoefficient N a ∧ deltaScaled = triadicallyScaledRowAmplitude h.delta (h.activationScale a) N (2 * kappaRate) ∧ witnessEccentricity (symmPart abar) * √↑d ≤ 3 ^ ↑G ∧ 3 ^ ↑G ≤ 1 + 3 * (witnessEccentricity (symmPart abar) * √↑d) ∧ L = Certificate.formulaicNormalizedReferenceTailShift d (responseWindowOrder g)
(Certificate.printRowOrder g) (2 * kappaRate) G ∧ ↑L < max 0
(Real.logb 3
(Certificate.shiftedTailAbsorptionPrefactor d (responseWindowOrder g)
(Certificate.printRowOrder g) G) / (2 * kappaRate)) + 1 ∧ 2 * Rad ≤ 3 ^ ↑J ∧ 3 ^ ↑J ≤ 1 + 3 * (2 * Rad) ∧ M = max (max (↑L) (↑J + 1)) 1 ∧ Kframe = Cflux * r⁻¹ * Book.Ch03.constantCoeffMatrixNormHalf (identityConstantCoeffMatrix d) * responseOneFromTwoGapFactor (responseWindowOrder g) r * √(observationFillingCoefficient d lambda abar * (Book.Ch02.geometricDiscount (1 - 2 * responseWindowOrder g) 1)⁻¹) * Real.rpow 3 ((r - kappaRate) * ↑M + kappaRate * ↑L - r) * √h.delta ∧ (∀ (Q : TriadicCube d),
(aRef.coeffOn Q).toCoeffField = affineCoefficient (Selection.normalizedRoot (symmPart abar)) ⋯
↑↑(normalizedCenteredCoeff aScaled abar hS)) ∧ ScalarIdentityPowerTail aRef (responseWindowOrder g) (√deltaScaled) kappaRate (3 ^ ↑L) ∧ ↑L ≤ M ∧ (∀ (i : system.CellIndex), (ruledObservationCube system i).scale ≤ M) ∧ (∀ (i : system.CellIndex),
responseBound i = √(observationFillingCoefficient d lambda abar * (Book.Ch02.geometricDiscount (1 - 2 * responseWindowOrder g) 1)⁻¹) * Real.rpow 3
(responseWindowOrder g * (↑M - ↑(ruledObservationCube system i).scale)) * √deltaScaled * Real.rpow 3 (-kappaRate * (↑M - ↑L))) ∧ (∀ (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 kappaRate Kframe
Row-level order conversion followed by fixed-parent aggregation supplies both the cellwise response bounds and the physical-frame RATE-AGG premise.