OAI/Computability/QuantumFactoring/NodeSplitMachine.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactQuantumFactoring.PhysicalNode.configWidth line 21
2. def OAI.ExactQuantumFactoring.PhysicalNode.query line 22
3. def OAI.ExactQuantumFactoring.PhysicalNode.update line 24
4. def OAI.ExactQuantumFactoring.PhysicalNode.machine line 28
5. def OAI.ExactQuantumFactoring.PhysicalNode.decoded line 29
6. lemma OAI.ExactQuantumFactoring.PhysicalNode.query_pack line 32
7. lemma OAI.ExactQuantumFactoring.PhysicalNode.query_value line 37
8. lemma OAI.ExactQuantumFactoring.PhysicalNode.decoded_value line 41
9. lemma OAI.ExactQuantumFactoring.PhysicalNode.next_eq line 46
10. lemma OAI.ExactQuantumFactoring.PhysicalNode.next_prime line 61
11. lemma OAI.ExactQuantumFactoring.PhysicalNode.next_split line 70

    Source documentation

    A passed actual split advances the bounded node stack. Its inputs are the runtime stack top and this very clock tick's retained raw outcome.

    lemma next_split {n s : ℕ} (hn : 128 ≤ n) (a : Basis (n+1)) (xs ys : List (Basis (n+1)))
        (b : Bool) (hx : xs.length ≤ s) (ha : 2 ≤ (bitsValue a).toNat) (hb : (bitsValue a).toNat < 2^n)
        (hp : ¬(bitsValue a).toNat.Prime) (r : FixedSplit.Raw n)
        (hr : UniversalSplit.passed ((query n s).eval (NodeStateCircuit.pack (a::xs) ys b)) r) :
        let q := (query n s).eval (NodeStateCircuit.pack (a::xs) ys b)
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.FixedSplit.Raw, OAI.ExactQuantumFactoring.UniversalSplit.passed, OAI.ExactQuantumFactoring.PhysicalNode.query