Finite-prefix control of the actual coupling recurrence. Each step may use only the bounds already proved on its preceding prefix.

theorem EulerParentRenewalPrefix.relative_step_error {a b e : ℝ} (ha : 0 < a) (ha2 : a ≤ 2) (he : 0 ≤ e) (h : |b / a - 1| ≤ e) : |b - a| ≤ 2 * e

theorem EulerParentRenewalPrefix.partial_sum_le {e : ℕ → ℝ} {η : ℝ} (he : EulerPacketSourceScaleChoice.SmallSeries e η) (n : ℕ) : ∑ i ∈ Finset.range n, e i ≤ η

theorem EulerParentRenewalPrefix.bounds_of_accumulated_error {e : ℕ → ℝ} {η v : ℝ} (he : EulerPacketSourceScaleChoice.SmallSeries e η) (hη : η ≤ 1 / 4) (n : ℕ) (hv : |v - 1| ≤ 2 * ∑ i ∈ Finset.range n, e i) : 1 / 2 ≤ v ∧ v ≤ 2

theorem EulerParentRenewalPrefix.accumulate_step {a e : ℕ → ℝ} (n : ℕ) (ha : 1 / 2 ≤ a n) (ha2 : a n ≤ 2) (he : 0 ≤ e n) (hprev : |a n - 1| ≤ 2 * ∑ i ∈ Finset.range n, e i) (hstep : |a (n + 1) / a n - 1| ≤ e n) : |a (n + 1) - 1| ≤ 2 * ∑ i ∈ Finset.range (n + 1), e i

theorem EulerParentRenewalPrefix.coupling_prefix {a e : ℕ → ℝ} {η : ℝ} (N : ℕ) (he : EulerPacketSourceScaleChoice.SmallSeries e η) (hη : η ≤ 1 / 4) (hzero : a 0 = 1) (hstep : ∀ n < N, (∀ i ≤ n, 1 / 2 ≤ a i ∧ a i ≤ 2) → |a (n + 1) / a n - 1| ≤ e n) (n : ℕ) : n ≤ N → (1 / 2 ≤ a n ∧ a n ≤ 2) ∧ |a n - 1| ≤ 2 * ∑ i ∈ Finset.range n, e i

No bound on a future coupling is an input. The step estimate can be established only after the previous finite prefix has been bounded.

theorem EulerParentRenewalPrefix.coupling_and_tilt_prefix {a β x e : ℕ → ℝ} {η : ℝ} (N : ℕ) (he : EulerPacketSourceScaleChoice.SmallSeries e η) (hη : η ≤ 1 / 4) (hzero : a 0 = 1) (hβzero : 1 / 2 ≤ β 0 * x 0 ^ 2 ∧ β 0 * x 0 ^ 2 ≤ 2) (hstep : ∀ n < N, (∀ i ≤ n, (1 / 2 ≤ a i ∧ a i ≤ 2) ∧ 1 / 2 ≤ β i * x i ^ 2 ∧ β i * x i ^ 2 ≤ 2) → |a (n + 1) / a n - 1| ≤ e n ∧ 1 / 2 ≤ β (n + 1) * x (n + 1) ^ 2 ∧ β (n + 1) * x (n + 1) ^ 2 ≤ 2) (n : ℕ) : n ≤ N → (1 / 2 ≤ a n ∧ a n ≤ 2) ∧ (1 / 2 ≤ β n * x n ^ 2 ∧ β n * x n ^ 2 ≤ 2) ∧ |a n - 1| ≤ 2 * ∑ i ∈ Finset.range n, e i

The same finite induction propagates the normalized tilt invariant along with the coupling. Its hypotheses mention only already-built stages.

theorem EulerParentRenewalPrefix.stage_congr_at {J D : ℕ} {C c X K : ℝ} {a β b γ : ℕ → ℝ} {n : ℕ} (G : EulerPacketSourceScaleGuards.StageGuards J D C c X K a β n) (ha : a n = b n) (hβ : β n = γ n) : EulerPacketSourceScaleGuards.StageGuards J D C c X K b γ n

theorem EulerParentRenewalPrefix.stage_guards_at (J D : ℕ) (hJ : 3 ≤ J) (C c X K δ : ℝ) (hC : 4 ≤ C) (hX : 8 ≤ X) (hK : 1 ≤ K) (hδ : δ ≤ 1 / 2) (hδK : 1000000 * K * δ ≤ 1) (hb : EulerPacketSourceScaleActual.ActualBounds J D C c X δ) (a β : ℕ → ℝ) (n : ℕ) (ha : 1 / 2 ≤ a n) (ha2 : a n ≤ 2) (hβ : 1 / 2 ≤ β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2) (hβ2 : β n * EulerPacketSourceScaleChoice.scaleSequence J X n ^ 2 ≤ 2) : EulerPacketSourceScaleGuards.StageGuards J D C c X K a β n

Extend just the current scalar values to a bounded artificial sequence, apply the uniform theorem, then transfer its local conclusion. No hypotheses on any future stage are required.