OAI/Computability/QuantumFactoring/OrderSamplerMass.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.OrderTrial.powerOrbit line 18

   Source documentation

   Distinct powers in one period; this is an embedding, not an oracle for r.

   def powerOrbit {G : Type*} [Group G] (a : G) : Fin (orderOf a)→G := fun t => a^t.val

2. lemma OAI.ExactQuantumFactoring.OrderTrial.powerOrbit_injective line 19
3. lemma OAI.ExactQuantumFactoring.OrderTrial.selectedSampleAmplitude_outside line 24
4. lemma OAI.ExactQuantumFactoring.OrderTrial.selectedSampleProbability_sum line 34
5. def OAI.ExactQuantumFactoring.OrderTrial.natBasis line 55

   Source documentation

   Exact bit representation used for modular-power values.

   def natBasis (w z : ℕ) : Basis w := fun i => (BitVec.ofNat w z).getLsbD i.val

   Mentions: OAI.ExactQuantumFactoring.Basis

6. lemma OAI.ExactQuantumFactoring.OrderTrial.natBasis_value line 56
7. lemma OAI.ExactQuantumFactoring.OrderTrial.natBasis_injectiveOn line 59
8. def OAI.ExactQuantumFactoring.OrderTrial.unitWord line 65

   Source documentation

   Embed all units into the physical modular-power register, when m<2^w.

   def unitWord {m w : ℕ} (u : (ZMod m)ˣ) : Basis w := natBasis w (u : ZMod m).val

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

9. lemma OAI.ExactQuantumFactoring.OrderTrial.unitWord_value line 66
10. lemma OAI.ExactQuantumFactoring.OrderTrial.unitWord_injective line 69
11. lemma OAI.ExactQuantumFactoring.OrderTrial.nat_pow_eq_unit line 77
12. lemma OAI.ExactQuantumFactoring.OrderTrial.nat_pow_eq_word_iff line 82
13. theorem OAI.ExactQuantumFactoring.OrderTrial.sampler_unit_amplitude line 90

    Source documentation

    The physical amplitude, at any encoded unit, equals the group-theoretic coherent residue sum. No early classical measurement is used here.

    theorem sampler_unit_amplitude {w s : ℕ} (a m : Basis w) (y : Basis (s+2))
        (hm : 2≤(bitsValue m).toNat) (u v : (ZMod (bitsValue m).toNat)ˣ)
        (ha : ((bitsValue a).toNat : ZMod (bitsValue m).toNat)=(u : ZMod (bitsValue m).toNat)) :
        (programMatrix (OrderSample.completeSampler w s)).mulVec
          (basisVector (OrderSample.word a m (fun _=>false) (fun _=>false)))
          (OrderSample.word a m y (unitWord (w:=w) v))=
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.OrderSample.completeSampler, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.OrderSample.word, OAI.ExactQuantumFactoring.OrderTrial.unitWord

14. lemma OAI.ExactQuantumFactoring.OrderTrial.outcomeMass_range line 106
15. lemma OAI.ExactQuantumFactoring.OrderTrial.sampler_word_injective line 130
16. def OAI.ExactQuantumFactoring.OrderTrial.samplerState line 137
17. lemma OAI.ExactQuantumFactoring.OrderTrial.sampler_outside_units line 141
18. theorem OAI.ExactQuantumFactoring.OrderTrial.sampler_selected_bin_mass line 162

    Source documentation

    The complete physical selected-bin probability is the sum of the literal residue probabilities at the TRUE order. False labels are not identified with artificial probabilities.

    theorem sampler_selected_bin_mass {w s : ℕ} (a m : Basis w) (y : Basis (s+2))
        (hm : 2≤(bitsValue m).toNat) (u : (ZMod (bitsValue m).toNat)ˣ)
        (ha : ((bitsValue a).toNat : ZMod (bitsValue m).toNat)=(u : ZMod (bitsValue m).toNat))
        (j : ℕ) (hy : Triangular.outputNumber y=bin (2^(s+2)) (orderOf u) j) :
        outcomeMass (fun z => z∈Set.range (OrderSample.word a m y)) (samplerState a m)=
          ∑ t : Fin (orderOf u), residueProbability (2^(s+2)) (orderOf u) j t.val := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.Triangular.outputNumber, OAI.ExactQuantumFactoring.OrderTrial.bin, OAI.ExactQuantumFactoring.OrderSample.word, OAI.ExactQuantumFactoring.OrderTrial.samplerState, OAI.ExactQuantumFactoring.OrderTrial.residueProbability