OAI/Computability/QuantumFactoring/NetworkEmissionCombinators.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NetworkEmission.NetEmits line 15

   Source documentation

   Exact, syntactic network emission. Pack budgets are internal certificates, not additional generator advice.

   def NetEmits {α : Type} (ea : α→List Bool) {n m : α→ℕ}
       (f : ∀x,BooleanNetwork (n x) (m x)) : Prop:=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.ofPack line 20
3. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.comp line 22
4. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.pair line 31
5. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.rewire line 40
6. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.identity line 48
7. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.select line 50
8. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.constant line 54
9. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.bit line 58
10. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.resize line 61
11. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.bnot line 64
12. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.band line 68
13. lemma OAI.ExactQuantumFactoring.NetworkEmission.NetEmits.wordConst line 74