OAI/Computability/QuantumFactoring/BitStackBinaryBasics.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BitStackProgram.binaryValue_append line 12
2. lemma OAI.ExactQuantumFactoring.BitStackProgram.bigEndian_value line 20
3. lemma OAI.ExactQuantumFactoring.BitStackProgram.double_bits_length line 30
4. lemma OAI.ExactQuantumFactoring.BitStackProgram.doubleOne_bits_length line 34
5. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.double line 38
6. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.doubleOne line 72
7. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.normalize line 76

   Source documentation

   Canonicalize a binary word, charging a linear-growth bit fold.

   noncomputable def normalize : Procedure (id : List Bool→List Bool) Nat.bits binaryValue := by
   …

   Mentions: OAI.ExactQuantumFactoring.BitStackProgram.Procedure, OAI.ExactQuantumFactoring.BitStackProgram.binaryValue