ArithmeticCandidateRoots.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

The arithmetic quotient and its candidate root

theorem OAI.JointDickman.divisorEdgeInverse_equation line 13
Source documentation
The reconstructed multiplier satisfies the exact affine equation before any residue model or exceptional event is introduced.
```
theorem divisorEdgeInverse_equation {a b c N : ℕ} {j : ℤ}
    (ha : 0 < a) (hc : 0 < c) (he : (a : ℤ)-b = j*c)
    (hcop : a.Coprime j.natAbs) {n : ℕ}
    (hn : n ∈ divisorEdgeNew a b c N j) :
    a*b*divisorEdgeInverse a b c n+b = c*n := by
…
```
Mentions: OAI.JointDickman.divisorEdgeNew, OAI.JointDickman.divisorEdgeInverse

theorem OAI.JointDickman.affine_quotient_prime_root line 29

Source documentation

Outside coefficient primes the remaining arithmetic argument has the ordinary linear root used by the candidate model.

theorem affine_quotient_prime_root {a b c m n p : ℕ} [Fact p.Prime]
    (he : a*b*m+b = c*n) (ha : ¬ p ∣ a) (hb : ¬ p ∣ b)
    (hc : ¬ p ∣ c) :
    p ∣ m ↔ (n : ZMod p) = (b : ZMod p)/(c : ZMod p) := by
…

theorem OAI.JointDickman.affine_quotient_no_third_coefficient line 47

Source documentation

A prime of the third coefficient cannot divide the remaining argument.

theorem affine_quotient_no_third_coefficient {a b c m n p : ℕ} [Fact p.Prime]
    (he : a*b*m+b = c*n) (hb : ¬ p ∣ b) (hc : p ∣ c) : ¬ p ∣ m := by
…

theorem OAI.JointDickman.prime_square_product_iff line 58
Source documentation
For a coefficient with exactly one factor of p, testing the quotient for p is a test of the original numerator modulo p².
```
theorem prime_square_product_iff {p d m : ℕ} (hp : p.Prime)
    (hd : p ∣ d) (hdd : ¬ p^2 ∣ d) : p^2 ∣ d*m ↔ p ∣ m := by
…
```
theorem OAI.JointDickman.affine_quotient_coefficient_root line 68
theorem OAI.JointDickman.candidate_affine_quotient_root line 77
Source documentation
With the manuscript's site indexing, the linear root is precisely candidateModRoot, not a new independently specified residue.
```
theorem candidate_affine_quotient_root {M p u m : ℕ} [Fact p.Prime]
    (e : BlockCandidateIndex M)
    (he : 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) :
    p ∣ m ↔ (u : ZMod p) = candidateModRoot p e := by
…
```
Mentions: OAI.JointDickman.BlockCandidateIndex, OAI.JointDickman.candidateHigh, OAI.JointDickman.candidateLow, OAI.JointDickman.candidateQuotient, OAI.JointDickman.candidateModRoot