OAI/Computability/QuantumFactoring/ExpressionPredicates.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NatExpr.testEq line 15
2. lemma OAI.ExactQuantumFactoring.NatExpr.eval_testEq line 17
3. def OAI.ExactQuantumFactoring.NatExpr.isOne line 24

   Source documentation

   A total exact predicate compiler. All intermediate words are widened from an explicit expression-derived bound, including on rejected inputs.

   def isOne {k b : ℕ} (e : NatExpr v) (vars : v → BooleanNetwork k b) : BooleanNetwork k 1 :=
   …

   Mentions: OAI.ExactQuantumFactoring.NatExpr, OAI.ExactQuantumFactoring.BooleanNetwork

4. lemma OAI.ExactQuantumFactoring.NatExpr.isOne_eval line 26
5. lemma OAI.ExactQuantumFactoring.NatExpr.isOne_count line 33