Lemma 14.4: finite-depth global-IH assembly

The induction invariant below is the production GlobalDepthLemma144InductionHypothesis, specialized to the actual discrete quantity, Euler product, and Section-13 error envelope. Thus one cutoff is uniform in D, z, and every legal parity coordinate. No abstract error function is introduced.

def MathlibNt.SieveTheory.Lemma144GlobalDepthAt (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (N Dmin : ℕ) : Prop

The concrete global Lemma-14.4 assertion at one depth and one cutoff.

Equations

• MathlibNt.SieveTheory.Lemma144GlobalDepthAt S H C K d Δ N Dmin = MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.GlobalDepthLemma144InductionHypothesis (MathlibNt.SieveTheory.suzukiActualT S) (fun (z : ℕ) => MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z) (fun (n D : ℕ) (x : ℝ) => MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H n (↑D) d x) 2 C K Δ N Dmin

def MathlibNt.SieveTheory.Lemma144UniformNatCeilAt (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (N Dmin : ℕ) : Prop

The concrete natural-ceiling form of Lemma 14.4 with one cutoff placed before D and the parity coordinate.

Equations

• MathlibNt.SieveTheory.Lemma144UniformNatCeilAt S H C K d Δ N Dmin = ∀ (D : ℕ), Dmin ≤ D → 2 ≤ D → ∀ x ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N, 2 ≤ ⌈↑D ^ (1 / x)⌉₊ → MathlibNt.SieveTheory.suzukiActualT S N D ⌈↑D ^ (1 / x)⌉₊ ≤ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / x)⌉₊ * (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N x + C * Real.exp √K * MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d x * Real.log ↑D ^ (-Δ))

theorem MathlibNt.SieveTheory.lemma144GlobalDepthAt_mono_cutoff {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {C K d Δ : ℝ} {N Dmin Dmin' : ℕ} (hcut : Dmin ≤ Dmin') (h : Lemma144GlobalDepthAt S H C K d Δ N Dmin) : Lemma144GlobalDepthAt S H C K d Δ N Dmin'

Raising the common cutoff preserves the concrete global induction hypothesis.

theorem MathlibNt.SieveTheory.lemma144GlobalDepthAt_of_uniform_natCeil (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (N Dmin : ℕ) (hceil : Lemma144UniformNatCeilAt S H C K d Δ N Dmin) : Lemma144GlobalDepthAt S H C K d Δ N Dmin

A natural-ceiling estimate with all quantifiers behind one cutoff implies production's exact-power global IH. The exact-power hypothesis identifies its natural ceiling with z; this is the bridge needed by the successor theorem's global IH rather than a pointwise surrogate.

theorem MathlibNt.SieveTheory.lemma14_4_finiteDepth_induction_final (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (depth : ℕ) (hbase : ∃ (Dmin : ℕ), 2 ≤ Dmin ∧ Lemma144UniformNatCeilAt S H C K d Δ 1 Dmin) (hsuccessor : ∀ (N Dmin : ℕ), 1 ≤ N → N < depth → 2 ≤ Dmin → Lemma144GlobalDepthAt S H C K d Δ N Dmin → ∃ (Dnext : ℕ), Dmin ≤ Dnext ∧ Lemma144UniformNatCeilAt S H C K d Δ (N + 1) Dnext) : ∃ (Dmin : ℕ), 2 ≤ Dmin ∧ ∀ (N : ℕ), 1 ≤ N → N ≤ depth → Lemma144GlobalDepthAt S H C K d Δ N Dmin

Complete finite-depth induction assembler for the concrete Lemma-14.4 invariant.

The successor consumes the genuine global depth-N IH at the current common cutoff and returns the depth-N+1 assertion at a (possibly larger) cutoff. Because the new cutoff is required to dominate the old one, all earlier depths are transported to it. The conclusion therefore has one cutoff before the quantifiers over depth, D, z, and the parity coordinate.