A positive half-cell endpoint can be chosen separately for each positive time. The resulting interval has refresh-scale length, and the source-rate bound gains the square root of that refresh scale.

theorem AVenhance.Infra.Section4.exists_positive_halfCell_endpoint_near {τ t : ℝ} (hτ : 0 < τ) (hτ1 : τ ≤ 1) (ht0 : 0 < t) (ht1 : t ≤ 1) : ∃ (l : ℤ), 0 < (↑l + 1 / 2) * τ ∧ (↑l + 1 / 2) * τ ≤ 1 ∧ max ((↑l + 1 / 2) * τ) t - min ((↑l + 1 / 2) * τ) t ≤ τ

For every point of [0,1], some positive half-cell endpoint in [0,1] is within one refresh length. The endpoint at τ/2 handles the initial half-cell; otherwise the floor chooses the preceding half-cell endpoint.

theorem AVenhance.Infra.Section4.hm_tauPP_le_one {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) : tauPP β I.Λ m ≤ 1

The actual Section 4 refresh time is at most one, so the geometric selector applies to every positive time up to one.

theorem AVenhance.Infra.Section4.hm_positive_time_halfCell_endpoint {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) (t : ℝ) : t ∈ Set.Ioc 0 1 → ∃ (l : ℤ), 0 < (↑l + 1 / 2) * tauPP β I.Λ m ∧ (↑l + 1 / 2) * tauPP β I.Λ m ≤ 1 ∧ max ((↑l + 1 / 2) * tauPP β I.Λ m) t - min ((↑l + 1 / 2) * tauPP β I.Λ m) t ≤ tauPP β I.Λ m

At every positive time, choose a positive zero endpoint of the H_m within one τPP interval. The interval between the chosen endpoint and t has length at most τPP, in the exact min/max form used by the pairing FTC.

theorem AVenhance.Infra.Section4.hm_regular_source_halfCell_gain_of_rates {β : ℝ} (I : Ingredients β) {m : ℕ} {κ κprev Creg Cprod Cκ Ctau Theta G : ℝ} (hκ : 0 < κ) (hκprev : 0 < κprev) (hCreg : 0 ≤ Creg) (hCprod : 0 ≤ Cprod) (hCκ : 0 ≤ Cκ) (hCtau : 0 ≤ Ctau) (hTheta : 0 ≤ Theta) (hKprev : κprev ≤ Cκ * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β))) (hProduct : a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ ≤ Cprod * κprev) (hTauPP : a β I.Λ (m - 1) * tauPP β I.Λ m ≤ Ctau * epsilon β I.Λ (m - 1) ^ (2 * delta β)) (hSourceRate : G ≤ Creg * Theta * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (√κprev)⁻¹ * epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) : √(tauPP β I.Λ m) * G ≤ Creg * Cprod * √(Cκ * Ctau) * epsilon β I.Λ (m - 1) ^ delta β * Theta

The source rate from the Hm estimate gains epsilon^(δ) after multiplication by sqrt(τPP). hKprev is the diffusivity-recursion κ comparison, hProduct is the diffusivity-recursion product comparison, and hTauPP is the preceding-amplitude refresh-scale comparison. The scalar amplitude Theta is kept abstract.

theorem AVenhance.Infra.Section4.hm_positive_time_halfCell_source_gain {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ κprev Creg Cprod Cκ Ctau Theta G : ℝ} (hκ : 0 < κ) (hκprev : 0 < κprev) (hCreg : 0 ≤ Creg) (hCprod : 0 ≤ Cprod) (hCκ : 0 ≤ Cκ) (hCtau : 0 ≤ Ctau) (hTheta : 0 ≤ Theta) (hGnonneg : 0 ≤ G) (hKprev : κprev ≤ Cκ * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β))) (hProduct : a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ ≤ Cprod * κprev) (hTauPP : a β I.Λ (m - 1) * tauPP β I.Λ m ≤ Ctau * epsilon β I.Λ (m - 1) ^ (2 * delta β)) (hSourceRate : G ≤ Creg * Theta * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (√κprev)⁻¹ * epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) (t : ℝ) : t ∈ Set.Ioc 0 1 → ∃ (l : ℤ), have c := (↑l + 1 / 2) * tauPP β I.Λ m; 0 < c ∧ c ≤ 1 ∧ max c t - min c t ≤ tauPP β I.Λ m ∧ √(max c t - min c t) * G ≤ Creg * Cprod * √(Cκ * Ctau) * epsilon β I.Λ (m - 1) ^ delta β * Theta

The source-rate gain and endpoint choice together give the exact coefficient bound needed in the regular-pairing Cauchy estimate on each positive-time interval. The returned interval length is in the same min / max form as frozen_hm_positive_time_bounds_of_pairings.

theorem AVenhance.Infra.Section4.hm_positive_time_halfCell_source_gain_from_A5 {β : ℝ} (I : Ingredients β) {m : ℕ} (hm : 1 ≤ m) {κ κprev Creg Cprod Cκ Theta G : ℝ} (hκ : 0 < κ) (hκprev : 0 < κprev) (hCreg : 0 ≤ Creg) (hCprod : 0 ≤ Cprod) (hCκ : 0 ≤ Cκ) (hTheta : 0 ≤ Theta) (hGnonneg : 0 ≤ G) (hKprev : κprev ≤ Cκ * (a β I.Λ (m - 1) * epsilon β I.Λ (m - 1) ^ (2 + gamma β))) (hProduct : a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ ≤ Cprod * κprev) (hSourceRate : G ≤ Creg * Theta * (a β I.Λ m ^ 2 * epsilon β I.Λ m ^ 4 / κ) * (√κprev)⁻¹ * epsilon β I.Λ (m - 1) ^ (-(1 + gamma β / 2))) (t : ℝ) : t ∈ Set.Ioc 0 1 → ∃ (l : ℤ), have c := (↑l + 1 / 2) * tauPP β I.Λ m; 0 < c ∧ c ≤ 1 ∧ max c t - min c t ≤ tauPP β I.Λ m ∧ √(max c t - min c t) * G ≤ Creg * Cprod * √(Cκ * 2 ^ (-25)) * epsilon β I.Λ (m - 1) ^ delta β * Theta

Inputs in the form of the diffusivity-recursion estimate plus the unconditional a_(m-1) τPP_m bound give the half-cell source gain. This wrapper removes the scale comparison from the caller: amplitude_tauPP_bounds supplies the coefficient 2⁻²⁵.