OAI/Computability/QuantumFactoring/PerfectPowerCircuit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.rootCheck line 16

   Source documentation

   Check a candidate root against the input integer, with its static exponent.

   def rootCheck (w e : ℕ) : BooleanNetwork (w+w) 1 :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootCheck_eval line 20
3. def OAI.ExactQuantumFactoring.BitArithmetic.exponentCheck line 36
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.exponentCheck_eval line 39
5. def OAI.ExactQuantumFactoring.BitArithmetic.perfectPowerNet line 54
6. theorem OAI.ExactQuantumFactoring.BitArithmetic.perfectPowerNet_correct line 59

   Source documentation

   The complete first AKS rejection check, as an actual polynomial-size Boolean circuit: exponents2..n and n exact bounded binary-root steps each.

   theorem perfectPowerNet_correct {n : ℕ} (hn : 2 ≤ n) (m : Basis (rootWidth n))
       (hm : (bitsValue m).toNat < 2^n) :
       (perfectPowerNet n).eval m 0=true ↔ Primality.PerfectPower (bitsValue m).toNat := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.BitArithmetic.rootWidth, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.BitArithmetic.perfectPowerNet, OAI.ExactQuantumFactoring.Primality.PerfectPower

7. lemma OAI.ExactQuantumFactoring.BitArithmetic.rootCheck_count line 80
8. abbrev OAI.ExactQuantumFactoring.BitArithmetic.perfectCheckBound line 90
9. lemma OAI.ExactQuantumFactoring.BitArithmetic.exponentCheck_count line 94
10. lemma OAI.ExactQuantumFactoring.BitArithmetic.perfectExponent_count line 104
11. lemma OAI.ExactQuantumFactoring.BitArithmetic.perfectPowerNet_count line 118