CandidateCollisionGeometry.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

A repeated rational root forces a prescribed third endpoint coefficient

theorem OAI.JointDickman.equal_candidate_roots_denominator line 11
theorem OAI.JointDickman.equal_candidate_roots_values line 24
theorem OAI.JointDickman.distinct_ordered_pairs_third line 42

theorem OAI.JointDickman.coincident_candidate_has_third_coefficient line 61

Source documentation

Any duplicate root at another pair makes a large, prescribed integer available at an endpoint outside the first pair.

theorem coincident_candidate_has_third_coefficient {B L T H M : ℕ} {τ C : ℝ}
    {S : Fin M → Finset ℕ} {e f : BlockCandidateIndex M}
    (he : e ∈ blockCandidates B L T H M τ C S)
    (hf : f ∈ blockCandidates B L T H M τ C S)
    (hp : e.1 ≠ f.1) (hr : blockCandidateRoot e = blockCandidateRoot f) :
    ∃ s : Fin M, s ≠ e.1.1 ∧ s ≠ e.1.2 ∧
      PrimeProductAvailable (candidateSiteValue e s).natAbs (S s) ∧
      T*candidateQuotient e ≤ (candidateSiteValue e s).natAbs := by
…

Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.blockCandidates, OAI.JointDickman.blockCandidateRoot, OAI.JointDickman.PrimeProductAvailable, OAI.JointDickman.candidateSiteValue, OAI.JointDickman.candidateQuotient