OAI/Computability/QuantumFactoring/NodeProgress.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.PhysicalNode.values line 19
2. lemma OAI.ExactQuantumFactoring.PhysicalNode.values_nil line 20
3. lemma OAI.ExactQuantumFactoring.PhysicalNode.values_cons line 21
4. lemma OAI.ExactQuantumFactoring.PhysicalNode.length_le_weight line 24
5. structure OAI.ExactQuantumFactoring.PhysicalNode.Good line 33
6. lemma OAI.ExactQuantumFactoring.PhysicalNode.Good.length_le line 39
7. lemma OAI.ExactQuantumFactoring.PhysicalNode.next_nil line 49
8. theorem OAI.ExactQuantumFactoring.PhysicalNode.next_good line 56

   Source documentation

   One literal machine step consumes one unit of the genuine prime-factor weight whenever pending work is nonempty. Empty work stays empty.

   theorem next_good {n N s k : ℕ} (hn : 128 ≤ n) (hk : k ≤ s)
       (xs ys : List (Basis (n+1))) (h : Good n N (k+1) xs ys) (r : FixedSplit.Raw n)
       (hr : UniversalSplit.passed ((query n s).eval (NodeStateCircuit.pack xs ys false)) r) :
       ∃ xs' ys', (machine n s).next (NodeStateCircuit.pack xs ys false) r=
         NodeStateCircuit.pack xs' ys' false ∧ Good n N k xs' ys' := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.PhysicalNode.Good, OAI.ExactQuantumFactoring.FixedSplit.Raw, OAI.ExactQuantumFactoring.UniversalSplit.passed, OAI.ExactQuantumFactoring.PhysicalNode.query, OAI.ExactQuantumFactoring.PhysicalNode.machine