OAI/Computability/QuantumFactoring/SamplerLabels.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.OrderTrial.sampleY line 15
2. def OAI.ExactQuantumFactoring.OrderTrial.sampleU line 17
3. lemma OAI.ExactQuantumFactoring.OrderTrial.sampleY_word line 20
4. lemma OAI.ExactQuantumFactoring.OrderTrial.sampleU_word line 26
5. def OAI.ExactQuantumFactoring.OrderTrial.SampleSelected line 33

   Source documentation

   Selected phase block, with every workspace bit accounted for. The input copies are compared to their retained read-only values.

   def SampleSelected {w b : ℕ} (a m : Basis w) (x : Basis (OrderSample.width w b)) : Prop :=
   …

   Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.OrderSample.width

6. lemma OAI.ExactQuantumFactoring.OrderTrial.sampleSelected_word line 36
7. lemma OAI.ExactQuantumFactoring.OrderTrial.sampleY_number_injective line 40
8. lemma OAI.ExactQuantumFactoring.OrderTrial.natBasis_outputNumber line 47
9. lemma OAI.ExactQuantumFactoring.OrderTrial.scanPairs_eq_iff line 50
10. lemma OAI.ExactQuantumFactoring.OrderTrial.selected_recovered_label line 62
11. theorem OAI.ExactQuantumFactoring.OrderTrial.sampler_recovered_label_mass line 90

    Source documentation

    Recovery and selected-block checking are now linked to the ACTUAL physical bin mass, without enumerating bins or residues in the circuit.

    theorem sampler_recovered_label_mass {w b s B : ℕ} (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))
        (hB : B^2≤2^(b+2)) (hs : 2^(b+2)<2^s) (hdB : orderOf u<B)
        (j : ℕ) (hj : j<orderOf u) (hcop : Nat.Coprime j (orderOf u)) :
        Exactness.outcomeMass (fun x : Basis (OrderSample.width w (b+2)) => SampleSelected a m x ∧
          scanPairs (2^(b+2)) B (Triangular.outputNumber (sampleY x)) (2*s+1)=(orderOf u,j))
          (samplerState (s:=b) a m)=
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.Exactness.outcomeMass, OAI.ExactQuantumFactoring.OrderSample.width, OAI.ExactQuantumFactoring.OrderTrial.SampleSelected, OAI.ExactQuantumFactoring.OrderTrial.scanPairs, OAI.ExactQuantumFactoring.Triangular.outputNumber, OAI.ExactQuantumFactoring.OrderTrial.sampleY, OAI.ExactQuantumFactoring.OrderTrial.samplerState