OAI/Computability/QuantumFactoring/FlatDataPredicates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.DataView.residueGood line 21
2. lemma OAI.ExactQuantumFactoring.DataView.canonicalResidue line 28
3. lemma OAI.ExactQuantumFactoring.DataView.goodList line 32
4. lemma OAI.ExactQuantumFactoring.DataView.canonicalList line 37
5. lemma OAI.ExactQuantumFactoring.DataView.listPassed line 41
6. lemma OAI.ExactQuantumFactoring.DataView.orderPassed line 54
7. lemma OAI.ExactQuantumFactoring.DataView.splitPassed line 59
8. theorem OAI.ExactQuantumFactoring.DataView.splitPassed_correct line 67

   Source documentation

   Actual verified data give the ideal local event on exactly the same retained outcome. The statement covers all nonzero divisors of a verified node.

   theorem splitPassed_correct {n : ℕ} (hM : 0 < M) (m : Basis n)
       (hm : 2 ≤ (bitsValue m).toNat) (hd : (bitsValue m).toNat ∣ M)
       (hn : 0 < n) (r : UniversalSplit.Raw n) :
       dataSplitPassed d m hn r ↔ UniversalSplit.passed m r := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.UniversalSplit.Raw, OAI.ExactQuantumFactoring.dataSplitPassed, OAI.ExactQuantumFactoring.UniversalSplit.passed