A κ=1, source-facing core of Lemma 10.17. The input package contains only signed DDEs, positivity/continuity, and the already proved zero-pairing identities. In particular, no global comparison |P| ≤ ρ Q is a field.

noncomputable def Section10Lemma1017Comparison.adjointPlus (s : ℝ) : ℝ

Equations

• Section10Lemma1017Comparison.adjointPlus s = s ^ 2 - 2 * s + 1 / 2

def Section10Lemma1017Comparison.adjointMinus (_s : ℝ) : ℝ

Equations

• Section10Lemma1017Comparison.adjointMinus _s = 1

theorem Section10Lemma1017Comparison.adjointPlus_dde (s : ℝ) : HasDerivAt (fun (u : ℝ) => u * adjointPlus u) (2 * adjointPlus s + adjointPlus (s + 1)) s

theorem Section10Lemma1017Comparison.adjointMinus_dde (s : ℝ) : HasDerivAt (fun (u : ℝ) => u * adjointMinus u) (2 * adjointMinus s - adjointMinus (s + 1)) s

theorem Section10Lemma1017Comparison.adjointPlus_pos {s : ℝ} (hs : 2 ≤ s) : 0 < adjointPlus s

structure Section10Lemma1017Comparison.SignedPQData (P Q : ℝ → ℝ) : Prop

The exact admissible input boundary for the κ=1 P/Q argument.

• continuousP : Continuous P
• continuousQ : Continuous Q
• positiveQ (s : ℝ) : 0 < s → 0 < Q s
• ddeP (s : ℝ) : 3 < s → HasDerivAt P (-(2 * P s - P (s - 1)) / s) s
• ddeQ (s : ℝ) : 3 < s → HasDerivAt Q (-(2 * Q s + Q (s - 1)) / s) s
• pairingP_zero (s : ℝ) : 3 ≤ s → s * adjointMinus s * P s + ∫ (t : ℝ) in s - 1..s, adjointMinus (t + 1) * P t = 0
• pairingQ_zero (s : ℝ) : 3 ≤ s → s * adjointPlus s * Q s - ∫ (t : ℝ) in s - 1..s, adjointPlus (t + 1) * Q t = 0

theorem Section10Lemma1017Comparison.strict_adjoint_window {Q : ℝ → ℝ} (hQ : Continuous Q) (hQpos : ∀ (t : ℝ), 0 < t → 0 < Q t) {s : ℝ} (hs : 3 ≤ s) : adjointPlus s * ∫ (t : ℝ) in s - 1..s, Q t < ∫ (t : ℝ) in s - 1..s, adjointPlus (t + 1) * Q t

Strict integral comparison behind Claim 10.18. It uses the explicit positive adjoint, rather than assuming any P/Q estimate.

theorem Section10Lemma1017Comparison.claim10_18_one_step_strict {P Q : ℝ → ℝ} (h : SignedPQData P Q) {ρ s : ℝ} (hρ : 0 < ρ) (hs : 3 ≤ s) (hwindow : ∀ t ∈ Set.Icc (s - 1) s, |P t| ≤ ρ * Q t) : |P s| < ρ * Q s

Claim 10.18, one-step strict improvement. A weak envelope on the current unit window becomes strict at its right endpoint. This is the local induction step; the data package itself contains no comparison assumption.

theorem Section10Lemma1017Comparison.compact_eta_extraction {P Q : ℝ → ℝ} (hP : Continuous P) (hQ : Continuous Q) {a b : ℝ} (hab : a ≤ b) (hQpos : ∀ s ∈ Set.Icc a b, 0 < Q s) (hpoint : ∀ s ∈ Set.Icc a b, |P s| < Q s) : ∃ (η : ℝ), 0 ≤ η ∧ η < 1 ∧ ∀ s ∈ Set.Icc a b, |P s| ≤ η * Q s

Compact extraction of a uniform coefficient strictly below one. This is applied to the positive hat-layer identities P=T⁺-T⁻, Q=T⁺+T⁻; those identities give the pointwise strict hypothesis without assuming a uniform comparison.

theorem Section10Lemma1017Comparison.compact_eta_for_positive_pair {Tplus Tminus : ℝ → ℝ} (hp : Continuous Tplus) (hm : Continuous Tminus) {a b : ℝ} (hab : a ≤ b) (hp_pos : ∀ s ∈ Set.Icc a b, 0 < Tplus s) (hm_pos : ∀ s ∈ Set.Icc a b, 0 < Tminus s) : ∃ (η : ℝ), 0 ≤ η ∧ η < 1 ∧ ∀ s ∈ Set.Icc a b, |Tplus s - Tminus s| ≤ η * (Tplus s + Tminus s)

For the Section 13 definitions P=T⁺-T⁻ and Q=T⁺+T⁻, the compact seed is automatic from strict positivity of the two hat layers. Thus the exported seed theorem does not take any P/Q comparison as a premise.

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

The compact seed followed by Claim 10.18 at its right endpoint.

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

Section-13-shaped public endpoint: positivity of T⁺,T⁻, the defining identities for P,Q, signed DDEs, explicit adjoints and pairing-zero produce a uniform compact coefficient and its strict Claim-10.18 improvement. There is no comparison hypothesis in this statement.