theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iii_uniform_reverse_adjacent_ratio_of_source {H : Section13HatLayers} (hH : Section13HatSourceContract H) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (sign : ErrorSign) (s σ : ℝ), 2 ≤ s → s ≤ σ → proposition131iiiReverseRatio H sign s ≤ C * (σ * Real.log (Real.exp 1 * σ))

Proposition 13.1(iii), reverse adjacent-ratio direction, with the residual Lemma-10.28 envelope premise discharged internally from the Section-13 source contract. One constant works for both signs and all 2 ≤ s ≤ σ.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD_opposite_le_errorEnvelope_of_source {H : Section13HatLayers} (hH : Section13HatSourceContract H) (Δ : ℝ) (hΔ : 0 ≤ Δ) : ∃ (C : ℝ), 1 ≤ C ∧ ∀ (N : ℕ) (D d σ : ℝ), 1 < D → 2 ≤ σ → qD H (ErrorSign.ofDepth N).opposite D d Δ σ ≤ C * (σ * Real.log (Real.exp 1 * σ)) * errorEnvelope H N D d σ

The q_D endpoint form used by Σ₁₂: the opposite-sign value at σ-1 is absorbed into the current error envelope with the explicit σ log(eσ) loss. For fixed Δ ≥ 0, the constant is uniform in the depth, cutoff, exponent d, and endpoint σ.