CubeFreeSupplyFromExceptions.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Problem337.badCoprimeDivisorMultiples line 11
Source documentation
The actual exceptional moduli: multiples of a bad divisor coprime to the fixed supply. The unit divisor is excluded, as in the Fourier collision API.
```
def badCoprimeDivisorMultiples (N P : ℕ) (Q : ℕ → Prop) : Finset ℕ := by
…
```
theorem OAI.Problem337.mem_badCoprimeDivisorMultiples line 16
theorem OAI.Problem337.marked_rational_supply_of_cube_free_bad_divisors line 26
Source documentation
Exact finite assembly of the cube-free alternative. The density premise counts the specified exceptional moduli, not an abstract set standing in for the desired result. The second premise is the all-divisor Fourier supply API. Both arithmetic premises remain explicit and must be proved separately.
```
theorem marked_rational_supply_of_cube_free_bad_divisors
    (m P B : ℕ) (Q : ℕ → Prop) (hP : 0 < P)
    (hbad : ((badCoprimeDivisorMultiples (m ^ 4) P Q).card : ℝ) <
      (m ^ 4 : ℕ) / 12)
    (hrep : ∀ d : ℕ, 0 < d → d ≤ m ^ 4 → Nat.Coprime d P →
      (∀ r : ℕ, 2 ≤ r → r ∣ d → Q r) →
      HasRationalDivisorSum (P ^ 2) (d : ℚ) B) :
    HasRationalDivisorSupply m (P ^ 4) (2 * B) := by
…
```
Mentions: OAI.Problem337.badCoprimeDivisorMultiples, OAI.Problem337.HasRationalDivisorSum, OAI.Problem337.HasRationalDivisorSupply