PrimalityRootCount.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.Primality.residueOrbit line 15
Source documentation
The nonnegative exponent orbit. In a finite group this is the manuscript's H; using its submonoid presentation makes the m^u p^v representatives explicit.
```
def residueOrbit (s m p : ℕ) : Submonoid (ZMod s) :=
…
```
lemma OAI.ExactQuantumFactoring.Primality.residueOrbit_rep line 18
def OAI.ExactQuantumFactoring.Primality.residueRoot line 22
lemma OAI.ExactQuantumFactoring.Primality.residueRoot_injective line 25
lemma OAI.ExactQuantumFactoring.Primality.eval_eq_on_orbit line 33

lemma OAI.ExactQuantumFactoring.Primality.eval_injective_low_degree line 49

Source documentation

The lower-bound injection is proved by h distinct roots of f-g, not by assuming any tested product has a nonzero value.

lemma eval_injective_low_degree {F : Type*} [Field F] {s m p : ℕ} [NeZero s]
    {w : F} (hw : IsPrimitiveRoot w s) {f g : F[X]}
    (hfm : Introspective s m f) (hfp : Introspective s p f)
    (hgm : Introspective s m g) (hgp : Introspective s p g)
    (hfg : f.eval w = g.eval w)
    (hf : f.natDegree < Nat.card (residueOrbit s m p))
    (hg : g.natDegree < Nat.card (residueOrbit s m p)) : f = g := by
…

Mentions: OAI.ExactQuantumFactoring.Primality.Introspective, OAI.ExactQuantumFactoring.Primality.residueOrbit

def OAI.ExactQuantumFactoring.Primality.subsetPolynomial line 62
lemma OAI.ExactQuantumFactoring.Primality.subsetPolynomial_injective line 65
lemma OAI.ExactQuantumFactoring.Primality.subsetPolynomial_degree line 71
lemma OAI.ExactQuantumFactoring.Primality.subsetPolynomial_introspective line 75

lemma OAI.ExactQuantumFactoring.Primality.subset_count_le_collision line 81

Source documentation

The entire lower/upper root count, prior to arithmetic estimates: a collision of two distinct integer exponents bounds the number of subset products.

lemma subset_count_le_collision {F : Type*} [Field F] {s m p : ℕ} [NeZero s]
    {w : F} (hw : IsPrimitiveRoot w s) (S : Finset F) {t k₁ k₂ : ℕ}
    (ht : t < Nat.card (residueOrbit s m p))
    (hm : ∀ a ∈ S, Introspective s m (X-C a))
    (hp : ∀ a ∈ S, Introspective s p (X-C a))
    (hk₁ : ∀ a ∈ S, Introspective s k₁ (X-C a))
    (hk₂ : ∀ a ∈ S, Introspective s k₂ (X-C a))
    (hk : w^k₁ = w^k₂) (hne : k₁ ≠ k₂) :
    S.card.choose t ≤ max k₁ k₂ := by
…

Mentions: OAI.ExactQuantumFactoring.Primality.residueOrbit, OAI.ExactQuantumFactoring.Primality.Introspective