Lemma 14.4: source-faithful moving-domain finite-depth contract

The source producer is only asserted while the continuous coordinate lies below sourceSigma D d. Accordingly, every clause quantified over D and a coordinate carries the pointwise hypothesis

x ≤ sourceSigma (D : ℝ) d.

No theorem in this file promotes this moving-domain statement to the legacy all-coordinate contract Lemma144UniformNatCeilAt or to GlobalDepthLemma144InductionHypothesis.

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

The exact-power form of Lemma 14.4 on its source-native moving domain.

Equations

• MathlibNt.SieveTheory.Lemma144MovingDomainGlobalDepthAt S H C K d Δ N Dmin = ∀ (D z : ℕ), Dmin ≤ D → 2 ≤ D → 2 ≤ z → ∀ x ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N, x ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → ↑D ^ (1 / x) = ↑z → MathlibNt.SieveTheory.suzukiActualT S N D z ≤ MathlibNt.SieveTheory.SwitchingPrinciple.suzukiVProduct S ↑z * (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 ^ (-Δ))

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

Natural-ceiling form of the same moving-domain assertion. The common cutoff precedes D; the source endpoint is evaluated at that D.

Equations

• MathlibNt.SieveTheory.Lemma144MovingDomainNatCeilAt S H C K d Δ N Dmin = ∀ (D : ℕ), Dmin ≤ D → 2 ≤ D → ∀ x ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N, x ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → 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 ^ (-Δ))

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

Restriction of the natural-ceiling moving-domain contract to one side of a Case-I/Case-II partition.

Equations

• MathlibNt.SieveTheory.Lemma144MovingDomainNatCeilRestrictedAt S H C K d Δ N Dmin Q = ∀ (D : ℕ), Dmin ≤ D → 2 ≤ D → ∀ x ∈ MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N, x ≤ MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → Q x → 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.lemma144MovingDomainGlobalDepthAt_mono_cutoff {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {C K d Δ : ℝ} {N Dmin Dmin' : ℕ} (hcut : Dmin ≤ Dmin') (h : Lemma144MovingDomainGlobalDepthAt S H C K d Δ N Dmin) : Lemma144MovingDomainGlobalDepthAt S H C K d Δ N Dmin'

Raising the common cutoff preserves the source-faithful exact-power contract.

theorem MathlibNt.SieveTheory.lemma144MovingDomainGlobalDepthAt_of_natCeil (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (N Dmin : ℕ) (hceil : Lemma144MovingDomainNatCeilAt S H C K d Δ N Dmin) : Lemma144MovingDomainGlobalDepthAt S H C K d Δ N Dmin

The natural ceiling gives the exact-power form without changing the moving coordinate domain.

theorem MathlibNt.SieveTheory.lemma144MovingDomainNatCeilAt_of_restricted_cases {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {C K d Δ : ℝ} {N DI DII : ℕ} {QI QII : ℝ → Prop} (hcover : ∀ x ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 N, QI x ∨ QII x) (hI : Lemma144MovingDomainNatCeilRestrictedAt S H C K d Δ N DI QI) (hII : Lemma144MovingDomainNatCeilRestrictedAt S H C K d Δ N DII QII) : Lemma144MovingDomainNatCeilAt S H C K d Δ N (max DI DII)

Case-I and Case-II packets combine pointwise at one cutoff. The moving source-domain premise is retained in both branches.

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

Source-faithful finite-depth induction. Each successor consumes only the moving-domain predecessor assertion, not the legacy all-coordinate global IH.

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

The Case-II successor packet at the quantifier order consumed by the moving-domain finite-depth assembler.

Equations

• MathlibNt.SieveTheory.Lemma144MovingDomainCaseIIHCase S H C K d Δ depth = ∀ (N Dmin : ℕ), 1 ≤ N → N < depth → 2 ≤ Dmin → MathlibNt.SieveTheory.Lemma144MovingDomainGlobalDepthAt S H C K d Δ N Dmin → ∃ (DII : ℕ), Dmin ≤ DII ∧ MathlibNt.SieveTheory.Lemma144MovingDomainNatCeilRestrictedAt S H C K d Δ (N + 1) DII (MathlibNt.SieveTheory.Lemma144CaseIIFinalSide (N + 1))

theorem MathlibNt.SieveTheory.lemma14_4_movingDomain_full_finiteDepth (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (C K d Δ : ℝ) (depth : ℕ) (hbase : ∃ (Dmin : ℕ), 2 ≤ Dmin ∧ Lemma144MovingDomainNatCeilAt S H C K d Δ 1 Dmin) (hcaseI : ∀ (N Dmin : ℕ), 1 ≤ N → N < depth → 2 ≤ Dmin → Lemma144MovingDomainGlobalDepthAt S H C K d Δ N Dmin → ∃ (DI : ℕ), Dmin ≤ DI ∧ Lemma144MovingDomainNatCeilRestrictedAt S H C K d Δ (N + 1) DI fun (x : ℝ) => ¬Lemma144CaseIIFinalSide (N + 1) x) (hcaseII : Lemma144MovingDomainCaseIIHCase S H C K d Δ depth) : ∃ (Dmin : ℕ), 2 ≤ Dmin ∧ ∀ (N : ℕ), 1 ≤ N → N ≤ depth → Lemma144MovingDomainGlobalDepthAt S H C K d Δ N Dmin

Total finite-depth assembly using the exact Case-II moving-domain packet. Case I is the logical complement of the odd low strip.