ResponseCommonDomination

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

Simultaneous directional response domination

The Section 3.5 response is evaluated from one measurable representative of the entire coarse block matrix. On the common physical event, every unit direction is bounded by the square of the observation-cube homogenization error formed from that same representative. The coefficient cutoff scale and observation scale remain separate.

theorem Algsuperdiff.Section3.Provider.Homogenization.ae_forall_cutoffResponseJ_le_observationHomogenizationError_sq {d : ℕ} (M : ABKModel d) (cubeScale coefficientScale : ℤ) {s : ℝ} (hs : 0 < s) : ∀ᵐ (omega : Cutoff.CutoffSample d) ∂↑(Cutoff.cutoffSampleLaw M), ∀ (e : HCPolySupport.Vec d), HCPolySupport.Book.Ch02.vecNorm e = 1 → Observable.cutoffResponseJ M cubeScale coefficientScale e omega ≤ Observable.cutoffHomogenizationErrorRepresentative M coefficientScale cubeScale s (Annealed.sigmaBar M coefficientScale) omega ^ 2

On one probability-one event, the observation-cube homogenization error dominates the actual cutoff response simultaneously in every unit direction. The comparator is the genuine running diffusivity at the coefficient cutoff scale.