OAI/Computability/QuantumFactoring/CyclicAlgebra.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactQuantumFactoring.Primality.Cyclic line 14

   Source documentation

   Exactly s coefficients with cyclic convolution, the concrete algebra (Z/mZ)[X]/(X^s-1) used in the appendix.

   abbrev Cyclic (R : Type*) [Semiring R] (s : ℕ) := AddMonoidAlgebra R (Fin s)

2. def OAI.ExactQuantumFactoring.Primality.cyclicOf line 16
3. lemma OAI.ExactQuantumFactoring.Primality.cyclicOf_coeff line 19
4. lemma OAI.ExactQuantumFactoring.Primality.cyclic_mul_coeff line 22
5. def OAI.ExactQuantumFactoring.Primality.cyclicX line 33

   Source documentation

   The residue class of X. No exponentially long polynomial is constructed.

   noncomputable def cyclicX {R : Type*} [Semiring R] (s : ℕ) [NeZero s] : Cyclic R s :=
   …

   Mentions: OAI.ExactQuantumFactoring.Primality.Cyclic

6. def OAI.ExactQuantumFactoring.Primality.cyclicC line 36
7. lemma OAI.ExactQuantumFactoring.Primality.cyclicC_nat line 39
8. lemma OAI.ExactQuantumFactoring.Primality.cyclic_prime_test line 48

   Source documentation

   Primes satisfy the literal cyclic-array test by characteristic-p Frobenius.

   lemma cyclic_prime_test {m s : ℕ} [NeZero s] (hm : m.Prime) (a : ℕ) :
       (cyclicX (R := ZMod m) s + cyclicC s (a : ZMod m))^m =
   …

   Mentions: OAI.ExactQuantumFactoring.Primality.cyclicX, OAI.ExactQuantumFactoring.Primality.cyclicC

9. def OAI.ExactQuantumFactoring.Primality.rootPower line 57
10. def OAI.ExactQuantumFactoring.Primality.cyclicEval line 65
11. lemma OAI.ExactQuantumFactoring.Primality.cyclicEval_X line 69
12. lemma OAI.ExactQuantumFactoring.Primality.cyclicEval_C line 74
13. lemma OAI.ExactQuantumFactoring.Primality.cyclic_test_introspective line 81

    Source documentation

    Equality of the two concrete coefficient arrays gives exactly the introspective identity needed by the appendix's root-count contradiction.

    lemma cyclic_test_introspective {F : Type*} [Field F] {m s p a : ℕ}
        [NeZero s] [CharP F p] (hs : 2 ≤ s) (hpm : p ∣ m)
        (h : (cyclicX (R := ZMod m) s + cyclicC s (a : ZMod m))^m =
    …

    Mentions: OAI.ExactQuantumFactoring.Primality.cyclicX, OAI.ExactQuantumFactoring.Primality.cyclicC