@[reducible, inline]

abbrev MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceClaim146AssemblyNext.Lemma1028CutoffMajorant (R : ℝ → ℝ) : Type

The genuine upstream Lemma-10.28 output, with its honest eventual cutoff. It contains neither a delayed/current ratio nor any Claim-14.6 conclusion.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceClaim146AssemblyNext.Lemma1028CutoffMajorant R = Section10Lemma1028FirstCrossing.Section10CommonMajorant R

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceClaim146AssemblyNext.SourceCutoffLogDomination (K A d M : ℝ) : Prop

The elementary moving-cutoff comparison still needed between Lemma 10.28's log(es) gain and the perturbation logarithm. This is numerical: it mentions no hat function, DDE certificate, integral, or Claim 14.6 conclusion.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceClaim146AssemblyNext.SourceCutoffLogDomination K A d M = (0 < d ∧ ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → M ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ∧ ∀ (t : ℝ), M ≤ t → t ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d → 2 * (d + 1) * K ^ 2 * A * max 1 (Real.log (1 + t ^ d / Real.log D)) ≤ Real.log (Real.exp 1 * t))

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceClaim146AssemblyNext.Proposition131MovingDelayedCurrentRatioOnSource (H : Section13HatLayers) (sign : ErrorSign) (d M : ℝ) : Prop

Source-range-corrected form of the moving ratio. The older Proposition131MovingDelayedCurrentRatio accidentally quantifies over every t ≥ M at each fixed D, rather than M ≤ t ≤ sourceSigma D d.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceClaim146AssemblyNext.Proposition131MovingDelayedCurrentRatioOnSource H sign d M = (0 < d ∧ 1 < M ∧ ∃ (D₀ : ℝ), 1 < D₀ ∧ ∀ (D : ℝ), D₀ ≤ D → M ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d ∧ ∀ (t : ℝ), M ≤ t → t ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma D d → 2 * (d + 1) * max 1 (Real.log (1 + t ^ d / Real.log D)) * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.weightedHat H sign t ≤ t * H.T sign.opposite (t - 1))

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceClaim146AssemblyNext.unitShift_of_cutoffMajorant {R : ℝ → ℝ} {β s : ℝ} (hDDE : Section10DDEApparatus R β) (Q : Lemma1028CutoffMajorant R) (hβ : β ≤ 3) (hs : Q.cutoff ≤ s) : s * Real.log (Real.exp 1 * s) * R s ≤ Q.A * R (s - 1)

Cutoff-aware Lemma 10.29, derived directly from the honest Lemma-10.28 majorant. No adjacent-value estimate is assumed.

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceClaim146AssemblyNext.CrossSignCutoffTransport {H : Section13HatLayers} (hH : Section13HatSourceContract H) (d : ℝ) : Type

The exact additional bridge/numerical fact required to turn the cutoff majorant into the source-range ratio. It is kept visible rather than hidden in a fake "majorant": the current Section13HatSection10BridgeAtThree is sign-indexed and does not expose that its two instances share the same Qhat and comparison constant.

• sign : ErrorSign
• ratioOnSource : ∃ (M : ℝ), Proposition131MovingDelayedCurrentRatioOnSource H self.sign d M

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceClaim146AssemblyNext.movingCertificate_of_globalRatioExtension {H : Section13HatLayers} (hH : Section13HatSourceContract H) (sign : ErrorSign) {d : ℝ} (Q : Lemma1028CutoffMajorant (BridgeAssembly.section13_bridgeAtThree hH sign).Qhat) (hglobal : Proposition131MovingDelayedCurrentRatio H sign d Q.cutoff) : MovingDDEAsymptoticCertificate H sign d Q.cutoff

Exact adapter to the existing certificate theorem. The extra premise is displayed deliberately: it is precisely the erroneous global-in-t extension which cannot follow from a moving-source cutoff estimate.

structure MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.SourceClaim146AssemblyNext.RemainingClaim146iiiSourceInputs (H : Section13HatLayers) (d Δ gap M : ℝ) : Prop

Exact status ledger. The honest cutoff majorant closes the cutoff-aware unit shift. The current APIs still require (i) repair of the moving-ratio quantifier, (ii) filling the bounded interval below the Lemma-10.28 cutoff in Proposition 13.1(iii), and (iii) the independent Lemma-13.3 compact head. Consequently Claim 14.6(iii) cannot honestly be exported from hH + Q alone.

• ratioOnSource (sign : ErrorSign) : Proposition131MovingDelayedCurrentRatioOnSource H sign d M
• tailDecay : Proposition131TailDecayContract H
• perturbation : FixedCompactPerturbationContract d M
• weightedHead : Lemma133WeightedHeadContract H d Δ gap M