ArithGraph.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Exact arithmetic reindexing in the divisor graph

The change of variables turns two divisor representations into an additive edge. The underlying integer identities hold in both directions without asymptotic hypotheses.

theorem OAI.JointDickman.divisor_edge_forward line 18
Source documentation
Reconstruct the second quotient and the additive edge from the first quotient. All variables are integers, allowing both signs of the lag.
```
theorem divisor_edge_forward {a b c j m z : ℤ}
    (hcoeff : a - b = j * c) (hquot : c * z = a * m + 1) :
    c * (z - j * m) = b * m + 1 ∧
      b * z + j = a * (z - j * m) := by
…
```
theorem OAI.JointDickman.divisor_edge_iff line 29
Source documentation
The congruence at the new endpoint reconstructs the old divisor representation. Coprimality with the lag is precisely the cancellation needed in the reverse direction.
```
theorem divisor_edge_iff {a b c j z : ℤ}
    (hcoeff : a - b = j * c) (hcop : IsCoprime a j) :
    (∃ m : ℤ, c * z = a * m + 1) ↔ a ∣ b * z + j := by
…
```

theorem OAI.JointDickman.divisor_edge_quotient_unique line 43

Source documentation

No multiplicity is introduced by the reindexing.

theorem divisor_edge_quotient_unique {a c z m₁ m₂ : ℤ} (ha : a ≠ 0)
    (hm₁ : c * z = a * m₁ + 1) (hm₂ : c * z = a * m₂ + 1) : m₁ = m₂ := by
…

theorem OAI.JointDickman.common_divisor_difference line 50
Source documentation
Both old divisibility conditions imply the coefficient difference is divisible by c, because the multiplier is a unit modulo c.
```
theorem common_divisor_difference {a b c m : ℤ}
    (ha : c ∣ a * m + 1) (hb : c ∣ b * m + 1) : c ∣ a - b := by
…
```