def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13MajorantsFinal.MovingClaim146iiiConclusion (H : Section13HatLayers) (d Δ : ℝ) : Prop

Exact conclusion of the already-closed moving Claim 14.6(iii).

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13MajorantsFinal.MovingClaim146iiiConclusion H d Δ = ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → ∀ (sign : MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign) (s : ℝ), 2 + sign.epsilon ≤ s → s ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d → ∫ (t : ℝ) in s..MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d, MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.qD H sign.opposite D d Δ t < (1 - 1 / MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d) ^ (1 - Δ) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.lambda H sign D d 0 s

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13MajorantsFinal.bridge_Qhat_sign_independent {H : Section13HatLayers} (hH : Section13HatSourceContract H) : (BridgeAssembly.section13_bridgeAtThree hH ErrorSign.plus).Qhat = (BridgeAssembly.section13_bridgeAtThree hH ErrorSign.minus).Qhat

Semantic audit: both sign-indexed bridges use literally the same Qhat. There is no plus/minus choice of scalar solution at this interface.

noncomputable def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13MajorantsFinal.duplicateQhatMajorant {H : Section13HatLayers} (hH : Section13HatSourceContract H) (Q : CutoffCorrectedRatio.CutoffMajorant (section13Qhat H)) (sign : ErrorSign) : CutoffCorrectedRatio.CutoffMajorant (BridgeAssembly.section13_bridgeAtThree hH sign).Qhat

Consequently one honest Lemma-10.28 majorant supplies both sign-indexed arguments expected by the moving Claim-14.6 theorem.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13MajorantsFinal.duplicateQhatMajorant hH Q x✝ = Q

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13MajorantsFinal.moving_claim14_6_iii_of_singleQhatMajorant {H : Section13HatLayers} (hH : Section13HatSourceContract H) {d Δ : ℝ} (hd : 0 < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (Q : CutoffCorrectedRatio.CutoffMajorant (section13Qhat H)) : MovingClaim146iiiConclusion H d Δ

Exact thin assembly into the closed moving Claim 14.6(iii). This theorem is included only to expose the semantic wiring; constructing Q from compact initial data is the still-missing upstream Lemma-10.28 adapter.

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.Section13MajorantsFinal.QhatCompactInitialData (H : Section13HatLayers) : Type

Historical compact-input audit boundary. The endpoint-derivative blocker has been removed by the corrected Ioc first-crossing interface. This structure is retained only as a record of the former mismatch and is not used downstream.

• S : ℝ
• four_le_S : 4 ≤ self.S
• endpoint_dde : HasDerivAt (section13Qhat H) (-(2 * section13Qhat H 3 + section13Qhat H (3 - 1)) / 3) 3
• values : ↑(Set.Icc 3 self.S) → ℝ
• values_eq (u : ↑(Set.Icc 3 self.S)) : self.values u = section13Qhat H ↑u