OAI/Computability/QuantumFactoring/TransitionNetworks.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.TransitionWords.encodeNet line 21

   Source documentation

   Each field is wired into its fixed source layout, and the final unused word is explicitly zeroed. The cap K and all placements are independent of inputs.

   def encodeNet {k n K : ℕ} (f : Fin K → BooleanNetwork k n) : BooleanNetwork k (n*(K+1)) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.TransitionWords.encodeNet_eval line 26
3. lemma OAI.ExactQuantumFactoring.TransitionWords.encodeNet_count line 33