Iterates Discharge Diffusivity #
Support for the Armstrong–Vicol anomalous-diffusion formalization.
theorem
AVenhance.Infra.Section4.iterate_chain_ratio_bound
{β Ck P κ : ℝ}
(I : Ingredients β)
(hCk : 0 ≤ Ck)
(hP : Ck ≤ P)
(hPt : Section3.kappaPrimeEndpointExpratConstant β ≤ P)
{m M : ℕ}
(hm : 2 ≤ m)
(hmM : m ≤ M)
(hκ : 0 < κ)
(hPerm : κ ∈ permittedInterval β I.Λ M)
(hA5 :
∀ (j : ℕ),
2 ≤ j →
j < M → epsilon β I.Λ j ^ 2 / (I.kappaAt κ j (M - j) * tau β I.Λ j) ≤ Ck * epsilon β I.Λ (j - 1) ^ (4 * delta β))
:
A terminal-aware exprat bound. The interior diffusivity-recursion estimate is never applied at m=M.
theorem
AVenhance.Infra.Section4.iterate_chain_step_size
{β Ccut κ : ℝ}
(I : Ingredients β)
(hz : I.Czeta ≤ Ccut)
(hh : I.Chat ≤ Ccut)
{m M : ℕ}
(hm : 1 ≤ m)
(hmM : m ≤ M)
(hκ : 0 < κ)
(hsmall :
Section3.lAmtOneStepConstant β Ccut * (epsilon β I.Λ m ^ 2 / (I.kappaAt κ m (M - m) * tau β I.Λ m) + epsilon β I.Λ (m - 1) ^ delta β) ≤ 9 / 160)
:
One-step enhancement controls its whole size, including the terminal step. This is the same terminal-aware mechanism used by Amnr and RelativeError KappaProduct.
theorem
AVenhance.Infra.Section4.iterate_chain_Kmat_entry_bound
{β Ccut κ : ℝ}
(I : Ingredients β)
(hz : I.Czeta ≤ Ccut)
{m M : ℕ}
(hm : 1 ≤ m)
(hκ : 0 < κ)
(hcondition : epsilon β I.Λ m ^ 2 ≤ I.kappaAt κ m (M - m) * tau β I.Λ m / 2)
(hsize :
I.kappaAt κ m (M - m) + a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / I.kappaAt κ m (M - m) ≤ 160 / 9 * I.kappaAt κ (m - 1) (M - (m - 1)))
(t : ℝ)
(j k : Fin 2)
:
Kmat is time-only; its zeroth entry bound needs no material flow estimate.