HomSpineResidueLevel

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

hlevel and hlevelDual with the EthmB(m) pairing DISCHARGED

What this file supplies

The installed hlevel and its dual carry three content-bearing hypotheses: the Theorem-C energy bound hSbound, and the pair hA/hB together with the budget split hsplit. This file DISCHARGES the second group at the concrete substitution against the two summands of EthmB(m):

• the defect witness is cut at E_B:= (EthmB(m))(ω).toReal — the same cut HomSpineFinalWitness makes for the root's clause (C2);
• C_w is the explicit sum of the four pairing constants (two per level condition), none of which carries randomness;
• hA, hB are then le_rfl — the slots ARE the pairing's left-hand sides — and hsplit is the budget split.

What remains of the two level conditions is:

  hSbound  (Theorem C's Step-2 energy density, at the printed constant shape)
  hdom1, hdom2  (the carrier seam — see `HomSpineResiduePairing`'s disclosure)
  hfin  (a.e. finiteness of the [0,∞] carrier: HomSpineFinalWitness's own step)

That pairing constant is bounded by the bundle's K_abs slot as a frame condition, not proved here: K_abs is a free parameter of the endpoint.

1. The base order and the Step-2 random factor

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutOrderBase {d : ℕ} (M : Section3.ABKModel d) (hlog : 4 ≤ |Real.log M.gamma|) : ↑HCPolySupport.FractionalOrder

The printed base order s = |log γ|⁻¹, as a FractionalOrder. Both conditions come from homS_le_quarter, i.e. from |log γ| ≥ 4.

Equations

• Algsuperdiff.Section4.Provider.Homogenization.recutOrderBase M hlog = ⟨Algsuperdiff.Section4.Provider.Homogenization.homS M, ⋯⟩

@[simp]

theorem Algsuperdiff.Section4.Provider.Homogenization.recutOrderBase_val {d : ℕ} (M : Section3.ABKModel d) (hlog : 4 ≤ |Real.log M.gamma|) : ↑(recutOrderBase M hlog) = homS M

noncomputable def Algsuperdiff.Section4.Provider.Homogenization.recutEnergyFactor {d : ℕ} (M : Section3.ABKModel d) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : ℝ

The random factor of the Step-2 constant: the minimal-scale factor 3^{(1-α)X_m(α)} times the printed 1 + 𝓔_{1/4}(□_m), cut to a real. hSbound's constant is C_en = C · recutEnergyFactor.

Equations

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

theorem Algsuperdiff.Section4.Provider.Homogenization.recutEnergyFactor_nonneg {d : ℕ} (M : Section3.ABKModel d) (Y : Section3.Cutoff.CutoffSample d → ENNReal) (m : ℤ) (omega : Section3.Cutoff.CutoffSample d) : 0 ≤ recutEnergyFactor M Y m omega