OAI/Computability/QuantumFactoring/VerifiedRoot.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.NodeMachine.first_verified line 19
2. lemma OAI.ExactQuantumFactoring.PhysicalTree.nodeWords_layout line 27
3. theorem OAI.ExactQuantumFactoring.PhysicalTree.verified_root line 34

   Source documentation

   The literal data-verifier flag implies a correct root readout on arbitrary raw histories, not just on histories assumed successful in the analysis.

   theorem verified_root {n N : ℕ} (hN : 2 ≤ N) (hb : N<2^n)
       (t : ℕ) (h : NodeMachine.Trace n (t+1))
       (hp : (machine n).verified (initialQueue n N) (t+1) h) :
       ∃ zs : List (Basis n), zs.length=n ∧ CorrectEncoding N n (SortedWords.numbers zs) ∧
         (rootResult n t).eval ((machine n).encoded (initialQueue n N) (t+1) h)=
           SortedWords.layout n n zs := by
   …

   Mentions: OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.initialQueue, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.CorrectEncoding, OAI.ExactQuantumFactoring.PhysicalTree.rootResult

4. theorem OAI.ExactQuantumFactoring.PhysicalTree.verifier_readout line 56

   Source documentation

   Exact equivalence of the physical data-verifier bit with the explicit retrospective data predicate, and its unconditional root-output soundness.

   theorem verifier_readout {n N : ℕ} (hn : 128 ≤ n) (hN : 2 ≤ N) (hb : N<2^n)
       (t : ℕ) (h : NodeMachine.Trace n (t+1))
       (hp : ((machine n).verifiedNet (t+1)).eval
         ((machine n).encoded (initialQueue n N) (t+1) h) 0=true) :
       ∃ zs : List (Basis n), zs.length=n ∧ CorrectEncoding N n (SortedWords.numbers zs) ∧
         (rootResult n t).eval ((machine n).encoded (initialQueue n N) (t+1) h)=
           SortedWords.layout n n zs :=
   …

   Mentions: OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.initialQueue, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.CorrectEncoding, OAI.ExactQuantumFactoring.PhysicalTree.rootResult