theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_sourceSigma_three_threshold (d : ℝ) (hd : 0 < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → 3 ≤ sourceSigma D d

An explicit threshold beyond which the source cutoff is at least three.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma_rpow_le_cubeRoot {D d : ℝ} (hD : 1 ≤ D) (hσ : 3 ≤ sourceSigma D d) : D ^ (1 / sourceSigma D d) ≤ D ^ (1 / 3)

Once σ ≥ 3, increasing the denominator of the exponent decreases the power of a base at least one.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_two_le_rpow_inv_sourceSigma_threshold (d : ℝ) (hd : 1 < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → 2 ≤ D ^ (1 / sourceSigma D d)

Explicit eventual lower bound 2 ≤ D^(1/σ(D)). The assumption 1 < d is essential to this proof: log D / σ(D) then grows like a positive power of log D divided by log log D.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_sourceSigma_geometry_threshold (d : ℝ) (hd : 1 < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D : ℝ), D0 ≤ D → 3 ≤ sourceSigma D d ∧ D ^ (1 / sourceSigma D d) ≤ D ^ (1 / 3) ∧ 2 ≤ D ^ (1 / sourceSigma D d)

The three moving geometric size premises share one explicit threshold.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.cubeRoot_le_of_nat_cubic_upper {D y : ℕ} (hyUpper : D ≤ y ^ 3) : ↑D ^ (1 / 3) ≤ ↑y

A natural cubic cutoff gives the required upper real cube-root inequality; it does not give equality unless D is a perfect cube.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.nat_pred_lt_cubeRoot_of_cubic_lower {D y : ℕ} (hyLower : (y - 1) ^ 3 < D) : ↑(y - 1) < ↑D ^ (1 / 3)

The strict lower cubic bracket places the predecessor below the real cube root.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.two_le_nat_cutoff_of_cubic_upper {D y : ℕ} (hD8 : 8 ≤ D) (hyUpper : D ≤ y ^ 3) : 2 ≤ y

A cubic upper bracket and D ≥ 8 force the natural cutoff to be at least two.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.nat_cutoff_le_half_of_cubic_lower {D y : ℕ} (hD8 : 8 ≤ D) (hyLower : (y - 1) ^ 3 < D) (hyUpper : D ≤ y ^ 3) : ↑y ≤ ↑D / 2

The natural bracket also yields the real y ≤ D/2 premise for D ≥ 8.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.nat_cubic_cutoff_real_geometry {D y : ℕ} (hD8 : 8 ≤ D) (hyLower : (y - 1) ^ 3 < D) (hyUpper : D ≤ y ^ 3) : ↑(y - 1) < ↑D ^ (1 / 3) ∧ ↑D ^ (1 / 3) ≤ ↑y ∧ 2 ≤ ↑y ∧ ↑y ≤ ↑D / 2

All real inequalities genuinely supplied by the natural cubic bracket. The casts are explicit, so this packet cannot be confused with a real-valued choice of y or with ⌈D^(1/3)⌉₊.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.exists_sourceSigma_and_nat_cubic_geometry_threshold (d : ℝ) (hd : 1 < d) : ∃ (D0 : ℝ), 1 < D0 ∧ ∀ (D y : ℕ), D0 ≤ ↑D → (y - 1) ^ 3 < D → D ≤ y ^ 3 → 3 ≤ sourceSigma (↑D) d ∧ ↑D ^ (1 / sourceSigma (↑D) d) ≤ ↑D ^ (1 / 3) ∧ 2 ≤ ↑D ^ (1 / sourceSigma (↑D) d) ∧ ↑(y - 1) < ↑D ^ (1 / 3) ∧ ↑D ^ (1 / 3) ≤ ↑y ∧ 2 ≤ ↑y ∧ ↑y ≤ ↑D / 2

One common eventual threshold supplies the source-σ geometry and all valid consequences of a natural cubic cutoff.

theorem MathlibNt.SieveTheory.SwitchingPrinciple.SuzukiLemma144KappaOne.nat_cubic_bracket_does_not_force_cubeRoot_eq : ∃ (D : ℕ) (y : ℕ), (y - 1) ^ 3 < D ∧ D ≤ y ^ 3 ∧ ↑D ^ (1 / 3) ≠ ↑y

Adversarial audit: the natural cubic bracket does not imply the exact identity D^(1/3)=y demanded by the current raw Case-II theorem. The pair D=2, y=2 is already a counterexample.