OAI/Computability/QuantumFactoring/FlatLookupCircuit.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.lookupWordNet line 20

   Source documentation

   Fixed-capacity, first-match read-only lookup. Every iteration is an explicit Boolean network; malformed/missing labels use the zero word.

   def lookupWordNet {k q w : ℕ} (query : BooleanNetwork k q) :
       List (BooleanNetwork k q × BooleanNetwork k w)→BooleanNetwork k w
     | []=>wordConstant 0
     | a::as=>wordMux (equalOn query a.1) a.2 (lookupWordNet query as)

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

2. def OAI.ExactQuantumFactoring.lookupWord line 25
3. lemma OAI.ExactQuantumFactoring.lookupWordNet_value line 29
4. lemma OAI.ExactQuantumFactoring.lookupWordNet_count line 44
5. def OAI.ExactQuantumFactoring.NodeMachine.logNets line 64

   Source documentation

   The rows are at their true retained locations. This construction has no quantum conditioning and does not evaluate a factorization operation.

   def logNets : (t : ℕ)→List (BooleanNetwork (M.width t) n ×
       BooleanNetwork (M.width t) (tensorWidth n n))
     | 0=>[]
     | t+1=>(M.rowQuery t,(M.lastNodeNet t).comp (PhysicalTree.nodeResult n))::
         ((logNets t).map (fun r=>((M.previousNet t).comp r.1,(M.previousNet t).comp r.2)))

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.tensorWidth, OAI.ExactQuantumFactoring.PhysicalTree.nodeResult

6. lemma OAI.ExactQuantumFactoring.NodeMachine.logNets_length line 70
7. lemma OAI.ExactQuantumFactoring.NodeMachine.logNets_counts line 75
8. lemma OAI.ExactQuantumFactoring.NodeMachine.logNets_values line 90