OAI/Computability/QuantumFactoring/LabelValidationCircuit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.OrderTrial.labelValidNet line 20

   Source documentation

   Every returned denominator, in EVERY mode, undergoes the full arithmetic check. No primality or order oracle appears in the network.

   def labelValidNet {k w : ℕ} (n : ℕ) (a m d j : BooleanNetwork k w) : BooleanNetwork k 1 :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.OrderTrial.labelValidNet_value line 27
3. lemma OAI.ExactQuantumFactoring.OrderTrial.labelValidNet_count line 39