SharpGlobalFrame

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

The retained global frame in the upper Step-1 coefficient

The upper potential load contains a product of reciprocal running diffusivities at the observation index and at the fine cube scale. Applying the growth branch of the induction window at both indices retains the factor 3^(-gamma * (i - j)). After the Whitney-scale and observation-endpoint specializations, this internal frame supplies the global 3^(-gamma * (m - n)) factor printed in ABK26. A ratio-only comparison between the two diffusivities loses this factor.

These are internal coefficient estimates.

theorem Algsuperdiff.Section3.Provider.Multiscale.sigmaBar_inv_le_growth_branch {d : ℕ} (M : ABKModel d) {m₀ : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m₀ E) {j : ℤ} (hj : j ≤ m₀) : (↑(Annealed.sigmaBar M j))⁻¹ ≤ 2 * √((Disorder.cstar M)⁻¹ * M.gamma) * 3 ^ (-(M.gamma * ↑j))

The reciprocal running diffusivity bounded from the growth branch of the induction window at one scale.

theorem Algsuperdiff.Section3.Provider.Multiscale.sigmaBar_inv_mul_sigmaBar_inv_le_framed_wave_coefficient {d : ℕ} (M : ABKModel d) {m₀ i j : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M m₀ E) (hji : j ≤ i) (hi : i ≤ m₀) : (↑(Annealed.sigmaBar M i))⁻¹ * (↑(Annealed.sigmaBar M j))⁻¹ ≤ 4 * (Disorder.cstar M)⁻¹ * M.gamma * 3 ^ (-(2 * M.gamma * ↑j)) * 3 ^ (-(M.gamma * ↑(i - j)))

Applying the preceding growth estimate at both indices retains the global depth frame on the wave coefficient.