CubeFreeRationalSupply.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.coprime_div_gcd_pow_of_prime_power_free line 11
Source documentation
Removing the full common prime-power part leaves a coprime quotient. Only primes of the supply need the displayed multiplicity bound.
```
theorem coprime_div_gcd_pow_of_prime_power_free {q P r : ℕ}
    (hq : 0 < q) (hP : 0 < P)
    (hfree : ∀ p : ℕ, p.Prime → p ∣ P → ¬p ^ (r + 1) ∣ q) :
    Nat.Coprime (q / Nat.gcd q (P ^ r)) P := by
…
```

theorem OAI.Problem337.cube_free_supply_split line 37

Source documentation

The finite cube-free splitting used by composite-modulus supply. No squarefreeness of P is needed; repeated primes only make the removal larger.

theorem cube_free_supply_split {q P : ℕ} (hq : 0 < q) (hP : 0 < P)
    (hfree : ∀ p : ℕ, p.Prime → ¬p ^ 3 ∣ q) :
    ∃ g d : ℕ, 0 < g ∧ 0 < d ∧ g ∣ P ^ 2 ∧
      d ∣ q ∧ g * d = q ∧ Nat.Coprime d P := by
…

theorem OAI.Problem337.rational_divisor_sum_of_gcd_square_quotient line 53
Source documentation
A representation of the coprime quotient, whose numerators divide P², rescales to the original integer with numerators dividing P⁴, and no increase in the number of summands.
```
theorem rational_divisor_sum_of_gcd_square_quotient {q P B : ℕ}
    (hq : 0 < q)
    (hrep : HasRationalDivisorSum (P ^ 2) ((q / Nat.gcd q (P ^ 2) : ℕ) : ℚ) B) :
    HasRationalDivisorSum (P ^ 4) (q : ℚ) B := by
…
```
Mentions: OAI.Problem337.HasRationalDivisorSum

theorem OAI.Problem337.rational_divisor_sum_of_cube_free_divisor_supply line 69

Source documentation

Supplying the coprime divisors is enough to supply a cube-free integer. The coprime-divisor premise includes 1, so no exceptional zero-frequency or unit-modulus case is being suppressed.

theorem rational_divisor_sum_of_cube_free_divisor_supply {q P B : ℕ}
    (hq : 0 < q) (hP : 0 < P)
    (hfree : ∀ p : ℕ, p.Prime → ¬p ^ 3 ∣ q)
    (hrep : ∀ d : ℕ, 0 < d → d ∣ q → Nat.Coprime d P →
      HasRationalDivisorSum (P ^ 2) (d : ℚ) B) :
    HasRationalDivisorSum (P ^ 4) (q : ℚ) B := by
…

Mentions: OAI.Problem337.HasRationalDivisorSum

theorem OAI.Problem337.marked_rational_supply_of_cube_free_set line 86

Source documentation

Finite assembly for the canonical marked-grouping interface. The unknown arithmetic inputs remain explicit: density of good cube-free moduli, and bounded rational-divisor supply for their coprime divisors.

theorem marked_rational_supply_of_cube_free_set
    (m P B : ℕ) (G : Finset ℕ) (hP : 0 < P)
    (hG : G ⊆ Finset.Icc 1 (m ^ 4))
    (hcard : 2 * m ^ 4 < 3 * G.card)
    (hfree : ∀ q ∈ G, ∀ p : ℕ, p.Prime → ¬p ^ 3 ∣ q)
    (hrep : ∀ q ∈ G, ∀ d : ℕ, 0 < d → d ∣ q → Nat.Coprime d P →
      HasRationalDivisorSum (P ^ 2) (d : ℚ) B) :
    HasRationalDivisorSupply m (P ^ 4) (2 * B) := by
…

Mentions: OAI.Problem337.HasRationalDivisorSum, OAI.Problem337.HasRationalDivisorSupply