OAI/Computability/QuantumFactoring/RetainedNodeFilter.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NodeMachine.nodePrefixFilter line 23
2. def OAI.ExactQuantumFactoring.NodeMachine.retainedNodeFilter line 29
3. lemma OAI.ExactQuantumFactoring.NodeMachine.nodePrefixFilter_passed line 33
4. theorem OAI.ExactQuantumFactoring.NodeMachine.retainedNodeFilter_passed line 81

   Source documentation

   Every split in the actual retained node history is tested against the final read-only verified table. No fresh random experiment or ideal flag is inserted.

   theorem retainedNodeFilter_passed {N : ℕ} (hn : 128≤n) (T : ℕ)
       (raw : BooleanNetwork (M.width T) (NodeKernel.width n))
       (x : Basis c) (h : Trace n T) (q : Basis n) (r : NodeKernel.Raw n)
       (hc : PhysicalTree.CompleteLog n N (M.dataLog x T h))
       (hq : (bitsValue q).toNat=0 ∨ 2≤(bitsValue q).toNat)
       (hP : (bitsValue q).toNat≠0 → (bitsValue q).toNat∈(M.dataLog x T h).map Prod.fst)
       (hr : raw.eval (M.encoded x T h)=NodeKernel.encoding q r) :
       (M.retainedNodeFilter (by omega) T raw).eval (M.encoded x T h) 0=true ↔ NodeKernel.passed q r :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.NodeKernel.width, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.NodeKernel.Raw, OAI.ExactQuantumFactoring.PhysicalTree.CompleteLog, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.NodeKernel.encoding, OAI.ExactQuantumFactoring.NodeKernel.passed