High-contrast homogenization:

Provider.PolynomialHomogenization.Root.Dirichlet.ExplicitFoldedFluxConstant

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

(α) part one: the flux constant of the folded row, made explicit

The aggregation concludes ∃ Kflux, 0 ≤ Kflux ∧ …, because it hides its own constant behind an existential. read off from PhysicalFluxRateAggregationConditional:55 that the witness is (3 ^ b · Kframe) ^ 2 · Kenergy, and recorded that reading as not available as a theorem.

This module repeats the same three steps — the observation-to-physical response transfer, the response/energy aggregation and the cap comparison — without the existential, so the constant is a named term in the conclusion:

Kflux = (3 ^ responseWindowOrder g · foldedAnchoredFrameConstant …) ^ 2 · Kenergy

with foldedAnchoredFrameConstant definitionally the exported frame constant, explicit in (d, g, κ, r, Cflux, Rad, cnorm, h.delta, J). The bracket 2 Rad ≤ 3 ^ J ≤ 1 + 3 (2 Rad) is exported alongside it, so the J can be traded for Rad downstream; no hypothesis of the aggregation is added, removed or weakened.

noncomputable def HCPolySupport.HighContrast.RowSupply.foldedAnchoredFrameConstant (d : ℕ) (g kappaRate r Cflux Rad cnorm delta J : ℝ) : ℝ

The frame constant, named. Definitionally the constant that RowRetainingPrintOrderGoodScale.exists_foldedAnchoredResidualFrameResponseRate exports: explicit in the dimension, the printed orders, the rate, the flux constant, the outer sandwich radius, the normalization radius, the certificate's amplitude and the bracket generation.

Equations

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

theorem HCPolySupport.HighContrast.RowSupply.RowRetainingPrintOrderGoodScale.explicit_foldedAnchoredPhysicalFluxDefectRate {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 : ℝ} (hd : 1 ≤ d) (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) (hrOne : r < 1) (aPhysical : CoeffField d) (haPhysical : aPhysical = affineCoefficient (matSqrt (symmPart abar)) ⋯ fun (z : Vec d) => scaledCoeff epsilon a z - skewPart abar) (aObs aCell : 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)) (u : H1Function U) (wCell : (i : system.CellIndex) → Book.Ch03.ForcedCubeSolution (whitneyCellCube system i) (aCell i) 0) (hfamily : RuledCellPhysicalForcedFamily system aPhysical u aCell wCell) {Kenergy : ℝ} {boundaryEnergy : ENNReal} (hKenergy : 0 ≤ Kenergy) (hglobalEnergy : (eVolumeAverage U fun (z : Vec d) => ENNReal.ofReal (coefficientEnergyDensity aPhysical u.grad z)) ≤ ENNReal.ofReal Kenergy * boundaryEnergy) {Uphys : Set (Vec d)} {cnorm : ℝ} (hcnorm : 0 < cnorm) (hInner : ellipsoid abar cnorm ⊆ Uphys) (hSandwich : HasBallSandwich (matImage (matSqrt (symmPart abar))⁻¹ Uphys) rho Rad) : ∃ (J : ℕ), 2 * Rad ≤ 3 ^ ↑J ∧ 3 ^ ↑J ≤ 1 + 3 * (2 * Rad) ∧ normalizedWhitneyRowEnergy system (physicalFullDualWhitneyFamilyCellEnergy system r (ruledPhysicalFluxDefectOnCell system aPhysical (fun (x : system.CellIndex) => identityConstantCoeffMatrix d) u)) ≤ ENNReal.ofReal ((Real.rpow 3 (responseWindowOrder g) * foldedAnchoredFrameConstant d g kappaRate r (coarseFluxResponseConstant d) Rad cnorm h.delta ↑J) ^ 2 * Kenergy * (epsilon * (x * eccentricityFoldFactor abar (foldedFrameEccentricityExponent g kappaRate))) ^ (2 * kappaRate)) * boundaryEnergy

(α), part one. The physical flux-defect row at the folded length, with the flux constant an explicit term rather than an existential witness.