def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.GlobalDepthLemma144InductionHypothesis (T : ℕ → ℕ → ℕ → ℝ) (V : ℕ → ℝ) (E : ℕ → ℕ → ℝ → ℝ) (β C K Δ : ℝ) (n Dmin : ℕ) : Prop

The genuine global depth-n form of the Lemma 14.4 induction hypothesis. It is uniform in the natural cutoff D', the sieve endpoint z', and every legal parity coordinate. The endpoint is tied to the coordinate by the source power relation; Dmin records the large-parameter threshold.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.GlobalDepthLemma144InductionHypothesis T V E β C K Δ n Dmin = ∀ (D' z' : ℕ), Dmin ≤ D' → 2 ≤ D' → 2 ≤ z' → ∀ x ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β n, ↑D' ^ (1 / x) = ↑z' → T n D' z' ≤ V z' * (MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β n x + C * Real.exp √K * E n D' x * Real.log ↑D' ^ (-Δ))

def MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry (support : Finset ℕ) (D Dmin : ℕ) (σ τ : ℝ) : Prop

The earliest outer-geometry edge not supplied by the current (14.10) carrier API. It is deliberately frozen separately: this is exactly what is needed to retain a prescribed global-IH cutoff after division by every carrier prime, and is not itself an induction hypothesis or endpoint estimate.

Equations

• MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.CarrierQuotientThresholdGeometry support D Dmin σ τ = ∀ p ∈ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.sigmaOneCarrier support D σ τ, Dmin * p ≤ D

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.ceilDiv_ge_threshold_of_scale {D p Dmin : ℕ} (hp : 0 < p) (hscale : Dmin * p ≤ D) : Dmin ≤ D ⌈/⌉ p

A quotient-scale lower bound simultaneously verifies the induction threshold and that the natural recursive cutoff is at least two.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.recursiveCoordinate_power_identity {D p : ℕ} (hp : 2 ≤ p) (hq : 2 ≤ D ⌈/⌉ p) : ↑(D ⌈/⌉ p) ^ (1 / recursiveCoordinate D p) = ↑p

The recursive logarithmic coordinate really parametrizes the natural endpoint p by a real power. Thus it is admissible for the global IH rather than merely an unrelated pointwise coordinate.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.parityDomain_mono {β : ℝ} {n : ℕ} {x y : ℝ} (hx : x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β n) (hxy : x ≤ y) : y ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β n

Suzuki's parity domains are upward closed.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144Equation1410.pointwiseInductionContract_of_globalDepthIH (support : Finset ℕ) (T : ℕ → ℕ → ℕ → ℝ) (V : ℕ → ℝ) (E : ℕ → ℕ → ℝ → ℝ) (β C K Δ : ℝ) (N D Dmin : ℕ) (σ τ : ℝ) (hDmin : 2 ≤ Dmin) (hprime : ∀ p ∈ support, Nat.Prime p) (hscale : CarrierQuotientThresholdGeometry support D Dmin σ τ) (hinherited : ∀ p ∈ sigmaOneCarrier support D σ τ, inheritedCoordinate D p ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain β (N - 1)) (hV : ∀ p ∈ sigmaOneCarrier support D σ τ, 0 ≤ V p) (hC : 0 ≤ C) (hSource : ∀ p ∈ sigmaOneCarrier support D σ τ, SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (recursiveCoordinate D p) ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 β (N - 1) (inheritedCoordinate D p)) (hError : ∀ p ∈ sigmaOneCarrier support D σ τ, E (N - 1) (D ⌈/⌉ p) (recursiveCoordinate D p) ≤ E (N - 1) (D ⌈/⌉ p) (inheritedCoordinate D p)) (hglobal : GlobalDepthLemma144InductionHypothesis T V E β C K Δ (N - 1) Dmin) : PointwiseInductionContract support T V E β C K Δ N D σ τ

Internalize the global Lemma-14.4 induction hypothesis at every carrier point of (14.10).

hscale is the exact remaining outer geometry: it says that every carrier prime leaves a quotient above the global induction threshold. From it we prove both ⌈D/p⌉ ≥ Dmin ≥ 2 and 2p ≤ D. The recursive coordinate is then proved to lie in I_{N-1} (rather than assumed there), and its power-coordinate identity is checked before the global IH is instantiated. No pointwise induction contract is an input.