ArithmeticSupport.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Arithmetic support at a reversing node

These are the elementary support facts preceding the progression estimate in Section 8. The numerator is automatically coprime to inherited slots; the remaining condition at a new prime is exactly nondivisibility by its square.

theorem OAI.Ostmann.reversal_numerator_coprime line 17

theorem OAI.Ostmann.reversal_inherited_coprime line 25

Source documentation

Both the inserted integer and its compensation product inherit all required coprimalities.

theorem reversal_inherited_coprime (v w HL HR s u p : ℤ)
    (hLR : IsCoprime HL HR) (hv : IsCoprime v HL) (hw : IsCoprime w HR)
    (hrel : v * HR - w * HL = s * u * p) :
    IsCoprime p (HL * HR) ∧ IsCoprime u (HL * HR) := by
…

theorem OAI.Ostmann.reversal_square_test line 35

Source documentation

A prime occurring once in u occurs once in the numerator exactly when it misses p.

theorem reversal_square_test (b s u p : ℕ) (hb : b.Prime)
    (hbs : ¬ b ∣ s) (hbu : b ∣ u) (hbu2 : ¬ b ^ 2 ∣ u) :
    (¬ b ^ 2 ∣ s * u * p) ↔ ¬ b ∣ p := by
…

theorem OAI.Ostmann.reversal_integral_of_prime_tests line 48

Source documentation

Divisibility by the frequency and all distinct new prime factors gives integer reconstruction.

theorem reversal_integral_of_prime_tests (s N : ℤ) (U : Finset ℕ)
    (hprime : ∀ b ∈ U, b.Prime) (hs : s ∣ N)
    (hsu : ∀ b ∈ U, IsCoprime s (b : ℤ))
    (hdiv : ∀ b ∈ U, (b : ℤ) ∣ N) :
    (s * ∏ b ∈ U, (b : ℤ)) ∣ N := by
…