OAI/Computability/QuantumFactoring/BitStackProcedures.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BitStackProgram.Runs.length_le line 13
2. structure OAI.ExactQuantumFactoring.BitStackProgram.Procedure line 43

   Source documentation

   A completely explicit finite-state Boolean-stack subroutine, with the same clean input/output convention as the frozen TM2 uniformity target.

   structure Procedure {α β : Type} (ea : α → List Bool) (eb : β → List Bool) (f : α → β) where
   …

3. lemma OAI.ExactQuantumFactoring.BitStackProgram.Procedure.output_length_le line 58
4. def OAI.ExactQuantumFactoring.BitStackProgram.Procedure.toTM2 line 67
5. lemma OAI.ExactQuantumFactoring.BitStackProgram.Procedure.toTM2_finite line 88