def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.clampTwo (R : ℝ → ℝ) (s : ℝ) : ℝ

A global continuous extension which does not alter a Section-13 function on [2,∞).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.clampTwo R s = R (max s 2)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.clampTwo_continuous {R : ℝ → ℝ} (hR : ContinuousOn R (Set.Ioi 0)) : Continuous (clampTwo R)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.clampTwo_eq {R : ℝ → ℝ} {s : ℝ} (hs : 2 ≤ s) : clampTwo R s = R s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.movingWindow_continuous {f : ℝ → ℝ} (hf : Continuous f) : Continuous fun (s : ℝ) => ∫ (t : ℝ) in s - 1..s, f t

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.signedPairing_continuous {b : ℝ} {R q : ℝ → ℝ} (hR : Continuous R) (hq : Continuous q) : Continuous (section10SignedPairing b R q)

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.continuous_zero_at_three {F : ℝ → ℝ} (hF : Continuous F) (hz : ∀ (s : ℝ), 3 < s → F s = 0) : F 3 = 0

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.pairing_clampTwo {b s : ℝ} {R q : ℝ → ℝ} (hs : 3 ≤ s) : section10SignedPairing b (clampTwo R) q s = section10SignedPairing b R q s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.clampTwo_hasDerivAt_P {H : Section13HatLayers} (hH : Section13HatSourceContract H) {s : ℝ} (hs : 3 < s) : HasDerivAt (clampTwo (section13Phat H)) (-(2 * clampTwo (section13Phat H) s - clampTwo (section13Phat H) (s - 1)) / s) s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.clampTwo_hasDerivAt_Q {H : Section13HatLayers} (hH : Section13HatSourceContract H) {s : ℝ} (hs : 3 < s) : HasDerivAt (clampTwo (section13Qhat H)) (-(2 * clampTwo (section13Qhat H) s + clampTwo (section13Qhat H) (s - 1)) / s) s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.section13_signedPQData {H : Section13HatLayers} (hH : Section13HatSourceContract H) : Section10Lemma1017Comparison.SignedPQData (clampTwo (section13Phat H)) (clampTwo (section13Qhat H))

The actual globally continuous SignedPQData required by Lemma 10.17. No comparison or pairing premise is used: the pairings come from Section 13.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.section13_global_uniform_eta {H : Section13HatLayers} (hH : Section13HatSourceContract H) : ∃ (η : ℝ), 0 < η ∧ η < 1 ∧ ∀ (s : ℝ), 3 ≤ s → |section13Phat H s| ≤ η * section13Qhat H s

Global Lemma 10.17 coefficient assembled from the source contract alone.

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.Section13HatSection10BridgeAtThree (H : Section13HatLayers) (sign : ErrorSign) : Type

A corrected sign-independent Section-10 bridge on the actual scalar-DDE range s ≥ 3. This records exactly what the pairing + Lemma 10.17 assembly proves for both signs.

• Qhat : ℝ → ℝ
• dde : Section10DDEApparatus self.Qhat 3
• K : ℝ
• one_le_K : 1 ≤ self.K
• hat_le (s : ℝ) : 3 ≤ s → H.T sign s ≤ self.K * self.Qhat s
• Q_le (s : ℝ) : 3 ≤ s → self.Qhat s ≤ self.K * H.T sign s

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.section13_bridgeAtThree {H : Section13HatLayers} (hH : Section13HatSourceContract H) (sign : ErrorSign) : Section13HatSection10BridgeAtThree H sign

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.section13_bridgeAtThree hH sign = { Qhat := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13Qhat H, dde := { adjoint := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.section13AdjointPlus, beta_ge_one := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.section13_bridgeAtThree._proof_9, continuous := ⋯, positive := ⋯, adjoint_positive := ⋯, original_dde := ⋯, adjoint_dde := ⋯, pairing_zero := ⋯ }, K := 2 / (1 - Classical.choose ⋯), one_le_K := ⋯, hat_le := ⋯, Q_le := ⋯ }

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.section13_plus_section10Bridge {H : Section13HatLayers} (hH : Section13HatSourceContract H) : Section13HatSection10Bridge H ErrorSign.plus

The positive sign has 2 + ε₊ = 3, so the corrected common bridge is literally the requested production Section13HatSection10Bridge.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.section13_plus_section10Bridge hH = { Qhat := (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.section13_bridgeAtThree hH MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus).Qhat, dde := have heq := MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.section13_plus_section10Bridge._proof_1; ⋯.mpr (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.section13_bridgeAtThree hH MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus).dde, K := (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.section13_bridgeAtThree hH MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.plus).K, one_le_K := ⋯, hat_le := ⋯, Q_le := ⋯ }

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.BridgeAssembly.production_minus_bridge_requires_early_scalar_dde {H : Section13HatLayers} (B : Section13HatSection10Bridge H ErrorSign.minus) (s : ℝ) : 2 < s → HasDerivAt B.Qhat (-(2 * B.Qhat s + B.Qhat (s - 1)) / s) s

Audit lemma exposing why the production record cannot be assembled for the negative sign from the stated source contract: it asks for the scalar Q̂ DDE already on s > 1, whereas section13Qhat_dde is available only on s > 3. This is an interface-strength mismatch, not a missing comparison or pairing.