OAI/Computability/QuantumFactoring/RuntimeListPreparation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.listMaskNet line 22

   Source documentation

   Compute ceil-log activation bits by bounded comparisons. The constant 2^i fits n bits, and the circuit is polynomial on invalid inputs too.

   def listMaskNet (n : ℕ) : BooleanNetwork n n :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.listMaskNet_eval line 25
3. lemma OAI.ExactQuantumFactoring.listMaskNet_count line 34
4. def OAI.ExactQuantumFactoring.padBits line 41
5. lemma OAI.ExactQuantumFactoring.padBits_at line 44
6. lemma OAI.ExactQuantumFactoring.padBits_injective line 48
7. lemma OAI.ExactQuantumFactoring.padBits_range line 54
8. lemma OAI.ExactQuantumFactoring.prefixFair_encode line 67
9. lemma OAI.ExactQuantumFactoring.maskedList_state line 80

   Source documentation

   Runtime active-width preparation, stated as an exact physical program column over the source's b=ceil(log₂m) fair state.

   lemma maskedList_state (n : ℕ) (m : Basis n) :
       (programMatrix (maskedPrefix n n le_rfl)).mulVec
         (basisVector (Fin.append ((listMaskNet n).eval m) (fun _ => false)))=
         encodeState (fun y => Fin.append ((listMaskNet n).eval m)
           (padBits (Nat.clog_le_of_le_pow (bitsValue m).isLt.le) y))
           (fairState (Nat.clog 2 (bitsValue m).toNat)) := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.maskedPrefix, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.listMaskNet, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.padBits, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.fairState

10. lemma OAI.ExactQuantumFactoring.padBits_value line 90