PrimeNormFibers.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Norm fibers for a fixed number of primary prime factors

Equal norms give b * conjugate b = b₀ * conjugate b₀. Consequently every prime factor of b is one of the prime factors of b₀ or its conjugate. For products of k primary primes this bounds every norm fiber by (2 * k)^k, uniformly in all prime supports and the norm. No general divisor estimate is needed for the structured coefficients.

lemma OAI.CubicFirstMoment.prime_tuple_norm_range_subset line 25
Source documentation
A prime in a tuple of the same norm must occur in the reference tuple or in its conjugate. Primary normalization turns association into equality.
```
lemma prime_tuple_norm_range_subset (f g : ι → Eisenstein)
    (hf : ∀ i, primaryPrime (f i)) (hg : ∀ i, primaryPrime (g i))
    (hn : normNat (∏ i, g i) = normNat (∏ i, f i)) (i : ι) :
    g i ∈ Finset.univ.image f ∪ Finset.univ.image (fun j => conjugate (f j)) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.normNat, OAI.CubicFirstMoment.conjugate
theorem OAI.CubicFirstMoment.primeProduct_norm_fiber_card line 48
Source documentation
The number of distinct products with a prescribed norm is bounded solely in terms of the number of prime factors, even with repetitions.
```
theorem primeProduct_norm_fiber_card (S : ι → Finset Eisenstein)
    (hS : ∀ i, ∀ p ∈ S i, primaryPrime p) (n : ℕ) :
    ((orderedConvolutionSupport S).filter (fun b => normNat b = n)).card ≤
      (2 * Fintype.card ι) ^ (Fintype.card ι) := by
…
```
Mentions: OAI.CubicFirstMoment.Eisenstein, OAI.CubicFirstMoment.primaryPrime, OAI.CubicFirstMoment.orderedConvolutionSupport, OAI.CubicFirstMoment.normNat