OAI/Computability/QuantumFactoring/PhysicalOrderDecoder.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.resizeWord_eq_natBasis line 18
2. def OAI.ExactQuantumFactoring.OrderSlots.usableOn line 27
3. lemma OAI.ExactQuantumFactoring.OrderSlots.usableOn_value line 29
4. lemma OAI.ExactQuantumFactoring.OrderSlots.usableOn_count line 35
5. def OAI.ExactQuantumFactoring.OrderSlots.orderResultNet line 47

   Source documentation

   Every ordinary raw trial uses its actual tensor block. Nonempty candidates are validated before a shared, linear-size least-positive-candidate fold.

   def orderResultNet {k n : ℕ} (a m : BooleanNetwork k n)
       (raw : BooleanNetwork k (ordinaryWidth n)) : BooleanNetwork k n :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.OrderSlots.ordinaryWidth

6. lemma OAI.ExactQuantumFactoring.OrderSlots.orderResultNet_value line 51
7. def OAI.ExactQuantumFactoring.OrderSlots.ordinaryOn line 65
8. lemma OAI.ExactQuantumFactoring.OrderSlots.ordinaryOn_eval line 69
9. def OAI.ExactQuantumFactoring.OrderSlots.outputOn line 83

   Source documentation

   Completed output decoding keeps the FULL rare guessed transition word. No truncation, success flag, or later true-order certificate enters this decoder.

   def outputOn {k n : ℕ} (a m : BooleanNetwork k n) (raw : BooleanNetwork k (width n)) :
       BooleanNetwork k (Completion.transitionWidth n) :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.OrderSlots.width, OAI.ExactQuantumFactoring.Completion.transitionWidth

10. lemma OAI.ExactQuantumFactoring.OrderSlots.outputOn_eval line 88