OAI/Computability/QuantumFactoring/ProgressionEvaluation.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Constant-length exact evaluation of the selected arithmetic progression. The exponentially many progression points are replaced by seven truncated arithmetic sums. This is the explicit arithmetic behind source Lemma 4.1.

  1. def OAI.ExactQuantumFactoring.OrderTrial.linearSum line 17

    Source documentation

    Five fixed terms, of which only the constant and linear ones are nonzero.

    def linearSum (a b : ℚ) (lo hi : ℕ) : ℚ :=
…
  2. lemma OAI.ExactQuantumFactoring.OrderTrial.linearSum_correct line 20
  3. def OAI.ExactQuantumFactoring.OrderTrial.rampSum line 28

    Source documentation

    A ramp can change sign only once along an arithmetic progression.

    def rampSum (a b : ℚ) (M : ℕ) : ℚ :=
…
  4. lemma OAI.ExactQuantumFactoring.OrderTrial.sum_ramp_filter_nonneg line 33
  5. lemma OAI.ExactQuantumFactoring.OrderTrial.sum_ramp_filter_pos line 43
  6. lemma OAI.ExactQuantumFactoring.OrderTrial.rampSum_correct line 53
  7. def OAI.ExactQuantumFactoring.OrderTrial.phaseSumRe line 74

    Source documentation

    The real coordinate of the seven-ramp spline derivative summed exactly.

    def phaseSumRe (a b : ℚ) (M : ℕ) : ℚ :=
…
  8. def OAI.ExactQuantumFactoring.OrderTrial.phaseSumIm line 78
  9. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseSumRe_correct line 83
  10. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseSumIm_correct line 94
  11. lemma OAI.ExactQuantumFactoring.OrderTrial.phaseSum_correct line 105
  12. def OAI.ExactQuantumFactoring.OrderTrial.sampleOffset line 127

    Source documentation

    Offset and slope are rational values of polynomial bit length, evaluated using the arithmetic nearest-bin rule rather than any transcendental oracle.

    def sampleOffset (Q d j t : ℕ) : ℚ :=
…
  13. def OAI.ExactQuantumFactoring.OrderTrial.sampleSlope line 130
  14. lemma OAI.ExactQuantumFactoring.OrderTrial.sampleLine_cast line 132
  15. lemma OAI.ExactQuantumFactoring.OrderTrial.sampleLine_bounds line 139
  16. def OAI.ExactQuantumFactoring.OrderTrial.fastResidueProbability line 163

    Source documentation

    Constant-piece rational P: seven ramp sums, hence no loop of length Q or d.

    def fastResidueProbability (Q d j t : ℕ) : ℚ :=
…
  17. lemma OAI.ExactQuantumFactoring.OrderTrial.residueAmplitude_fast line 169
  18. lemma OAI.ExactQuantumFactoring.OrderTrial.fastResidueProbability_correct line 181
  19. lemma OAI.ExactQuantumFactoring.OrderTrial.fastResidueProbability_eq line 189