noncomputable def MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeffA0 (N : ℕ) (K : ℝ) : ℝ

The part of the algebraic endpoint coefficient which is independent of the source cutoff parameter σ. In particular it is fixed once N and K are fixed.

Equations

• MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeffA0 N K = 9 * K * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3

noncomputable def MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeffA1 (N : ℕ) (K : ℝ) : ℝ

The coefficient of σ in the algebraic endpoint coefficient. This is fixed once N and K are fixed.

Equations

• MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeffA1 N K = 18 * K ^ 2 * (1 + 3 * K) * MathlibNt.SieveTheory.SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2

noncomputable def MathlibNt.SieveTheory.caseIIQDEndpointCoeffA0 (_d Δ C K : ℝ) : ℝ

The coefficient left after removing the single factor σ from the cubic q_D(3) endpoint coefficient. (The argument d is retained to match the endpoint interface, although the explicit coefficient does not use it.)

Equations

• MathlibNt.SieveTheory.caseIIQDEndpointCoeffA0 _d Δ C K = 72 * K ^ 2 * (1 + 3 * K) * C * Real.exp √K * (3 / 2) ^ Δ

noncomputable def MathlibNt.SieveTheory.caseIIQDRelativeEndpointCoeffA0 (_d Δ _C K : ℝ) : ℝ

The cubic-q_D(3) coefficient after cancelling the already present common scale C * exp (sqrt K) * E. The factor 3 pays for E ≥ 1/3, so this relative coefficient is independent of C.

Equations

• MathlibNt.SieveTheory.caseIIQDRelativeEndpointCoeffA0 _d Δ _C K = 216 * K ^ 2 * (1 + 3 * K) * (3 / 2) ^ Δ

theorem MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeff_exact_sigma_split (N : ℕ) (σ K : ℝ) : 9 * K * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3 + 18 * K ^ 2 * σ * (1 + 3 * K) * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2 = caseIIAlgebraicEndpointCoeffA0 N K + σ * caseIIAlgebraicEndpointCoeffA1 N K

Exact a₀ + σ a₁ decomposition of the algebraic coefficient occurring in caseIIAlgebraicEndpointCoeff. The statement displays that coefficient rather than using its coarse name as a black box.

theorem MathlibNt.SieveTheory.caseIIQDEndpointCoeff_exact_sigma_split (d Δ σ C K : ℝ) : 72 * K ^ 2 * σ * (1 + 3 * K) * C * Real.exp √K * (3 / 2) ^ Δ = σ * caseIIQDEndpointCoeffA0 d Δ C K

Exact extraction of the single factor σ from the cubic q_D(3) endpoint coefficient.

theorem MathlibNt.SieveTheory.caseIIQDEndpointCoeffA0_le_commonScale_mul_relative (d Δ C K E : ℝ) (hC : 0 ≤ C) (hK : 0 ≤ K) (hE : 1 / 3 ≤ E) : caseIIQDEndpointCoeffA0 d Δ C K ≤ C * Real.exp √K * E * caseIIQDRelativeEndpointCoeffA0 d Δ C K

The raw cubic endpoint coefficient is paid by one (not two) copies of the common scale.

noncomputable def MathlibNt.SieveTheory.caseIISharpPositiveEndpointRelativeCoeff (N : ℕ) (D d Δ σ C K : ℝ) : ℝ

The fixed-coefficient relative endpoint expression. Its only dependence on the moving source cutoff is through the three displayed factors σ. Consequently a₀, a₁, and aq₀ can be frozen before an eventual argument.

Equations

• MathlibNt.SieveTheory.caseIISharpPositiveEndpointRelativeCoeff N D d Δ σ C K = MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeffA0 N K * Real.log D ^ (Δ - 1) + σ * MathlibNt.SieveTheory.caseIIAlgebraicEndpointCoeffA1 N K * Real.log D ^ (Δ - 1) + σ * MathlibNt.SieveTheory.caseIIQDRelativeEndpointCoeffA0 d Δ C K / Real.log D + 27 * K * Real.log D ^ (Δ - 1)

theorem MathlibNt.SieveTheory.caseIISharpPositiveEndpointRelativeCoeff_eq (N : ℕ) (D d Δ σ C K : ℝ) : caseIISharpPositiveEndpointRelativeCoeff N D d Δ σ C K = caseIIAlgebraicEndpointCoeffA0 N K * Real.log D ^ (Δ - 1) + σ * caseIIAlgebraicEndpointCoeffA1 N K * Real.log D ^ (Δ - 1) + σ * caseIIQDRelativeEndpointCoeffA0 d Δ C K / Real.log D + 27 * K * Real.log D ^ (Δ - 1)

Exact coefficient identity before inserting the error envelope.

theorem MathlibNt.SieveTheory.caseII_positiveEndpoint_packet_fixed_coefficients {N : ℕ} {D d Δ σ C K E L I B0 V lhs : ℝ} (hpacket : lhs ≤ B0 + V * (I + ((9 * K * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3 + 18 * K ^ 2 * σ * (1 + 3 * K) * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) * Real.log D ^ (Δ - 1) + 72 * K ^ 2 * σ * (1 + 3 * K) * C * Real.exp √K * (3 / 2) ^ Δ / Real.log D + 27 * K * Real.log D ^ (Δ - 1) * E) * L)) : lhs ≤ B0 + V * (I + (caseIIAlgebraicEndpointCoeffA0 N K * Real.log D ^ (Δ - 1) + σ * caseIIAlgebraicEndpointCoeffA1 N K * Real.log D ^ (Δ - 1) + σ * caseIIQDEndpointCoeffA0 d Δ C K / Real.log D + 27 * K * Real.log D ^ (Δ - 1) * E) * L)

Restatement of the positive endpoint packet with all σ-dependence exposed. Notice the position of E: the algebraic and cubic-q_D corrections do not carry E; only the sharp raw-base term does. This is the exact shape needed before any later common-envelope absorption.

The premise is the positive endpoint packet written with the two explicit production coefficients. The conclusion is definitionally the same packet, but with fixed coefficients a₀, a₁, and aq₀.

theorem MathlibNt.SieveTheory.caseII_positiveEndpoint_relative_packet_fixed_coefficients (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {N : ℕ} {D d Δ σ s C K I B0 V lhs : ℝ} (hpacket : lhs ≤ B0 + V * (I + ((9 * K * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3 + 18 * K ^ 2 * σ * (1 + 3 * K) * SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) * Real.log D ^ (Δ - 1) + 72 * K ^ 2 * σ * (1 + 3 * K) * C * Real.exp √K * (3 / 2) ^ Δ / Real.log D + 27 * K * Real.log D ^ (Δ - 1) * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s) * Real.log D ^ (-Δ))) : lhs ≤ B0 + V * (I + (caseIIAlgebraicEndpointCoeffA0 N K * Real.log D ^ (Δ - 1) + σ * caseIIAlgebraicEndpointCoeffA1 N K * Real.log D ^ (Δ - 1) + σ * caseIIQDEndpointCoeffA0 d Δ C K / Real.log D + 27 * K * Real.log D ^ (Δ - 1) * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N D d s) * Real.log D ^ (-Δ))

The same restatement specialized to the production normalization L = (log D)^(-Δ) and the production error envelope. This formulation makes its correct location manifest and is directly consumable by eventual bounds.