PPTPrefixGrouping.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Finite maximal-prefix grouping in the full-fiber sieve. The injective choice is made on each residual family, after the maximal-prefix argument has proved the largest-prime mismatch for every nontrivial residual preimage.

def OAI.TotientAsymptotic.pptPrefixProduct line 18
lemma OAI.TotientAsymptotic.ppt_prefix_suffix_product line 20
lemma OAI.TotientAsymptotic.ppt_suffix_largest_prime line 24
def OAI.TotientAsymptotic.PPTBadResidual line 51
Source documentation
The elementary residual facts supplied by maximal-prefix selection. This is an internal grouping invariant, not a published-input assumption.
```
def PPTBadResidual (d r : ℕ) : Prop :=
…
```

theorem OAI.TotientAsymptotic.ppt_maximal_prefix_grouping line 60

Source documentation

Each failed rough prime product has a maximal prefix. All nontrivial preimages of its residual have a different largest prime.

theorem ppt_maximal_prefix_grouping {d N : ℕ} (hd : 0 < d)
    (S : Finset ℕ) (p : ℕ → ℕ → ℕ)
    (hrep : ∀ n ∈ S, n = pptSuffixProduct (p n) N 0)
    (hprime : ∀ n ∈ S, ∀ i < N, (p n i).Prime)
    (horder : ∀ n ∈ S, ∀ i k : ℕ, i < k → k < N → p n k < p n i)
    (hlarge : ∀ n ∈ S, ∀ i < N, d+1 < p n i)
    (hbad : ∀ n ∈ S, ¬FullFiber d n) :
    ∃ j : ℕ → ℕ, ∀ n ∈ S,
      j n < N ∧ 0 < pptPrefixProduct (p n) (j n) ∧
      n = pptPrefixProduct (p n) (j n)*pptSuffixProduct (p n) N (j n) ∧
      PPTBadResidual d (pptSuffixProduct (p n) N (j n)) := by
…

Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.pptSuffixProduct, OAI.TotientAsymptotic.FullFiber, OAI.TotientAsymptotic.pptPrefixProduct, OAI.TotientAsymptotic.PPTBadResidual

def OAI.TotientAsymptotic.pptPrefixCell line 111

lemma OAI.TotientAsymptotic.ppt_prefix_cell_residual_injective line 115

Source documentation

Fixing the removed prefix makes the residual map injective.

lemma ppt_prefix_cell_residual_injective (S : Finset ℕ) (j pref residual : ℕ → ℕ)
    (hfactor : ∀ n ∈ S, n = pref n*residual n) (J c : ℕ) :
    Set.InjOn residual (pptPrefixCell S j pref J c : Set ℕ) := by
…

Mentions: OAI.TotientAsymptotic.pptPrefixCell

lemma OAI.TotientAsymptotic.ppt_prefix_cell_residual_card line 123
theorem OAI.TotientAsymptotic.ppt_prefix_cell_bad_witness line 132
Source documentation
Apply the injective bad-witness choice only after the residual family is fixed. The largest-prime mismatch and the nonsingleton seed branch are both retained.
```
theorem ppt_prefix_cell_bad_witness {d q : ℕ} (hd : 0 < d)
    (hqpos : 0 < q) (hq : q.totient = d)
    (S : Finset ℕ) (j pref residual : ℕ → ℕ)
    (hbad : ∀ n ∈ S, PPTBadResidual d (residual n)) (J c : ℕ) :
    let R := (pptPrefixCell S j pref J c).image residual
…
```
Mentions: OAI.TotientAsymptotic.PPTBadResidual, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.pptPrefixCell
lemma OAI.TotientAsymptotic.ppt_prefix_cells_cover line 158
Source documentation
The actual chosen prefix index and prefix product cover the original family by finitely many residual cells.
```
lemma ppt_prefix_cells_cover (S : Finset ℕ) (j pref : ℕ → ℕ) (N : ℕ)
    (hindex : ∀ n ∈ S, j n < N) :
    S ⊆ (Finset.range N).biUnion (fun J =>
      (S.image pref).biUnion (fun c => pptPrefixCell S j pref J c)) := by
…
```
Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.pptPrefixCell

lemma OAI.TotientAsymptotic.ppt_prefix_group_count_le line 172

Source documentation

Counting the original failed candidates reduces to counting the distinct residuals in each fixed-prefix cell.

lemma ppt_prefix_group_count_le (S : Finset ℕ) (j pref residual : ℕ → ℕ) (N : ℕ)
    (hindex : ∀ n ∈ S, j n < N)
    (hfactor : ∀ n ∈ S, n = pref n*residual n) :
    (S.card : ℝ) ≤ ∑ J ∈ Finset.range N, ∑ c ∈ S.image pref,
      (((pptPrefixCell S j pref J c).image residual).card : ℝ) := by
…

Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.pptPrefixCell

def OAI.TotientAsymptotic.pptPrefixesAt line 187
Source documentation
Only prefixes selected at index J enter its reciprocal mass.
```
def pptPrefixesAt (S : Finset ℕ) (j pref : ℕ → ℕ) (J : ℕ) : Finset ℕ :=
…
```
lemma OAI.TotientAsymptotic.mem_pptPrefixesAt line 190
lemma OAI.TotientAsymptotic.ppt_prefix_cells_exact_cover line 201
lemma OAI.TotientAsymptotic.ppt_prefix_group_count_exact line 216
Source documentation
The exact-index partition preserves each prefix length before bounding its reciprocal totient mass. Residual injectivity is applied inside the fixed-prefix cell, as required by the bad-witness map.
```
lemma ppt_prefix_group_count_exact (S : Finset ℕ) (j pref residual : ℕ → ℕ) (N : ℕ)
    (hindex : ∀ n ∈ S, j n < N)
    (hfactor : ∀ n ∈ S, n = pref n*residual n) :
    (S.card : ℝ) ≤ ∑ J ∈ Finset.range N, ∑ c ∈ pptPrefixesAt S j pref J,
      (((pptPrefixCell S j pref J c).image residual).card : ℝ) := by
…
```
Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.pptPrefixesAt, OAI.TotientAsymptotic.pptPrefixCell