TransferArithmetic.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The arithmetic separation of diagonal and transferred terms

theorem OAI.Ostmann.transferred_products_coprime line 12

Source documentation

A nonzero transferred frequency rules out a shared prime between the two inherited products. All such primes exceed the frequency.

theorem transferred_products_coprime (HL HR : ℕ) (v w s P : ℤ) (hs : s ≠ 0)
    (hrel : v * HR - w * HL = s * P)
    (hsmall : ∀ q, q.Prime → q ∣ HL → q ∣ HR → s.natAbs < q)
    (hunit : ∀ q, q.Prime → q ∣ HL → q ∣ HR → IsCoprime (q : ℤ) P) :
    HL.Coprime HR := by
…

theorem OAI.Ostmann.large_prime_factors_coprime_frequency line 29

theorem OAI.Ostmann.diagonal_products_equal line 38

Source documentation

The zero numerator has only the equal-product, equal-frequency diagonal when prime factors exceed the frequencies.

theorem diagonal_products_equal (HL HR : ℕ) (hHL : 0 < HL) (v w : ℤ)
    (hv : v ≠ 0) (hw : w ≠ 0) (hrel : v * HR = w * HL)
    (hL : ∀ q, q.Prime → q ∣ HL → v.natAbs < q)
    (hR : ∀ q, q.Prime → q ∣ HR → w.natAbs < q) : HL = HR ∧ v = w := by
…

theorem OAI.Ostmann.unique_transferred_frequency line 59
Source documentation
Regrouping a nonzero numerator by the new signed frequency is one-to-one, exactly as in the transfer substitution.
```
theorem unique_transferred_frequency (N P : ℤ) (hN : N ≠ 0) (hP : P ≠ 0)
    (hdiv : P ∣ N) : ∃! s : ℤ, s ≠ 0 ∧ N = s * P := by
…
```