OAI/Computability/QuantumFactoring/RetainedSplitFilter.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NodeMachine.splitModulus line 24
2. def OAI.ExactQuantumFactoring.NodeMachine.splitList line 26
3. def OAI.ExactQuantumFactoring.NodeMachine.splitBase line 28
4. def OAI.ExactQuantumFactoring.NodeMachine.splitOrder line 30
5. def OAI.ExactQuantumFactoring.NodeMachine.splitActualFilter line 33
6. def OAI.ExactQuantumFactoring.NodeMachine.splitDummyFilter line 39
7. def OAI.ExactQuantumFactoring.NodeMachine.retainedSplitFilter line 45
8. lemma OAI.ExactQuantumFactoring.NodeMachine.splitModulus_eval line 50
9. lemma OAI.ExactQuantumFactoring.NodeMachine.splitList_eval line 55
10. lemma OAI.ExactQuantumFactoring.NodeMachine.splitBase_eval line 60
11. lemma OAI.ExactQuantumFactoring.NodeMachine.splitOrder_eval line 65
12. lemma OAI.ExactQuantumFactoring.NodeMachine.splitDummyFilter_exact line 71
13. theorem OAI.ExactQuantumFactoring.NodeMachine.retainedSplitFilter_exact line 87

    Source documentation

    The hard/ordinary/rare/dummy selection is on the actual retained split's modulus and coin strings. The table is the same final retained complete log.

    theorem retainedSplitFilter_exact {N P : ℕ} (hn : 128≤n) (t : ℕ)
        (raw : BooleanNetwork (M.width t) (FixedSplit.width n))
        (x : Basis c) (h : Trace n t) (q : Basis n) (r : UniversalSplit.Raw n)
        (hc : PhysicalTree.CompleteLog n N (M.dataLog x t h))
        (hP : P∈(M.dataLog x t h).map Prod.fst) (hP0 : P≠0)
        (hdiv : UniversalSplit.Hard (bitsValue q).toNat → (bitsValue q).toNat∣P)
        (hr : raw.eval (M.encoded x t h)=FixedSplit.encoding q r) :
        (M.retainedSplitFilter (by omega) t raw).eval (M.encoded x t h) 0=true ↔
          dataSplitPassed (trueData P) q (by omega) r := by
    …

    Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.FixedSplit.width, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.NodeMachine.Trace, OAI.ExactQuantumFactoring.UniversalSplit.Raw, OAI.ExactQuantumFactoring.PhysicalTree.CompleteLog, OAI.ExactQuantumFactoring.UniversalSplit.Hard, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.FixedSplit.encoding, OAI.ExactQuantumFactoring.dataSplitPassed, OAI.ExactQuantumFactoring.trueData