Uniform reverse adjacent ratio for the Σ₁₂ endpoint

The missing direction is the upper bound for the earlier, opposite-sign layer relative to the current layer. The source of this direction is the increasing W₊ half of Lemma 10.28. We freeze that earliest analytic edge below in its multiplied (10.44) form; no adjacent-value quotient is a field of the edge.

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section10Lemma1028ReverseEnvelopeEdge (R : ℝ → ℝ) : Prop

The increasing-envelope half of Lemma 10.28, specialized to DDE(2,1,3). By (10.44), this is exactly (log W₊)' ≥ 0 after multiplication by the positive value s * R s. The constants precede the moving variable.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section10Lemma1028ReverseEnvelopeEdge R = ∃ (c : ℝ) (S : ℝ), 1 ≤ c ∧ Real.exp 2 ≤ S ∧ 4 ≤ S ∧ ∀ (s : ℝ), S ≤ s → 0 ≤ -R (s - 1) + s * (Section10CanonicalXi.xi s + c - 2 / s) * R s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.canonicalXi_add_const_le_log_e_mul (c : ℝ) : ∃ (A : ℝ), 1 ≤ A ∧ ∀ (s : ℝ), Real.exp 2 ≤ s → Section10CanonicalXi.xi s + c - 2 / s ≤ A * Real.log (Real.exp 1 * s)

The canonical phase in the increasing-envelope edge is at most a fixed multiple of log (e s).

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section10_reverse_unitShift_after_cutoff {R : ℝ → ℝ} (hpos : ∀ (s : ℝ), 0 < s → 0 < R s) (hedge : Section10Lemma1028ReverseEnvelopeEdge R) : ∃ (A : ℝ) (S : ℝ), 1 ≤ A ∧ Real.exp 2 ≤ S ∧ 4 ≤ S ∧ ∀ (s : ℝ), S ≤ s → R (s - 1) ≤ A * (s * Real.log (Real.exp 1 * s)) * R s

Lemma 10.28's increasing envelope gives the missing direction of Lemma 10.29, uniformly after one fixed cutoff.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiiReverseRatio (H : Section13HatLayers) (sign : ErrorSign) (s : ℝ) : ℝ

The literal opposite-earlier/current quotient required at the Σ₁₂ endpoint.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.proposition131iiiReverseRatio H sign s = H.T sign.opposite (s - 1) / H.T sign s

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

Source-faithful uniform reverse adjacent ratio. A single constant works for both signs and every moving endpoint 2 ≤ s ≤ σ. The only residual source premise is the increasing-envelope half of Lemma 10.28 for the common Qhat; compact coordinates are discharged by continuity and positivity.