PhysicalNodeCompletion.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactQuantumFactoring.PhysicalNode.config_good line 19
theorem OAI.ExactQuantumFactoring.PhysicalNode.complete line 57
Source documentation
Every passing actual history of the literal 2n-clock machine ends in a complete prime list, without sticky failure. The input and all next queries are actual measured-word encodings, not an oracle call to mathematical factorization.
```
theorem complete {n N : ℕ} (hn : 128 ≤ n) (hN : 2 ≤ N) (hb : N<2^n)
    (h : SplitMachine.Trace n (2*n))
    (hp : (machine n (2*n)).passed (NodeStateCircuit.pack [natBasis (n+1) N] [] false) (2*n) h) :
    ∃ ys, (machine n (2*n)).config (NodeStateCircuit.pack [natBasis (n+1) N] [] false) (2*n) h=
      NodeStateCircuit.pack [] ys false ∧
      (∀ p ∈ values ys,p.Prime) ∧ (values ys).prod=N ∧ ys.length<n := by
…
```
Mentions: OAI.ExactQuantumFactoring.SplitMachine.Trace, OAI.ExactQuantumFactoring.PhysicalNode.machine, OAI.ExactQuantumFactoring.PhysicalNode.values