OAI/Computability/QuantumFactoring/TreeHistoryAccess.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.NodeMachine.previousNet line 21

   Source documentation

   Access only retained earlier wires. No history is recomputed.

   def previousNet (t : ℕ) : BooleanNetwork (M.width (t+1)) (M.width t) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. def OAI.ExactQuantumFactoring.NodeMachine.lastNodeNet line 24
3. lemma OAI.ExactQuantumFactoring.NodeMachine.previousNet_encoded line 28
4. lemma OAI.ExactQuantumFactoring.NodeMachine.lastNodeNet_encoded line 36
5. def OAI.ExactQuantumFactoring.NodeMachine.firstNodeNet line 46
6. def OAI.ExactQuantumFactoring.NodeMachine.firstRaw line 49
7. lemma OAI.ExactQuantumFactoring.NodeMachine.firstNodeNet_encoded line 52
8. lemma OAI.ExactQuantumFactoring.NodeMachine.first_passed line 59
9. lemma OAI.ExactQuantumFactoring.NodeMachine.firstNodeNet_count line 64