PathGauge

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

Uniform control of the coarse gauge along the perturbation segment

The J sensitivity estimate applies the D_h bound at every point t of the segment a + t h, t ∈ [0,1], but its statement involves only the coarse gauge lambda_{3/8,2}^{-1} of the base coefficient. The source closes this gap by quoting the conditional lambda sensitivity estimate along the segment; in the present formalization the same content is produced directly by the self-referential bootstrap of Provider.Lambda.Bootstrap, which shows that under the frozen smallness gate the coarse gauge never more than doubles along the segment.

The single analytic input is hcube, the p = 0 specialization of the D_h bound on every triadic descendant of the unit cube with the root gauge as coefficient — exactly the hcube premise of Provider.Lambda.Spine.unitCubeLambda_inv_perturb_le_of_cube_dhFluxForm_bound. It is a premise here and is discharged where this lemma is used.

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

theorem Algsuperdiff.Section24.Sensitivity.Provider.Response.pathGauge_le_two_mul_of_cube_dhFluxForm_bound {d : ℕ} [NeZero d] (dimension : 2 ≤ d) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) (h : Frozen.Section24.LInfSkewMatrixFieldOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) {K : ℝ} (hK : 0 ≤ K) (hcube : ∀ (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d), (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) (τ : ℝ) (w : HCPolySupport.Vec d), |Lambda.dhFluxForm (HCPolySupport.Book.Ch02.cubeDomain R) (Frozen.Section24.perturbCoeffOn (HCPolySupport.Book.Ch02.cubeDomain R) (F.coeffOn R) (Lambda.descendantField hk hR h) τ) (Lambda.descendantField hk hR h) w| ≤ 2 * (K * Lambda.pathGauge a h τ) * 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) τ) 0 w) (hsmall : 4 * K * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹ ≤ 1 / 2) (τ : ℝ) (hτ₀ : 0 ≤ τ) (hτ₁ : τ ≤ 1) : Lambda.pathGauge a h τ ≤ 2 * (Frozen.Section24.unitCubeLambda (3 / 8) (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) a)⁻¹

The coarse gauge at most doubles along the perturbation segment.

Given the per-descendant pure-flux D_h bound with the root gauge as coefficient (hcube) and the smallness gate 4 K lambda^{-1}(a) ≤ 1/2, the coarse gauge lambda_{3/8,2}^{-1} at every point of the segment a + tau h, tau ∈ [0,1], is at most twice its value at the base point.

This is the bootstrap conclusion Psi tau ≤ Psi 0 / (1 - 4 K Psi 0) of Provider.Lambda.Bootstrap.le_riccati_of_ratio_engine fed by the ratio engine of Provider.Lambda.Engine; the crude a-priori bound needed to run the engine is discharged here by Provider.Lambda.CrudeBound.