RetainedOrderTest.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.ExactQuantumFactoring.NodeMachine.retainedOrderFilter_exact line 22

Source documentation

Both actual usable slots and actual dummy slots, with the identical physical coin and retained guessed string in their respective branches.

theorem retainedOrderFilter_exact {N P : ℕ} (hn : 2 ≤ n) (t : ℕ)
    (a m : BooleanNetwork (M.width t) n) (raw : BooleanNetwork (M.width t) (OrderSlots.width n))
    (x : Basis c) (h : Trace n t) (r : OrderSlots.Result n)
    (hc : PhysicalTree.CompleteLog n N (M.dataLog x t h))
    (hP : P∈(M.dataLog x t h).map Prod.fst) (hP0 : P≠0)
    (hd : 2 ≤ (bitsValue (m.eval (M.encoded x t h))).toNat)
    (hdiv : (bitsValue (m.eval (M.encoded x t h))).toNat∣P)
    (hr : raw.eval (M.encoded x t h)=OrderSlots.layout n r) :
    (M.retainedOrderFilter t a m raw).eval (M.encoded x t h) 0=true ↔
      dataOrderPassed (trueData P) (a.eval (M.encoded x t h)) (m.eval (M.encoded x t h)) r := by
…

Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.OrderSlots.width, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.OrderSlots.Result, OAI.ExactQuantumFactoring.PhysicalTree.CompleteLog, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.OrderSlots.layout, OAI.ExactQuantumFactoring.dataOrderPassed, OAI.ExactQuantumFactoring.trueData