OAI/Computability/QuantumFactoring/CyclicTestCircuit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BitArithmetic.arrayConstant_decode line 15
2. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicXNet line 21
3. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicCNet line 23
4. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicXNet_value line 26
5. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicCNet_value line 35
6. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicPowerOn line 43
7. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicPowerOn_value line 47
8. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicPowerOn_count line 56
9. lemma OAI.ExactQuantumFactoring.BitArithmetic.horner_reverse line 64
10. def OAI.ExactQuantumFactoring.BitArithmetic.cyclicTest line 72

    Source documentation

    Literal 8s AKS congruence on s coefficient words, m in the input word.

    def cyclicTest (s w a : ℕ) [NeZero s] : BooleanNetwork w 1 :=
    …

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

11. lemma OAI.ExactQuantumFactoring.BitArithmetic.cyclicTest_correct line 81