OAI/Computability/QuantumFactoring/PhysicalNodeSafety.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.PhysicalNode.next_safe line 19
2. theorem OAI.ExactQuantumFactoring.PhysicalNode.config_safe line 77

   Source documentation

   Safety is unconditional on every raw quantum outcome. In particular even a failed retained candidate only stalls; all subsequent nonzero queries divide this node's original modulus.

   theorem config_safe {n N : ℕ} (hn : 128  ≤  n) (hN : 2  ≤  N) (hb : N < 2^n)
       (t : ℕ) (h : SplitMachine.Trace n t) :
       ∃ xs ys b, (machine n (2*n)).config
           (NodeStateCircuit.pack [natBasis (n+1) N] [] false) t h=NodeStateCircuit.pack xs ys b ∧
         Good n N (2*n) xs ys := by
   …

   Mentions: OAI.ExactQuantumFactoring.SplitMachine.Trace, OAI.ExactQuantumFactoring.PhysicalNode.machine, OAI.ExactQuantumFactoring.PhysicalNode.Good

3. lemma OAI.ExactQuantumFactoring.PhysicalNode.Good.pending_dvd line 105
4. theorem OAI.ExactQuantumFactoring.PhysicalNode.query_safe line 110