OAI/Computability/QuantumFactoring/RetrospectiveNode.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.PhysicalNode.natBasis_zero line 21
2. lemma OAI.ExactQuantumFactoring.PhysicalNode.start_zero line 28
3. lemma OAI.ExactQuantumFactoring.PhysicalNode.config_zero line 39
4. lemma OAI.ExactQuantumFactoring.PhysicalNode.query_zero line 48
5. lemma OAI.ExactQuantumFactoring.dataSplitPassed_zero line 58
6. def OAI.ExactQuantumFactoring.NodeKernel.dataTests line 71

   Source documentation

   Retrospective evaluation on the actual split trace, with one verified read-only factor-data view for this physical node. The controller and all query words are the same ones used by the physical run.

   noncomputable def dataTests {n : ℕ} (q : Basis n) (d : FactorData) (hn : 0<n) :
       (t : ℕ)→SplitMachine.Trace n t→Prop
     | 0,_=>True
     | t+1,r=>dataTests q d hn t r.1 ∧ dataSplitPassed d
         ((PhysicalNode.query n (2*n)).eval
           ((PhysicalNode.machine n (2*n)).config (start q) t r.1)) hn r.2

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.FactorData, OAI.ExactQuantumFactoring.SplitMachine.Trace, OAI.ExactQuantumFactoring.dataSplitPassed, OAI.ExactQuantumFactoring.PhysicalNode.query, OAI.ExactQuantumFactoring.PhysicalNode.machine, OAI.ExactQuantumFactoring.NodeKernel.start

7. lemma OAI.ExactQuantumFactoring.NodeKernel.dataTests_correct line 78
8. def OAI.ExactQuantumFactoring.NodeKernel.dataPassed line 97
9. lemma OAI.ExactQuantumFactoring.NodeKernel.dataPassed_correct line 100