OAI/Computability/QuantumFactoring/NodeVerifiedCircuit.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.PhysicalTree.resultFields line 20
2. def OAI.ExactQuantumFactoring.PhysicalTree.nodeWords line 22
3. lemma OAI.ExactQuantumFactoring.PhysicalTree.fields_nodeWords line 24
4. lemma OAI.ExactQuantumFactoring.PhysicalTree.nodeWords_length line 28
5. lemma OAI.ExactQuantumFactoring.PhysicalTree.numbers_nodeWords line 30
6. def OAI.ExactQuantumFactoring.PhysicalTree.NodeVerified line 34
7. lemma OAI.ExactQuantumFactoring.PhysicalTree.node_verified_of_passed line 38
8. theorem OAI.ExactQuantumFactoring.PhysicalTree.update_verified line 59

   Source documentation

   The queue remains canonical for ANY retrospectively verified local result, not only for results obtained on the all-good event.

   theorem update_verified {n : ℕ} (hn : 128 ≤ n) (a : Basis n) (as : List (Basis n))
       (hlen : (a::as).length ≤ capacity n) (ha : 2 ≤ (bitsValue a).toNat)
       (r : NodeKernel.Raw n) (hv : NodeVerified a r) :
       ∃ kids : List (Basis n), SortedWords.numbers kids=AuxiliaryTree.children (bitsValue a).toNat ∧
         (update n).eval (Fin.append (stackEncoding (capacity n) n (a::as)) (NodeKernel.encoding a r))=
           stackEncoding (capacity n) n (kids++as) := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.PhysicalTree.capacity, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.NodeKernel.Raw, OAI.ExactQuantumFactoring.PhysicalTree.NodeVerified, OAI.ExactQuantumFactoring.AuxiliaryTree.children, OAI.ExactQuantumFactoring.PhysicalTree.update, OAI.ExactQuantumFactoring.NodeKernel.encoding

9. def OAI.ExactQuantumFactoring.NodeMachine.verified line 75
10. def OAI.ExactQuantumFactoring.NodeMachine.rowQuery line 80
11. def OAI.ExactQuantumFactoring.NodeMachine.rowFields line 82
12. def OAI.ExactQuantumFactoring.NodeMachine.rowVerifiedNet line 84
13. def OAI.ExactQuantumFactoring.NodeMachine.verifiedNet line 86
14. lemma OAI.ExactQuantumFactoring.NodeMachine.rowQuery_encoded line 90
15. lemma OAI.ExactQuantumFactoring.NodeMachine.rowFields_encoded line 93
16. lemma OAI.ExactQuantumFactoring.NodeMachine.rowVerifiedNet_encoded line 97
17. theorem OAI.ExactQuantumFactoring.NodeMachine.verifiedNet_encoded line 107

    Source documentation

    A literal, bounded Boolean verifier of every actual retained root/node factor list. No predicate is silently converted to an oracle gate.

    theorem verifiedNet_encoded (hn : 128 ≤ n) (x : Basis c) (t : ℕ) (h : Trace n t) :
        (M.verifiedNet t).eval (M.encoded x t h) 0=true ↔ M.verified x t h := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.NodeMachine.Trace