ArithmeticRootIdentification.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic root families agree outside the explicit exceptional events

theorem OAI.JointDickman.trimmedCandidatePrimeHit_eq line 11
def OAI.JointDickman.arithmeticCandidatePrimeFamily line 23

theorem OAI.JointDickman.arithmetic_roots_eq_masked line 29

Source documentation

All three exclusions have their own proved probability bounds. The quotient family here is the actual family satisfying the affine equations.

theorem arithmetic_roots_eq_masked {B L T H M u : ℕ} {τ C : ℝ}
    (I : Finset (BlockCandidateIndex M)) (m : BlockCandidateIndex M → ℕ)
    (he : ∀ e ∈ I, BlockCandidateAdmissible B L T H τ C e)
    (heq : ∀ e ∈ I, candidateHigh e*candidateLow e*m e+candidateLow e =
      candidateQuotient e*(u+(e.1.1.val+1)))
    (hforce : ∀ e ∈ I, ¬ CandidateForcedWitness B e
      (fun i => coefficientPrimeSet B (u+(i.val+1))))
    (hactual : ¬ ArithmeticCoefficientHit B I m)
    (hmasked : ¬ MaskedCoefficientEvent I (arithmeticPrimePatterns B M u)
      (fun p => (u : ZMod p.val))) :
    arithmeticCandidatePrimeFamily B I m =
      maskedPrimeRootFamily I (arithmeticPrimePatterns B M u) (fun p => (u : ZMod p.val)) := by
…

Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.candidateHigh, OAI.JointDickman.candidateLow, OAI.JointDickman.candidateQuotient, OAI.JointDickman.CandidateForcedWitness, OAI.JointDickman.coefficientPrimeSet, OAI.JointDickman.ArithmeticCoefficientHit, OAI.JointDickman.MaskedCoefficientEvent, OAI.JointDickman.arithmeticPrimePatterns, OAI.JointDickman.arithmeticCandidatePrimeFamily, OAI.JointDickman.maskedPrimeRootFamily