VerifiedTreeCompletion.lean`

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExactQuantumFactoring.PhysicalTree.verified_queue_invariant line 22
Source documentation
On any retrospectively verified 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 verified_queue_invariant {n N : ℕ} (hn : 128 ≤ n) (hN : 2 ≤ N) (hb : N < 2^n)
    (t : ℕ) (h : NodeMachine.Trace n t)
    (hp : (machine n).verified (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.verified_complete line 80
Source documentation
The full actual tree controller terminates in the fixed 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 verified_complete {n N : ℕ} (hn : 128 ≤ n) (hN : 2 ≤ N) (hb : N < 2^n)
    (h : NodeMachine.Trace n (2*n^2))
    (hp : (machine n).verified (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
theorem OAI.ExactQuantumFactoring.PhysicalTree.passed_verified line 90
Source documentation
Every good chronological run passes the literal complete-node verification. The converse is deliberately NOT asserted: local filters still must be checked.
```
theorem passed_verified {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).verified (initialQueue n N) t h := by
…
```
Mentions: OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.initialQueue