OAI/Computability/QuantumFactoring/PhysicalTrialLaw.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.OrderTrial.recovered line 19
2. def OAI.ExactQuantumFactoring.OrderTrial.modeFirst line 24
3. def OAI.ExactQuantumFactoring.OrderTrial.modeSecond line 26
4. def OAI.ExactQuantumFactoring.OrderTrial.modeThird line 28
5. def OAI.ExactQuantumFactoring.OrderTrial.labelEvent line 31
6. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseScale_bounds line 34
7. lemma OAI.ExactQuantumFactoring.OrderTrial.first_mass line 41
8. lemma OAI.ExactQuantumFactoring.OrderTrial.second_mass line 65
9. lemma OAI.ExactQuantumFactoring.OrderTrial.third_mass line 83
10. theorem OAI.ExactQuantumFactoring.OrderTrial.labelEvent_mass line 102

    Source documentation

    True-order cancellation for the ACTUAL physical finite-gate experiment, with all unselected sampler amplitudes, guesses, and retention coins retained.

    theorem labelEvent_mass {w n s : ℕ} (hn : 1≤n) (hs : 2^(s+2)=(2^n)^16)
        (a m : Basis w) (hm : 2≤(bitsValue m).toNat) (u : (ZMod (bitsValue m).toNat)ˣ)
        (ha : ((bitsValue a).toNat : ZMod (bitsValue m).toNat)=(u : ZMod (bitsValue m).toNat))
        (hdB : orderOf u<2^n) (j : ℕ) (hj : j<orderOf u) (hcop : Nat.Coprime j (orderOf u)) :
        outcomeMass (labelEvent s n a m (orderOf u) j) (rawState s n a m)=
          (prescribedMass (orderOf u):ℝ) := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.OrderTrial.labelEvent, OAI.ExactQuantumFactoring.OrderTrial.rawState, OAI.ExactQuantumFactoring.OrderTrial.prescribedMass