ArithmeticRootMask.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Matching arithmetic quotient tests with the masked residue tests

theorem OAI.JointDickman.candidateSiteValue_low line 12
theorem OAI.JointDickman.candidateSiteValue_high line 16
theorem OAI.JointDickman.candidate_occupied_root_impossible line 31
Source documentation
Away from coefficient primes, an occupied residue root would be one of the already controlled forced hits at a third site.
```
theorem candidate_occupied_root_impossible {B L T H M p u : ℕ} {τ C : ℝ}
    [Fact p.Prime] {e : BlockCandidateIndex M}
    (he : BlockCandidateAdmissible B L T H τ C e) (hp : p ∈ auxiliaryPrimes B)
    (ha : ¬ p ∣ candidateHigh e) (hb : ¬ p ∣ candidateLow e)
    (hc : ¬ p ∣ candidateQuotient e)
    (hno : ¬ CandidateForcedWitness B e (fun i => coefficientPrimeSet B (u+(i.val+1))))
    (hocc : blockPrimeHit M p (u : ZMod p) ≠ emptyBlockPrimeHit M) :
    (u : ZMod p) ≠ candidateModRoot p e := by
…
```
Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.candidateHigh, OAI.JointDickman.candidateLow, OAI.JointDickman.candidateQuotient, OAI.JointDickman.CandidateForcedWitness, OAI.JointDickman.coefficientPrimeSet, OAI.JointDickman.blockPrimeHit, OAI.JointDickman.emptyBlockPrimeHit, OAI.JointDickman.candidateModRoot

theorem OAI.JointDickman.arithmetic_quotient_masked_hit line 61

Source documentation

Thus every nonexceptional auxiliary prime has the same test in the actual quotient and the masked conditional model.

theorem arithmetic_quotient_masked_hit {B L T H M p u m : ℕ} {τ C : ℝ}
    [Fact p.Prime] (I : Finset (BlockCandidateIndex M))
    {e : BlockCandidateIndex M} (heI : e ∈ I)
    (he : BlockCandidateAdmissible B L T H τ C e) (hp : p ∈ auxiliaryPrimes B)
    (heq : candidateHigh e*candidateLow e*m+candidateLow e =
      candidateQuotient e*(u+(e.1.1.val+1)))
    (ha : ¬ p ∣ candidateHigh e) (hb : ¬ p ∣ candidateLow e)
    (hc : ¬ p ∣ candidateQuotient e)
    (hno : ¬ CandidateForcedWitness B e (fun i => coefficientPrimeSet B (u+(i.val+1)))) :
    p ∣ m ↔ e ∈ (maskedCandidatePrimeHit I p
      (blockPrimeHit M p (u : ZMod p)) (u : ZMod p)).val := by
…

Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.BlockCandidateAdmissible, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.candidateHigh, OAI.JointDickman.candidateLow, OAI.JointDickman.candidateQuotient, OAI.JointDickman.CandidateForcedWitness, OAI.JointDickman.coefficientPrimeSet, OAI.JointDickman.maskedCandidatePrimeHit, OAI.JointDickman.blockPrimeHit