PhysicalTreeCompletion.lean`

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.PhysicalTree.machine line 22
def OAI.ExactQuantumFactoring.PhysicalTree.initialQueue line 23
theorem OAI.ExactQuantumFactoring.PhysicalTree.queue_invariant line 29
Source documentation
On the actual all-passed raw history, the literal physical pending queue is exactly the remaining canonical occurrence preorder. This is a proof invariant, not a precomputed queue or advice to the circuit.
```
theorem queue_invariant {n N : ℕ} (hn : 128 ≤ n) (hN : 2 ≤ N) (hb : N < 2^n)
    (t : ℕ) (h : NodeMachine.Trace n t)
    (hp : (machine n).passed (initialQueue n N) t h) :
    (machine n).config (initialQueue n N) t h=
      stackEncoding (capacity n) n (canonicalWords n (AuxiliaryTree.run t [N])) := by
…
```
Mentions: OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.initialQueue, OAI.ExactQuantumFactoring.PhysicalTree.capacity, OAI.ExactQuantumFactoring.AuxiliaryTree.run
theorem OAI.ExactQuantumFactoring.PhysicalTree.complete line 87
Source documentation
The full actual tree controller terminates in the source's polynomial occurrence cap, with no truncation on a passing history. The circuit nevertheless has fixed worst-case dimensions on all other histories as well.
```
theorem complete {n N : ℕ} (hn : 128 ≤ n) (hN : 2 ≤ N) (hb : N < 2^n)
    (h : NodeMachine.Trace n (2*n^2))
    (hp : (machine n).passed (initialQueue n N) (2*n^2) h) :
    (machine n).config (initialQueue n N) (2*n^2) h=stackEncoding (capacity n) n [] := by
…
```
Mentions: OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.initialQueue, OAI.ExactQuantumFactoring.PhysicalTree.capacity