CompositeBadModuli.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.Problem337.indexed_divisor_collision_eq line 14
Source documentation
A finite natural list has the same collision count whether residues are represented by remainders or by elements of ZMod.
```
theorem indexed_divisor_collision_eq (P q : ℕ) [NeZero q] :
    indexedResidueCollisionCount (fun d : ↥P.divisors => (d.val : ZMod q)) =
      (collisionPairs P.divisors (fun d => d % q)).card := by
…
```
Mentions: OAI.Problem337.indexedResidueCollisionCount, OAI.Problem337.collisionPairs
theorem OAI.Problem337.divisorResidueEnergy_eq_collision_quotient line 27
Source documentation
Exact normalized energy of the complete divisor list.
```
theorem divisorResidueEnergy_eq_collision_quotient (P q : ℕ) [NeZero q] :
    divisorResidueEnergy P q =
      ((collisionPairs P.divisors (fun d => d % q)).card : ℝ) /
        (P.divisors.card : ℝ)^2 := by
…
```
Mentions: OAI.Problem337.divisorResidueEnergy, OAI.Problem337.collisionPairs
def OAI.Problem337.CompositeSupply.BadModulus line 41
Source documentation
A global, total predicate independent of any later ambient supply range. The strict energy inequality is encoded without division or typeclass data.
```
def BadModulus (d : ℕ) : Prop :=
…
```
lemma OAI.Problem337.CompositeSupply.divisor_card_pos line 47
lemma OAI.Problem337.CompositeSupply.badModulus_iff_energy line 52
lemma OAI.Problem337.CompositeSupply.badModulus_fixed_base_energy line 66
Source documentation
All bad moduli in a dyadic block have a large energy already in its smaller, fixed divisor pool. This is the input for collision double counting.
```
lemma badModulus_fixed_base_energy {D d : ℕ} [NeZero d]
    (hD : 0 < D) (hDd : D ≤ d) (hd : BadModulus d) :
    1 / (d : ℝ)^(7 / 8 : ℝ) < divisorResidueEnergy (base D) d := by
…
```
Mentions: OAI.Problem337.D, OAI.Problem337.CompositeSupply.BadModulus, OAI.Problem337.divisorResidueEnergy, OAI.Problem337.CompositeSupply.base
lemma OAI.Problem337.CompositeSupply.badModulus_fixed_base_collisions line 75
Source documentation
Collision-count version of the fixed-pool implication, ready for the finite exceptional-modulus theorem.
```
lemma badModulus_fixed_base_collisions {D d : ℕ} [NeZero d]
    (hD : 0 < D) (hDd : D ≤ d) (hd : BadModulus d) :
    ((base D).divisors.card : ℝ)^2 ≤
      (d : ℝ)^(7 / 8 : ℝ) *
        ((collisionPairs (base D).divisors (fun a => a % d)).card : ℝ) := by
…
```
Mentions: OAI.Problem337.D, OAI.Problem337.CompositeSupply.BadModulus, OAI.Problem337.CompositeSupply.base, OAI.Problem337.collisionPairs
lemma OAI.Problem337.CompositeSupply.badModulus_prime_lower line 90
Source documentation
The same global bad modulus satisfies the logarithmic roughness condition needed in any smaller dyadic block.
```
lemma badModulus_prime_lower {D d p : ℕ} (hD : 2 ≤ D) (hDd : D ≤ d)
    (hd : BadModulus d) (hp : p.Prime) (hpd : p ∣ d) :
    Real.log (2 * (D : ℝ)) ≤ (p : ℝ) := by
…
```
Mentions: OAI.Problem337.D, OAI.Problem337.CompositeSupply.BadModulus
lemma OAI.Problem337.CompositeSupply.ambient_energy_le_of_not_bad line 104
Source documentation
Outside the global bad set, every conductor dividing a modulus coprime to the ambient pool has the required ambient-pool energy bound.
```
lemma ambient_energy_le_of_not_bad {Y q d : ℕ} [NeZero d]
    (hq : 0 < q) (hqY : q ≤ Y) (hdq : d ∣ q)
    (hc : (base Y).Coprime q) (hnd : ¬ BadModulus d) (hd : 2 ≤ d) :
    divisorResidueEnergy (base Y) d ≤ 1 / (d : ℝ)^(7 / 8 : ℝ) := by
…
```
Mentions: OAI.Problem337.CompositeSupply.base, OAI.Problem337.CompositeSupply.BadModulus, OAI.Problem337.divisorResidueEnergy

lemma OAI.Problem337.CompositeSupply.ambient_collisions_le_of_not_bad line 121

Source documentation

The same ambient estimate in the unnormalized form used by the finite eight-product criterion.

lemma ambient_collisions_le_of_not_bad {Y q d : ℕ} [NeZero d]
    (hq : 0 < q) (hqY : q ≤ Y) (hdq : d ∣ q)
    (hc : (base Y).Coprime q) (hnd : ¬ BadModulus d) (hd : 2 ≤ d) :
    ((collisionPairs (base Y).divisors (fun a => a % d)).card : ℝ) ≤
      ((base Y).divisors.card : ℝ)^2 / (d : ℝ)^(7 / 8 : ℝ) := by
…

Mentions: OAI.Problem337.CompositeSupply.base, OAI.Problem337.CompositeSupply.BadModulus, OAI.Problem337.collisionPairs

lemma OAI.Problem337.CompositeSupply.log_le_conductor line 137
Source documentation
Every nontrivial conductor of a modulus coprime to the ambient pool starts beyond the logarithmic cutoff.
```
lemma log_le_conductor {Y q d : ℕ} (hc : (base Y).Coprime q)
    (hdq : d ∣ q) (hd : 2 ≤ d) : Real.log (Y : ℝ) ≤ (d : ℝ) := by
…
```
Mentions: OAI.Problem337.CompositeSupply.base