OAI/Computability/QuantumFactoring/ModularMultiply.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.BitArithmetic.mulMod line 15

   Source documentation

   Full double-width product followed by full double-width remainder, with no word overflow. The narrow remainder is valid because the modulus is a word.

   def mulMod {n w : ℕ} (a b m : BooleanNetwork n w) : BooleanNetwork n w :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.BitArithmetic.mulMod_count line 19
3. lemma OAI.ExactQuantumFactoring.BitArithmetic.mulMod_word line 27
4. def OAI.ExactQuantumFactoring.BitArithmetic.wordMux line 45

   Source documentation

   A word mux shares previously computed word outputs via fanout; it does not recompute the operand circuit separately at every bit.

   def wordMux {n w : ℕ} (c : BooleanNetwork n 1) (a b : BooleanNetwork n w) :
       BooleanNetwork n w :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

5. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordMux_eval line 51
6. lemma OAI.ExactQuantumFactoring.BitArithmetic.wordMux_count line 62