CubeRatio

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

The conditional per-cube estimate at a mesoscopic cube

Source: ABK26. Once the smallness condition has been verified at a mesoscopic triadic cube R, the conditional sensitivity machinery applies there and yields

lambda_{t,q}^{-1}(R; a + h)  <=  2 lambda_{t,q}^{-1}(R; a) .

This module proves the one-cube specialization of that statement, namely the factor-two ratio for the pure-flux response and hence for |sigma_*^{-1}(R)|.

• the ratio engine at R (CubeGauge.cubeGauge_ratio_engine) together with the crude bound (CubeGauge.cubeGauge_le_crude) feeds the gauge-free self-referential bootstrap Provider.Lambda.Bootstrap, whose smallness gate 4 K Psi(0) <= 1/2 is exactly the mesoscopic smallness condition;
• the bootstrap's closed form gives the ratio 1 + 4 K Psi(0) <= 2 for the pure-flux response at R;
• Provider.Lambda.DescendantBridge converts the all-loadings response ratio into the |sigma_*^{-1}(R)| ratio consumed by the mesoscale assembly.

The smallness condition is a hypothesis of both statements below; it is discharged, unconditionally, in LambdaUnconditional.Closure.

Every declaration in this module is an internal helper for the Section 2.4 sensitivity providers.

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.perturbCoeffOn_zero_aeeq_domain {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (c : HCPolySupport.Book.Ch02.CoeffOn U) (g : Frozen.Section24.LInfSkewMatrixFieldOn U) : (Frozen.Section24.perturbCoeffOn U c g 0).AEEq c

The perturbation path starts at the base coefficient, at any domain.

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.responseJ_perturb_le_two_mul {d : ℕ} [NeZero d] (dimension : 2 ≤ d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) (hsmall : 4 * mesoFluxConst d h R * cubeGauge R a h.toLInfSkewMatrixFieldOn 0 ≤ 1 / 2) (w : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (Lambda.descendantField hk hR h.toLInfSkewMatrixFieldOn) 1) 0 w ≤ 2 * HCPolySupport.Book.Ch02.responseJ (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (Lambda.descendantField hk hR h.toLInfSkewMatrixFieldOn) 0) 0 w

The per-cube conditional estimate at a mesoscopic cube. Under the mesoscopic smallness condition, the pure-flux response of the perturbed field is at most twice the pure-flux response of the base field, at every loading.

hsmall is the mesoscopic smallness condition; it is discharged unconditionally at the mesoscopic depth in LambdaUnconditional.Closure.

theorem Algsuperdiff.Section24.Sensitivity.Provider.LambdaUnconditional.coarseSigmaStarInvMatrixNorm_perturb_le_two {d : ℕ} [NeZero d] (dimension : 2 ≤ d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.UnitCubeSkewW2Infinity d) (F G : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (hF : (F.coeffOn (HCPolySupport.originCube d 0)).AEEq a) (hG : (G.coeffOn (HCPolySupport.originCube d 0)).AEEq (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0)) a h.toLInfSkewMatrixFieldOn 1)) {k : ℤ} (hk : k ≤ (HCPolySupport.originCube d 0).scale) {R : HCPolySupport.TriadicCube d} (hR : R ∈ HCPolySupport.descendantsAtScale (HCPolySupport.originCube d 0) k) (hsmall : 4 * mesoFluxConst d h R * cubeGauge R a h.toLInfSkewMatrixFieldOn 0 ≤ 1 / 2) : HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R G ≤ 2 * HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm R F

The per-cube sigma_*^{-1} ratio at a mesoscopic cube. This is the form consumed by the mesoscale assembly Provider.Mesoscale.LambdaAssembly.unitCubeLambda_inv_le_of_mesoscale_descendant_ratio.