Abstract-real scale arithmetic for the tiny source contract #
Pure real lemmas (no project definitions). The smallness x^{δ N_*} of the last increment
(x = ε_{m-1}) beats the polynomial losses r² L² of the coefficient jets and of the analytic
radius, and the loss √κ_{m-1}/√κ_m ≲ ε_m^{-β} coming from the lower bound
ε_m^{2β} ≤ K κ_m κ_{m-1} (a_m² ε_m⁴/κ_m ≤ K κ_{m-1}).
theorem
AVenhance.Infra.Section5.Contracts.sc_Z_core
{x εm κm κp K Y δ q β E : ℝ}
(hx0 : 0 < x)
(hx1 : x ≤ 1)
(hεm : 0 < εm)
(hκm : 0 < κm)
(hκp : 0 < κp)
(hK : 1 ≤ K)
(hκpK : κp ≤ K)
(hβ : 0 < β)
(hpow : x ^ q ≤ 2 * εm)
(hε : εm ^ (2 * β) ≤ K * κp * κm)
(hE : δ + q * β ≤ E)
(hY : 0 ≤ Y)
:
√κ_{m-1} · Y x^E ≤ C x^δ √κ_m, from E ≥ δ + q β, x^q ≤ 2 ε_m, ε_m^{2β} ≤ K κ_{m-1} κ_m
and κ_{m-1} ≤ K.
theorem
AVenhance.Infra.Section5.Contracts.sc_Z_chain
{x δ γ Cs Cs' F N : ℝ}
(hx0 : 0 < x)
(hCs : 0 ≤ Cs)
:
The product of the polynomial losses and the smallness (C x^{2δ})^{N/2} is a single power
of x.
The coefficient constant: c ≤ C_c (κ_{m-1} C_B)² r⁴ for r ≥ 1.
theorem
AVenhance.Infra.Section5.Contracts.sc_final_chain
{x κp B CB CZ Y Cc c G A F L' r S E δ sk : ℝ}
(hκp : 0 < κp)
(hCB : 0 ≤ CB)
(hB : 0 ≤ B)
(hG0 : 0 ≤ G)
(hr : 0 ≤ r)
(hcle : c ≤ Cc * ((κp * CB) ^ 2 * r ^ 4))
(hsum : √(c * S) ≤ √(7 * c) * (G / √κp))
(hG : G = B * A * F * L' ^ 2)
(hchain : r ^ 2 * A * F * L' ^ 2 = Y * E)
(hZ : √κp * (Y * E) ≤ CZ * x ^ δ * sk)
:
The final scalar chain for the nondivergence energy.