The Σ₁₂ endpoint q_D factor

The literal factor-one predicate in CaseISigma12QDEnvelopeFactor is false for arbitrary Section13HatLayers: its structure carries no relation between the two signed layers. The endpoint argument only needs a factor fixed in D. The result below supplies exactly that factor from the positive Section-13 contract; in particular the desired comparison is not assumed as a premise.

noncomputable def MathlibNt.SieveTheory.caseISigma12QDFixedFactor (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N : ℕ) (Δ s : ℝ) : ℝ

The fixed-in-D signed-layer quotient occurring after qD and errorEnvelope are expanded.

Equations

• MathlibNt.SieveTheory.caseISigma12QDFixedFactor H N Δ s = (s / (s - 1)) ^ Δ * (H.T (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (s - 1) / H.T (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N) s)

theorem MathlibNt.SieveTheory.caseISigma12_qD_sign_eq_pred (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N : ℕ} (hN : 1 ≤ N) (s : ℝ) : H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite (s - 1) = H.T (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth (N - 1)) (s - 1)

At successor depth, the delayed layer in q_D^∓ is literally the layer selected by the predecessor parity.

theorem MathlibNt.SieveTheory.caseISigma12_qD_le_fixedFactor_mul_errorEnvelope {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) (N : ℕ) {D d Δ s : ℝ} (hD : 1 < D) (hs : 2 ≤ s) : SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite D d Δ s ≤ caseISigma12QDFixedFactor H N Δ s * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s

The endpoint value q_D^∓(s) is bounded by a factor independent of D times the inherited envelope. This is the source-order comparison required by Σ₁₂; the fixed factor can subsequently be absorbed by the existing strict source-order gap.

theorem MathlibNt.SieveTheory.exists_caseISigma12_qD_envelope_factor {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) (N : ℕ) {Δ s : ℝ} (hs : 2 ≤ s) : ∃ (A : ℝ), 0 ≤ A ∧ ∀ (D d : ℝ), 1 < D → SwitchingPrinciple.SuzukiLemma144KappaOne.qD H (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).opposite D d Δ s ≤ A * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s

Packaged form: for fixed H,N,Δ,s, one nonnegative constant works for every D>1 and every d.