Primality.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Necessary exact primality component of Appendix A. The tests are polynomial congruences, not a primality oracle. These lemmas start the appendix's actual root-count proof; no polynomial-time implementation is assumed here.

def OAI.ExactQuantumFactoring.Primality.Introspective line 16
Source documentation
The evaluation form of an introspective exponent modulo X^s-1.
```
def Introspective {F : Type*} [CommRing F] (s k : ℕ) (f : F[X]) : Prop :=
…
```
lemma OAI.ExactQuantumFactoring.Primality.Introspective.one line 19
lemma OAI.ExactQuantumFactoring.Primality.Introspective.mul_exp line 22
lemma OAI.ExactQuantumFactoring.Primality.Introspective.pow_exp line 30
lemma OAI.ExactQuantumFactoring.Primality.Introspective.mul_poly line 36
lemma OAI.ExactQuantumFactoring.Primality.Introspective.prod line 43
lemma OAI.ExactQuantumFactoring.Primality.introspective_of_congruence line 56
Source documentation
A successful congruence test implies the evaluation identity at every s-th root. This implication includes the zero polynomial case correctly.
```
lemma introspective_of_congruence {F : Type*} [CommRing F] {s k : ℕ} {f : F[X]}
    (h : X^s - 1 ∣ f^k - f.comp (X^k)) : Introspective s k f := by
…
```
Mentions: OAI.ExactQuantumFactoring.Primality.Introspective
lemma OAI.ExactQuantumFactoring.Primality.natCast_frobenius line 63
lemma OAI.ExactQuantumFactoring.Primality.linear_frobenius line 67
lemma OAI.ExactQuantumFactoring.Primality.propagate line 75
Source documentation
Every product tested in the root count propagates along m^u p^v, precisely as in equation (A.4); no division by its value at a root is involved.
```
lemma propagate {F ι : Type*} [CommRing F] (p : ℕ) [Fact p.Prime] [CharP F p]
    (s m : ℕ) (S : Finset ι) (a : ι → ℕ)
    (htest : ∀ i ∈ S, Introspective s m (X+C (a i : F))) (u v : ℕ) :
    Introspective s (m^u*p^v) (∏ i ∈ S, (X+C (a i : F))) := by
…
```
Mentions: OAI.ExactQuantumFactoring.Primality.Introspective