Documentation

MathlibNt.SieveTheory.LinearSieve.Suzuki.SuzukiMovingClaim146ToCaseIIFinal

source
def MathlibNt.SieveTheory.MovingClaim14_6iiiAtSource (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (d Δ : ℝ) :
Prop

Exact conclusion exported by the moving Claim 14.6(iii) assembly. Keeping this conclusion as a named interface lets this consumer compile even when the large upstream cutoff-majorant module has not yet been installed as an import.

Equations
Instances For
    Inspect dependencies

    MathlibNt.SieveTheory.MovingClaim14_6iiiAtSource · compiled type and proof/definition references.

    source
    def MathlibNt.SieveTheory.MovingCaseIIRelativeAssembler (Tdisc : ℕ → ℝ → ℝ → ℝ) (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (B₀ : ℕ → ℕ → ℝ) (d Δ C K : ℝ) :
    Prop

    The genuine discrete Case-II assembly boundary. Its conclusion is the relative-bracket estimate, not the downstream Claim-14.5 bound. Both cutoffs are the literal natural ceilings used by the production endpoint.

    Equations
    Instances For
      Inspect dependencies

      MathlibNt.SieveTheory.MovingCaseIIRelativeAssembler · compiled type and proof/definition references.

      source
      def MathlibNt.SieveTheory.MovingCaseIINormalization (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (B₀ : ℕ → ℕ → ℝ) (d Δ σ K C C145 : ℝ) :
      Prop

      The remaining normalization from the source recurrence to the published Claim-14.5 scale. This is a coefficient comparison, rather than Claim 14.5 itself, and therefore does not assume the downstream conclusion.

      Equations
      Instances For
        Inspect dependencies

        MathlibNt.SieveTheory.MovingCaseIINormalization · compiled type and proof/definition references.

        source
        def MathlibNt.SieveTheory.Claim14_5NatEventualAt (Tdisc : ℕ → ℝ → ℝ → ℝ) (S : BoundingSieve) (H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers) (N : ℕ) (d Δ σ K s C145 : ℝ) :
        Prop

        Natural-parameter version of the publication conclusion. Unlike the real-parameter convenience wrapper in SuzukiClaim145CaseSplitFinal, this form retains the literal natural parameter consumed by the rounded endpoint.

        Equations
        Instances For
          Inspect dependencies

          MathlibNt.SieveTheory.Claim14_5NatEventualAt · compiled type and proof/definition references.

          source
          theorem MathlibNt.SieveTheory.claim14_5_caseII_natEventual_of_movingClaim146 {Tdisc : ℕ → ℝ → ℝ → ℝ} {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {B₀ : ℕ → ℕ → ℝ} {N : ℕ} {d Δ σ K C C145 s : ℝ} (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) (hN : Odd N) (hd1 : 1 < d) (hd : 7 / (1 - Δ) < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hs1 : 1 < s) (hs3 : s ≤ 3) (hC : 0 ≤ C) (hK : 0 ≤ K) (hF0 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) (hF1 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) (hscaleNonneg : ∀ (D : ℕ), 0 ≤ C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ)) (hcert : SwitchingPrinciple.SuzukiLemma144KappaOne.MovingClaim14_6TailCertificate H 2 d Δ) (hmovingIII : MovingClaim14_6iiiAtSource H d Δ) (hassemble : MovingCaseIIRelativeAssembler Tdisc S H B₀ d Δ C K) (hnormalize : MovingCaseIINormalization S H B₀ d Δ σ K C C145) :
          Claim14_5NatEventualAt Tdisc S H N d Δ σ K s C145

          Moving Claims 14.6(i)--(iii), the source relative bracket, and exact natural-ceiling geometry close the Case-II branch. All thresholds are merged before the natural parameter D is introduced.

          Inspect dependencies

          MathlibNt.SieveTheory.claim14_5_caseII_natEventual_of_movingClaim146 · compiled type and proof/definition references.

          source
          theorem MathlibNt.SieveTheory.claim14_5_natEventual_exact_case_split_with_movingClaim146_caseII {Tdisc : ℕ → ℝ → ℝ → ℝ} {S : BoundingSieve} {H : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatLayers} {B₀ : ℕ → ℕ → ℝ} {N : ℕ} {d Δ σ K C C145 D C1 ΘK s : ℝ} (hdom : s ∈ SuzukiFiniteContinuousLayers.suzukiParityDomainOne 2 N) (hsσ : s ≤ σ) (hlarge : C1 * K ^ ΘK < Real.log D) (hH : SwitchingPrinciple.SuzukiLemma144KappaOne.Section13HatContract H 2) (hd1 : 1 < d) (hd : 7 / (1 - Δ) < d) (hΔ0 : 0 < Δ) (hΔ1 : Δ < 1) (hC : 0 ≤ C) (hK : 0 ≤ K) (hF0 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 N 3) (hF1 : 0 ≤ SuzukiFiniteContinuousLayers.finiteSourceLayer 1 2 (N - 1) 2) (hscaleNonneg : ∀ (D : ℕ), 0 ≤ C * Real.exp √K * SwitchingPrinciple.SuzukiLemma144KappaOne.errorEnvelope H N (↑D) d s * Real.log ↑D ^ (-Δ)) (hcert : SwitchingPrinciple.SuzukiLemma144KappaOne.MovingClaim14_6TailCertificate H 2 d Δ) (hmovingIII : MovingClaim14_6iiiAtSource H d Δ) (hassemble : MovingCaseIIRelativeAssembler Tdisc S H B₀ d Δ C K) (hnormalize : MovingCaseIINormalization S H B₀ d Δ σ K C C145) (hI : 2 + ↑(N % 2) ≤ s → s ≤ σ → Claim14_5NatEventualAt Tdisc S H N d Δ σ K s C145) :
          Claim14_5NatEventualAt Tdisc S H N d Δ σ K s C145

          Exact Case-I/Case-II split with a natural rounded cutoff. The branch is the same tagged split exported by SuzukiClaim145CaseSplitFinal; Case II is supplied by the moving Claim-14.6 closure above, while Case I remains its independent producer.

          Inspect dependencies

          MathlibNt.SieveTheory.claim14_5_natEventual_exact_case_split_with_movingClaim146_caseII · compiled type and proof/definition references.