Case-I endpoint consumer under the source parameter packet

This endpoint consumer discharges the literal (14.23) scalar with the sharpened uniform theorem. Its assumptions are exactly Suzuki's source packet, rather than the stronger artificial condition 7 / (1 - (Δ + 2 / Θ)) < d.

theorem MathlibNt.SieveTheory.exists_caseI1423EndpointSourceBounds_sourceLargeLog_uniform_of_source (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) {d Δ Θ : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatSourceContract H) (hsrc : SuzukiClaim145SourceParameters d Δ Θ) : ∃ (C1min : ℝ), 1 ≤ C1min ∧ ∀ (C1 C K : ℝ), C1min ≤ C1 → 0 < C → 2 ≤ K → ∃ (A11 : ℝ) (A12 : ℝ), 0 ≤ A11 ∧ 0 ≤ A12 ∧ ∀ (N D : ℕ) (s : ℝ), 3 ≤ D → C1 * K ^ Θ < Real.log ↑D → 2 ≤ N → 2 ≤ s → s - 1 ∈ SuzukiFiniteContinuousLayers.KappaOneModel.parityDomain 2 (N - 1) → s ≤ SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d → have σ := SwitchingPrinciple.SuzukiLemma144KappaOne.sourceSigma (↑D) d; have z := ⌈↑D ^ (1 / s)⌉₊; have B := sigma12InheritedBudget S H N D z C K d Δ s; caseI1423Sigma11Endpoint S N D z K s σ ≤ A11 * caseI1423RemainderUnit B (↑D) σ ∧ caseI1423Sigma12Endpoint S H N D z C K d Δ s σ ≤ A12 * caseI1423RemainderUnit B (↑D) σ

Source-large-log endpoint bounds with the cutoff before C, K, depth, and coordinate, under exactly the source parameter packet.