OrderTrialLaw.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.OrderTrial.selectedSampleAmplitude line 17
Source documentation
Unnormalized joint amplitude after modular powering and the selected phase-transform block. The modular-power register is NOT copied before this interference sum.
```
noncomputable def selectedSampleAmplitude {G : Type*} [Group G]
    (Q k : ℕ) (a u : G) : ℂ := by
…
```
lemma OAI.ExactQuantumFactoring.OrderTrial.selectedSampleAmplitude_residue line 23
lemma OAI.ExactQuantumFactoring.OrderTrial.selectedSampleProbability_residue line 33
def OAI.ExactQuantumFactoring.OrderTrial.ValidCandidate line 41
Source documentation
The literal modular-power verification in all three trial modes.
```
def ValidCandidate {G : Type*} [Group G] (B : ℕ) (a : G) (d : ℕ) : Prop :=
…
```
lemma OAI.ExactQuantumFactoring.OrderTrial.ValidCandidate.order_dvd line 44
lemma OAI.ExactQuantumFactoring.OrderTrial.trueOrder_valid line 48
lemma OAI.ExactQuantumFactoring.OrderTrial.reduced_mass_sum line 54
Source documentation
Summing the exact per-reduced-label mass gives the prescribed true-order probability phi(r) lambda(r), including r=1 and its label j=0.
```
lemma reduced_mass_sum {n Q B d : ℕ} (hB : 0 < B) (hd : 0 < d) :
    (∑ j ∈ (Finset.range d).filter (fun j => Nat.Coprime j d),
      (firstModeMass n Q B d j + secondModeMass n Q B d j +
        thirdModeMass n Q B d j)) =
      (Nat.totient d : ℝ) * (prescribedMass d : ℝ) := by
…
```
Mentions: OAI.ExactQuantumFactoring.OrderTrial.firstModeMass, OAI.ExactQuantumFactoring.OrderTrial.secondModeMass, OAI.ExactQuantumFactoring.OrderTrial.thirdModeMass, OAI.ExactQuantumFactoring.OrderTrial.prescribedMass