PhysicalDataLog.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.NodeMachine.dataLog line 22
Source documentation
Projection of the actual retained record, including dummy rows. No true factorization is used in constructing this projection.
```
def dataLog (x : Basis c) : (t : ℕ)→Trace n t→List (ℕ×List ℕ)
  | 0,_=>[]
  | t+1,h=>
    let q:=M.query.eval (M.config x t h.1)
…
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.NodeMachine.Trace
lemma OAI.ExactQuantumFactoring.NodeMachine.dataLog_length line 28
lemma OAI.ExactQuantumFactoring.NodeMachine.dataLog_correct line 32
lemma OAI.ExactQuantumFactoring.PhysicalTree.verified_query_value line 44
lemma OAI.ExactQuantumFactoring.PhysicalTree.verified_dataLog_labels line 69
Source documentation
The labels on the actual verified physical history are exactly the occurrence-preserving canonical traversal, including its zero padding.
```
lemma verified_dataLog_labels {n N : ℕ} (hn : 128 ≤ n) (hN : 2 ≤ N) (hb : N < 2^n)
    (t : ℕ) (h : NodeMachine.Trace n t)
    (hv : (machine n).verified (initialQueue n N) t h) :
    ((machine n).dataLog (initialQueue n N) t h).map Prod.fst=AuxiliaryTree.seen [N] t := by
…
```
Mentions: OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.initialQueue, OAI.ExactQuantumFactoring.AuxiliaryTree.seen
def OAI.ExactQuantumFactoring.PhysicalTree.CompleteLog line 84
Source documentation
Concrete flat complete-data condition sufficient for retrospective lookup: root present, every required child present, and every non-dummy row a complete prime factorization. Equal labels from different parents are NOT collapsed.
```
def CompleteLog (n N : ℕ) (rows : List (ℕ×List ℕ)) : Prop :=
…
```
theorem OAI.ExactQuantumFactoring.PhysicalTree.verified_complete_log line 89