WitnessCollision.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Exact comparison data extracted from two basic witnesses for colliding tuples.

def OAI.TotientAsymptotic.wholeWitnessPrime line 12
def OAI.TotientAsymptotic.witnessTuple line 15
lemma OAI.TotientAsymptotic.wholeWitness_shift_product line 18
lemma OAI.TotientAsymptotic.witness_tuple_value_at_cut line 35
Source documentation
Every valid cutoff gives the same integer value. No witness representative is discarded from the tail totient.
```
lemma witness_tuple_value_at_cut {x : ℝ} {H k : ℕ} {p : ℕ}
    {η : RemainderDatum (L x H)} (hη : IsBasicRemainder x H η)
    (hL : L x H < m x) (hR : R x H < L x H) (hk : k < L x H) :
    tupleValue (witnessTuple p η) = (suffixPreimage η k).totient *
      ∏ r ∈ Finset.Icc 0 k, (wholeWitnessPrime p η r-1) := by
…
```
Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.tupleValue, OAI.TotientAsymptotic.witnessTuple, OAI.TotientAsymptotic.suffixPreimage, OAI.TotientAsymptotic.wholeWitnessPrime

theorem OAI.TotientAsymptotic.witness_collision_cancel line 58

Source documentation

Cancel all matched primes up to the cutoff, including the common prefix. The first differing prime survives, and at most k-i+1 indices survive.

theorem witness_collision_cancel {x : ℝ} {H i k p q : ℕ}
    {η ξ : RemainderDatum (L x H)}
    (hη : IsBasicRemainder x H η) (hξ : IsBasicRemainder x H ξ)
    (hp : p.Prime) (hL : L x H < m x) (hR : R x H < L x H)
    (hk : k < L x H) (hik : i ≤ k)
    (hv : tupleValue (witnessTuple p η) = tupleValue (witnessTuple q ξ))
    (hfirst : wholeWitnessPrime p η i ≠ wholeWitnessPrime q ξ i)
    (hcommon : ∀ j < i, wholeWitnessPrime p η j = wholeWitnessPrime q ξ j) :
    let I := (Finset.Icc 0 k).filter (fun j => wholeWitnessPrime p η j ≠ wholeWitnessPrime q ξ j)
…

Mentions: OAI.TotientAsymptotic.RemainderDatum, OAI.TotientAsymptotic.L, OAI.TotientAsymptotic.IsBasicRemainder, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.tupleValue, OAI.TotientAsymptotic.witnessTuple, OAI.TotientAsymptotic.wholeWitnessPrime