PPTActualResidual.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Actual residual data after choosing the terminal prefix and canceling matching coordinates. This keeps the candidate integer, both finite factor labels, and the exact shifted-product equation together.

def OAI.TotientAsymptotic.pptTailIndices line 17
def OAI.TotientAsymptotic.pptTailList line 20
lemma OAI.TotientAsymptotic.ppt_tail_list_product line 24
lemma OAI.TotientAsymptotic.ppt_tail_list_mem line 37

theorem OAI.TotientAsymptotic.ppt_actual_truncated_block line 47

Source documentation

The residual pair and both factor labels are built from the actual lists. The first prime survives cancellation, and the target size is divided by the totient of precisely the canceled product.

theorem ppt_actual_truncated_block {k l J d n E N : ℕ}
    (p : Fin k → ℕ) (q : Fin l → ℕ) (hJp : J ≤ k) (hJq : J ≤ l)
    (hJ : 0 < J) {W V z K : ℝ}
    (hp : ∀ i, IsNormalPrime W (p i)) (hq : ∀ i, IsNormalPrime W (q i))
    (hpa : StrictAnti p) (hqa : StrictAnti q)
    (hp3 : ∀ i, 3 ≤ p i) (hq3 : ∀ i, 3 ≤ q i)
    (hfirst : p ⟨0,hJ.trans_le hJp⟩ ≠ q ⟨0,hJ.trans_le hJq⟩)
    (hn : n = ∏ i, p i)
    (heq : d*shiftedProduct p = E*shiftedProduct q)
    (hE : 0 < E) (hV : 1 ≤ V) (hEV : (largestPrimeFactor E : ℝ) ≤ V)
    (hptail : ∀ i : Fin k, J ≤ i.val → (largestPrimeFactor (p i-1) : ℝ) ≤ V)
    (hqtail : ∀ i : Fin l, J ≤ i.val → (largestPrimeFactor (q i-1) : ℝ) ≤ V)
…

Mentions: OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.IsNormalPrime, OAI.TotientAsymptotic.shiftedProduct, OAI.TotientAsymptotic.largestPrimeFactor