NodeStateFailure.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.step_failure line 20
Source documentation
Failed candidates leave genuine pending factors unchanged and only set the sticky verifier bit. They cannot introduce an unrelated query into the log.
```
lemma step_failure {s w : ℕ} (hw : 128 ≤ w) (a d : Basis w)
    (xs ys : List (Basis w)) (b : Bool) (hx : xs.length ≤ s)
    (ha : 2 ≤ (bitsValue a).toNat) (hp : ¬(bitsValue a).toNat.Prime)
    (hd : ¬ProperDivisor (bitsValue a).toNat (bitsValue d).toNat) :
    (step s w).eval (Fin.append (pack (a::xs) ys b) d)=pack (a::xs) ys true := by
…
```
Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.step, OAI.ExactQuantumFactoring.BitArithmetic.NodeStateCircuit.pack