theorem Section10Lemma1017Comparison.propagate_one_unit {P Q : ℝ → ℝ} (h : SignedPQData P Q) {ρ a : ℝ} (hρ : 0 < ρ) (ha : 4 ≤ a) (hprev : ∀ t ∈ Set.Icc (a - 1) a, |P t| ≤ ρ * Q t) (t : ℝ) : t ∈ Set.Icc a (a + 1) → |P t| ≤ ρ * Q t

A weak envelope on one closed unit interval propagates to the next closed unit interval. The proof is genuinely over the reals: if the envelope first failed, compactness supplies a first nonnegative point; continuity makes it an equality point, while Claim 10.18 makes it strict.

theorem Section10Lemma1017Comparison.global_eta_of_compact_seed {P Q : ℝ → ℝ} (h : SignedPQData P Q) (hpoint : ∀ t ∈ Set.Icc 3 4, |P t| < Q t) : ∃ (η : ℝ), 0 < η ∧ η < 1 ∧ ∀ (s : ℝ), 3 ≤ s → |P s| ≤ η * Q s

A compact strict seed on [3,4] propagates to every real s ≥ 3. The natural-number induction is only used to cover successive real unit intervals; propagate_one_unit proves every point of each interval.

theorem Section10Lemma1017Comparison.lemma10_17_global_uniform_eta {Tplus Tminus P Q : ℝ → ℝ} (h : SignedPQData P Q) (hP : P = fun (s : ℝ) => Tplus s - Tminus s) (hQ : Q = fun (s : ℝ) => Tplus s + Tminus s) (hp_pos : ∀ s ∈ Set.Icc 3 4, 0 < Tplus s) (hm_pos : ∀ s ∈ Set.Icc 3 4, 0 < Tminus s) : ∃ (η : ℝ), 0 < η ∧ η < 1 ∧ ∀ (s : ℝ), 3 ≤ s → |P s| ≤ η * Q s

Lemma 10.17, source-facing global endpoint. Positivity of the two hat layers automatically supplies the compact seed; no global P/Q comparison is assumed.