OAI/Computability/QuantumFactoring/RawTrialDecoder.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.OrderTrial.rawAcceptNet line 21

   Source documentation

   Exact ordinary trial decoder, including the sampler's full workspace test, continued-fraction reconstruction, arithmetic validation, and all three retained coin tests. Its inputs are actual retained raw bits.

   def rawAcceptNet {k u s n : ℕ} (a m : BooleanNetwork k u)
       (r : BooleanNetwork k (rawWidth u s n)) : BooleanNetwork k 1 :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.OrderTrial.rawWidth

2. lemma OAI.ExactQuantumFactoring.OrderTrial.rawAcceptNet_value line 28
3. def OAI.ExactQuantumFactoring.OrderTrial.trialValueNet line 50
4. lemma OAI.ExactQuantumFactoring.OrderTrial.trialValueNet_value line 54
5. lemma OAI.ExactQuantumFactoring.OrderTrial.trialResult_getD_lt line 68
6. def OAI.ExactQuantumFactoring.OrderTrial.trialSmallValueNet line 80

   Source documentation

   Only VALID ordinary candidates are narrowed to n bits. This does not apply to the separately completed rare guess, whose whole transition word is kept.

   def trialSmallValueNet {k u s n : ℕ} (a m : BooleanNetwork k u)
       (r : BooleanNetwork k (rawWidth u s n)) : BooleanNetwork k n :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.OrderTrial.rawWidth

7. lemma OAI.ExactQuantumFactoring.OrderTrial.trialSmallValueNet_value line 83