OAI/Computability/QuantumFactoring/FactoringRelabel.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.relocateVal line 18

   Source documentation

   Move the physical input after the branch bit to the front, and place the readout immediately after the true input. The retained history is permuted, never erased or initialized with input-dependent advice.

   def relocateVal (A m ℓ i : ℕ) : ℕ :=
   …

2. lemma OAI.ExactQuantumFactoring.relocateVal_lt line 22
3. lemma OAI.ExactQuantumFactoring.relocateVal_injective line 27
4. def OAI.ExactQuantumFactoring.relocate line 37
5. lemma OAI.ExactQuantumFactoring.relocate_input line 43
6. lemma OAI.ExactQuantumFactoring.relocate_output line 50
7. lemma OAI.ExactQuantumFactoring.shiftedInput_pad line 58