Iterates Physical Kernel Gains

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_physical_stream_kernel_gains {a e γ κ c L F : ℝ} (ha : 0 ≤ a) (he : 0 < e) (hκ : 0 < κ) (hc : 0 < c) (hL : 0 < L) (hFp : 0 < F) (hlower : c * (a * e ^ (2 + γ)) ≤ κ) (hF : F = e ^ (1 + γ / 2) * L) : 24 * (2 * (2 ^ 19 * a) / L ^ 2) / κ ≤ 48 * 2 ^ 19 / c / F ^ 2 ∧ 24 * (16 / κ * (32 * a * e ^ 2) ^ 2 * (2 * (256 * e⁻¹ / L) ^ 2) ^ 2) / κ ≤ 24 * (16 * 32 ^ 2 * 4 * 256 ^ 4) / c ^ 2 / F ^ 4

Literal diffusivity scaling supplies both stream kernels, including all absolute losses from the actual terminal norm estimate.

theorem AVenhance.Infra.Section4.iterate_physical_linear_kernel_gain {κ τ K a e H ρ : ℝ} (hκ : 0 < κ) (hK : 0 ≤ K) (he : e ≠ 0) (htime : τ * a ≤ H * ρ) : 24 * (8 * (2 * τ * K * κ) * (8192 * a * e) * (256 * e⁻¹)) / κ ≤ 24 * 8 * 2 * K * 2 ^ 21 * H * ρ

The linear material kernel keeps the primitive gain, after using the proved amplitude-times-period estimate.