RetrospectiveTree.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactQuantumFactoring.PhysicalTree.verified_query_safe line 18
def OAI.ExactQuantumFactoring.NodeMachine.dataTests line 40
Source documentation
Read-only postprocessing of the retained actual history. Each node receives only the flat row data at its actual runtime label. Occurrences are retained; lookup selects the first matching verified record, not a factorization oracle.
```
noncomputable def dataTests (rows : List (ℕ×List ℕ)) (x : Basis c) (hn : 0<n) :
    (t : ℕ)→Trace n t→Prop
  | 0,_=>True
  | t+1,r=>dataTests rows x hn t r.1 ∧
    let q:=M.query.eval (M.config x t r.1)
…
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.NodeMachine.Trace
lemma OAI.ExactQuantumFactoring.PhysicalTree.dataTests_correct line 49
def OAI.ExactQuantumFactoring.PhysicalTree.accepted line 69
Source documentation
Literal event specification for completed-data retrospective checking. The Boolean implementation of the arithmetic and the whole polynomial-time compiler are separate obligations, not consequences of this definition.
```
noncomputable def accepted {n N : ℕ} (hn : 0<n) (r : NodeMachine.Trace n (2*n^2)) : Prop :=
…
```
Mentions: OAI.ExactQuantumFactoring.NodeMachine.Trace
theorem OAI.ExactQuantumFactoring.PhysicalTree.accepted_iff_passed line 77
Source documentation
Same-history retrospective equivalence, with the actual physical data tree and actual divisibility-safe node controller. Unverified factor data is rejected first; no comparison to a counterfactual run is used.
```
theorem accepted_iff_passed {n N : ℕ} (hn : 128 ≤ n) (hN : 2 ≤ N) (hb : N<2^n)
    (r : NodeMachine.Trace n (2*n^2)) :
    accepted (N:=N) (by omega) r ↔ (machine n).passed (initialQueue n N) (2*n^2) r := by
…
```
Mentions: OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.PhysicalTree.accepted, OAI.ExactQuantumFactoring.PhysicalTree.machine, OAI.ExactQuantumFactoring.PhysicalTree.initialQueue
theorem OAI.ExactQuantumFactoring.PhysicalTree.accepted_mass line 92
Source documentation
Exact accepted mass, after the actual complete-data checks. This is still an event theorem: using it as a physical phase flag requires the missing fully assembled retrospective Boolean network, rather than an arbitrary predicate.
```
theorem accepted_mass {n N : ℕ} (hn : 128 ≤ n) (hN : 2 ≤ N) (hb : N<2^n) :
    Exactness.outcomeMass (accepted (n:=n) (N:=N) (by omega))
…
```
Mentions: OAI.ExactQuantumFactoring.Exactness.outcomeMass, OAI.ExactQuantumFactoring.PhysicalTree.accepted