OAI/Computability/QuantumFactoring/OrderCandidateLaw.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.outcomeMass_finite_union line 19
2. def OAI.ExactQuantumFactoring.OrderTrial.ValidLabel line 43
3. def OAI.ExactQuantumFactoring.OrderTrial.labelPair line 46
4. lemma OAI.ExactQuantumFactoring.OrderTrial.labelEvent_pair line 51
5. lemma OAI.ExactQuantumFactoring.OrderTrial.labelEvent_unique line 63
6. def OAI.ExactQuantumFactoring.OrderTrial.trialResult line 71

   Source documentation

   Arithmetic validation is performed in every mode, before any returned candidate is used. The plain scan/guess never serves as an order certificate.

   noncomputable def trialResult {w : ℕ} (s n : ℕ) (a m : Basis w) (x : Raw w s n) : Option ℕ := by
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.OrderTrial.Raw

7. lemma OAI.ExactQuantumFactoring.OrderTrial.trialResult_some line 77
8. lemma OAI.ExactQuantumFactoring.OrderTrial.validLabel_order_dvd line 96
9. lemma OAI.ExactQuantumFactoring.OrderTrial.true_validLabel line 105
10. lemma OAI.ExactQuantumFactoring.OrderTrial.trialResult_multiple line 113
11. theorem OAI.ExactQuantumFactoring.OrderTrial.trialResult_mass line 123

    Source documentation

    The physical, validated order trial has the manuscript's exact true-order mass phi(r)*lambda(r). False candidates remain in the recorded history.

    theorem trialResult_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) :
        outcomeMass (fun x => trialResult s n a m x=some (orderOf u)) (rawState s n a m)=
          (Nat.totient (orderOf u):ℝ)*(prescribedMass (orderOf u):ℝ) := by
    …

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

12. lemma OAI.ExactQuantumFactoring.OrderTrial.actual_trial_lower line 155