OAI/Computability/QuantumFactoring/TrialControlCircuit.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. inductive OAI.ExactQuantumFactoring.OrderTrial.DecodeVar line 18
2. def OAI.ExactQuantumFactoring.OrderTrial.decodeVars line 20
3. def OAI.ExactQuantumFactoring.OrderTrial.firstRetNet line 23
4. def OAI.ExactQuantumFactoring.OrderTrial.secondRetNet line 26
5. def OAI.ExactQuantumFactoring.OrderTrial.thirdRetNet line 29
6. lemma OAI.ExactQuantumFactoring.OrderTrial.firstRetNet_value line 33
7. lemma OAI.ExactQuantumFactoring.OrderTrial.secondRetNet_value line 40
8. lemma OAI.ExactQuantumFactoring.OrderTrial.thirdRetNet_value line 49
9. def OAI.ExactQuantumFactoring.OrderTrial.trialAcceptOn line 59

   Source documentation

   Mode guards are outside the rational computations. In particular malformed labels and residue guesses cannot turn an irrelevant retention into acceptance.

   def trialAcceptOn {k w : ℕ} (n : ℕ) (a m mode d j t c : BooleanNetwork k w)
       (selected : BooleanNetwork k 1) : BooleanNetwork k 1 :=
   …

   Mentions: OAI.ExactQuantumFactoring.BooleanNetwork

10. lemma OAI.ExactQuantumFactoring.OrderTrial.trialAcceptOn_value line 68
11. lemma OAI.ExactQuantumFactoring.OrderTrial.labelEvent_self line 99

    Source documentation

    At the actually recovered/guessed pair, pair equality checks simplify but sampler scratch selection and the actual recorded retention coin do not.

    lemma labelEvent_self {u s n : ℕ} (a m : Basis u) (r : Raw u s n) :
        labelEvent s n a m (labelPair s n r).1 (labelPair s n r).2 r ↔
          (((bitsValue r.1).toNat<2 ∧ SampleSelected a m r.2.1 ∧
            Retains (firstRetention n (labelPair s n r).1 (labelPair s n r).2) r.2.2.2.2.2) ∨
           ((bitsValue r.1).toNat=2 ∧ (bitsValue r.2.2.2.2.1).toNat<(labelPair s n r).1 ∧
            Retains (discrepancyRetention n (labelPair s n r).1 (labelPair s n r).2
              (bitsValue r.2.2.2.2.1).toNat) r.2.2.2.2.2) ∨
           ((bitsValue r.1).toNat=3 ∧
            Retains (remainderRetention n (labelPair s n r).1 (labelPair s n r).2) r.2.2.2.2.2)) := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.OrderTrial.Raw, OAI.ExactQuantumFactoring.OrderTrial.labelEvent, OAI.ExactQuantumFactoring.OrderTrial.labelPair, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.OrderTrial.SampleSelected, OAI.ExactQuantumFactoring.OrderTrial.Retains, OAI.ExactQuantumFactoring.OrderTrial.firstRetention, OAI.ExactQuantumFactoring.OrderTrial.discrepancyRetention, OAI.ExactQuantumFactoring.OrderTrial.remainderRetention