Case-I successor geometry: the first non-automatic edge

This file audits the pointwise-in-D hypotheses of the uniform Case-I successor in their actual order. The moving source cutoff and both power cutoffs are automatic, uniformly in every Case-I coordinate s ≤ σ(D). The next strict source-domain inequality is not automatic at the legal odd boundary N = 3, s = 3; it is therefore frozen as the first genuine premise.

structure MathlibNt.SieveTheory.CaseIPreThresholdGeometryPacket (D : ℕ) (d s : ℝ) : Prop

The geometry available before the first strict source-domain premise.

• hD4 : 4 ≤ D
• hsigma : 1 < SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d
• hpowerSigma : 2 ≤ ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d)
• hpowerS : 2 ≤ ↑D ^ (1 / s)
• hpowerOrder : ↑D ^ (1 / SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d) ≤ ↑D ^ (1 / s)

theorem MathlibNt.SieveTheory.exists_caseI_preThreshold_geometry_packet (d : ℝ) (hd : 1 < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D _N : ℕ), D0 ≤ ↑D → ∀ (s : ℝ), 2 ≤ s → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → CaseIPreThresholdGeometryPacket D d s

A single cutoff depending only on d gives all geometry preceding the strict Section-13 threshold, uniformly in N and in every Case-I coordinate 2 ≤ s ≤ sourceSigma D d.

def MathlibNt.SieveTheory.CaseIStrictSourceThreshold (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N : ℕ) (s : ℝ) : Prop

The first premise not supplied by the global IH, parity domains, and the source contract. Naming it prevents a chain of pointwise implications from making the uniform successor vacuous.

Equations

• MathlibNt.SieveTheory.CaseIStrictSourceThreshold H N s = (H.betaHat + (MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth N).epsilon < s)

theorem MathlibNt.SieveTheory.odd_boundary_is_legal_caseI_coordinate : 3 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 3 ∧ 3 - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (3 - 1) ∧ 2 + (SwitchingPrinciple.SuzukiLemma144KappaOne.ErrorSign.ofDepth 3).epsilon ≤ 3

N=3, s=3 is a literal legal parity-boundary point, including the weak source lower bound used by the uniform Σ₁₂ theorem.

theorem MathlibNt.SieveTheory.odd_boundary_does_not_supply_strict_source_threshold {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) : ¬CaseIStrictSourceThreshold H 3 3

At that legal point every source contract has betaHat = 2, so the strict threshold demanded next by the successor is false. This is a theorem-level counterexample to deriving the threshold from the advertised inputs.

theorem MathlibNt.SieveTheory.odd_natCeil_cubic_condition_not_automatic : have z := ⌈↑2 ^ (1 / 3)⌉₊; ¬z ^ 3 ≤ 2

The subsequent odd cubic condition is independently non-automatic for a natural ceiling: at D=2, s=3, the ceiling is 2, whose cube exceeds D. Thus even strengthening the first strict edge would not justify silently manufacturing z^3 ≤ D from ceiling geometry.