TUpgrade Consumers Amplitude

Support for the Armstrong–Vicol anomalous-diffusion formalization.

theorem AVenhance.Infra.Section4.iterate_coordinate_profile_amplitude_mono {u : ℝ → Homogenization.Vec 2 → ℝ} {κ N B L : ℝ} {i : ℕ} (hN : 0 ≤ N) (hNB : N ≤ B) (h : iterateCoordinateEnergyProfile u κ N L i) : iterateCoordinateEnergyProfile u κ B L i

Enlarging a nonnegative amplitude preserves every coordinate energy.

theorem AVenhance.Infra.Section4.iterate_amplitude_bound_of_strict_enlargements {a N K : ℝ} (hK : 0 ≤ K) (h : ∀ (B : ℝ), N < B → a ≤ B * K) : a ≤ N * K

Remove an artificial strict-positivity premise without dividing by the amplitude.