Lemma 14.4: actual-type, all-depth, no-Dmin induction

This module contains only logical assembly over production objects. Claim 14.5 is consumed as ActualClaim145BoundAt, its normalization is the concrete ActualClaim145BoundAt.to_lemma144_moving_of_scalar, and the induction invariant is Lemma144MovingDomainNatCeilAt ... N 2. No abstract quantitative-complement predicate is introduced.

theorem MathlibNt.SieveTheory.natCeil_rpow_le_self_on_parityDomain {N D : ℕ} {s : ℝ} (hD : 2 ≤ D) (hs : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N) : ⌈↑D ^ (1 / s)⌉₊ ≤ D

On the production parity domain the natural power ceiling never exceeds D. This is the endpoint-order premise of the actual Claim-14.5 bridge.

theorem MathlibNt.SieveTheory.actualClaim145_to_moving_at_common_constant (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {C C145 K d Δ s : ℝ} {N D : ℕ} (hC145 : 0 ≤ C145) (hd : 0 < d) (hCnorm : claim145UniformNormalizationConstant C145 d ≤ C) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hD : 2 ≤ D) (hs : s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N) (hclaim : ActualClaim145BoundAt S H N D d Δ K s C145) : suzukiActualT S N D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ))

The actual Claim-14.5 regime gives the moving Lemma-14.4 target at any positive common constant dominating the explicit normalization constant.

theorem MathlibNt.SieveTheory.lemma14_4_noDmin_base_one_of_actualClaim145 (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {C C145 K d Δ C1 Θ : ℝ} {Dbase : ℕ} (hC145 : 0 ≤ C145) (hd : 0 < d) (hCnorm : claim145UniformNormalizationConstant C145 d ≤ C) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (_hK : 2 ≤ K) (_hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hDbase : 2 ≤ Dbase) (hbase : Lemma144MovingDomainNatCeilAt S H C K d Δ 1 Dbase) (hbudget : Real.log ↑Dbase ≤ C1 * K ^ Θ) (hclaim : ∀ (N D : ℕ) (s : ℝ), 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → ActualClaim145BoundAt S H N D d Δ K s C145) (hcaseIIBase : ∀ (D : ℕ) (s : ℝ), 2 ≤ D → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 1 → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → ¬2 ≤ s → suzukiActualT S 1 D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 1 s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H 1 (↑D) d s * Real.log ↑D ^ (-Δ))) : Lemma144MovingDomainNatCeilAt S H C K d Δ 1 2

Base N=1: Claim 14.5 closes its literal source disjunction, while on the complement its logarithmic inequality pays the one production base cutoff. Thus the resulting invariant has cutoff exactly 2, not an existential Dmin.

theorem MathlibNt.SieveTheory.lemma14_4_noDmin_successor_of_actual_cases (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {C C145 K d Δ C1 Θ : ℝ} (N : ℕ) (hC145 : 0 ≤ C145) (hd : 0 < d) (hCnorm : claim145UniformNormalizationConstant C145 d ≤ C) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (_hK : 2 ≤ K) (_hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hpred : Lemma144MovingDomainNatCeilAt S H C K d Δ N 2) (hclaim : ∀ (D : ℕ) (s : ℝ), 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → ActualClaim145BoundAt S H (N + 1) D d Δ K s C145) (hcaseI : ∀ (D : ℕ) (s : ℝ), 2 ≤ D → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N + 1) → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → ¬(Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s) → ¬Lemma144CaseIIFinalSide (N + 1) s → Lemma144MovingDomainGlobalDepthAt S H C K d Δ N 2 → suzukiActualT S (N + 1) D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N + 1) s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N + 1) (↑D) d s * Real.log ↑D ^ (-Δ))) (hcaseII : ∀ (D : ℕ) (s : ℝ), 2 ≤ D → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N + 1) → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → Lemma144CaseIIFinalSide (N + 1) s → Lemma144MovingDomainGlobalDepthAt S H C K d Δ N 2 → suzukiActualT S (N + 1) D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N + 1) s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N + 1) (↑D) d s * Real.log ↑D ^ (-Δ))) : Lemma144MovingDomainNatCeilAt S H C K d Δ (N + 1) 2

Narrow successor bridge for the forthcoming K-uniform Case-I/II producers. Its assumptions are their literal production output types at the single point (N+1,D,s); the predecessor is the actual moving exact-power contract at cutoff 2.

theorem MathlibNt.SieveTheory.lemma14_4_noDmin_allDepth_induction (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (hbase : Lemma144MovingDomainNatCeilAt S H C K d Δ 1 2) (hsucc : ∀ (N : ℕ), 1 ≤ N → Lemma144MovingDomainNatCeilAt S H C K d Δ N 2 → Lemma144MovingDomainNatCeilAt S H C K d Δ (N + 1) 2) (N : ℕ) : 1 ≤ N → Lemma144MovingDomainNatCeilAt S H C K d Δ N 2

Pure all-depth induction glue. There is no depth bound and no cutoff in the conclusion. The successor argument is intended to be instantiated by the preceding actual Case-I/II bridge once their K-uniform producers land.

theorem MathlibNt.SieveTheory.lemma14_4_noDmin_allDepth_of_actualClaim145_and_cases (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {C C145 K d Δ C1 Θ : ℝ} (hC145 : 0 ≤ C145) (hd : 0 < d) (hCnorm : claim145UniformNormalizationConstant C145 d ≤ C) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hK : 2 ≤ K) (hlocal : SwitchingPrinciple.HasDimensionOneLocalProductBound S K) (hbase : Lemma144MovingDomainNatCeilAt S H C K d Δ 1 2) (hclaim : ∀ (N D : ℕ) (s : ℝ), 1 ≤ N → 2 ≤ D → 2 ≤ s → Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s → ActualClaim145BoundAt S H N D d Δ K s C145) (hcaseI : ∀ (N D : ℕ) (s : ℝ), 1 ≤ N → 2 ≤ D → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N + 1) → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → ¬(Real.log ↑D ≤ C1 * K ^ Θ ∨ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d ≤ s) → ¬Lemma144CaseIIFinalSide (N + 1) s → Lemma144MovingDomainGlobalDepthAt S H C K d Δ N 2 → suzukiActualT S (N + 1) D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N + 1) s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N + 1) (↑D) d s * Real.log ↑D ^ (-Δ))) (hcaseII : ∀ (N D : ℕ) (s : ℝ), 1 ≤ N → 2 ≤ D → s ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N + 1) → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 2 ≤ ⌈↑D ^ (1 / s)⌉₊ → Lemma144CaseIIFinalSide (N + 1) s → Lemma144MovingDomainGlobalDepthAt S H C K d Δ N 2 → suzukiActualT S (N + 1) D ⌈↑D ^ (1 / s)⌉₊ ≤ SwitchingPrinciple.suzukiVProduct S ↑⌈↑D ^ (1 / s)⌉₊ * (SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N + 1) s + C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H (N + 1) (↑D) d s * Real.log ↑D ^ (-Δ))) (N : ℕ) : 1 ≤ N → Lemma144MovingDomainNatCeilAt S H C K d Δ N 2

All-depth no-Dmin assembler with the real Claim-14.5 and moving-domain types exposed at the headline. The only unfilled inputs are the forthcoming pointwise outputs of the K-uniform Case-I and Case-II producers; they are not collapsed into an abstract complement predicate.