OAI/Computability/QuantumFactoring/RetentionDenominators.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

Explicit, uniform O(n) fair-bit lengths for every order-trial retention. Mere dyadicity would not bound the worst-case circuit cost.

  1. def OAI.ExactQuantumFactoring.OrderTrial.DyadicAt line 15
  2. lemma OAI.ExactQuantumFactoring.OrderTrial.DyadicAt.integer line 17
  3. lemma OAI.ExactQuantumFactoring.OrderTrial.DyadicAt.mono line 21
  4. lemma OAI.ExactQuantumFactoring.OrderTrial.DyadicAt.add line 28
  5. lemma OAI.ExactQuantumFactoring.OrderTrial.DyadicAt.sub line 32
  6. lemma OAI.ExactQuantumFactoring.OrderTrial.DyadicAt.mul line 36
  7. lemma OAI.ExactQuantumFactoring.OrderTrial.DyadicAt.int_mul line 43
  8. lemma OAI.ExactQuantumFactoring.OrderTrial.majorant_at line 48
  9. lemma OAI.ExactQuantumFactoring.OrderTrial.majorantSum_at line 56
  10. lemma OAI.ExactQuantumFactoring.OrderTrial.probability_at line 63
  11. lemma OAI.ExactQuantumFactoring.OrderTrial.coefficient_at line 71
  12. lemma OAI.ExactQuantumFactoring.OrderTrial.lambda_at line 72
  13. lemma OAI.ExactQuantumFactoring.OrderTrial.remainder_at line 75
  14. def OAI.ExactQuantumFactoring.OrderTrial.discrepancyRetention line 84
  15. def OAI.ExactQuantumFactoring.OrderTrial.remainderRetention line 87
  16. lemma OAI.ExactQuantumFactoring.OrderTrial.discrepancy_at line 90
  17. lemma OAI.ExactQuantumFactoring.OrderTrial.remainderRetention_at line 96
  18. def OAI.ExactQuantumFactoring.OrderTrial.retentionBits line 103

    Source documentation

    One clock-independent number of bits works for all three modes, on every valid label, including d=1,j=0.

    def retentionBits (n : ℕ) := 80*n+20
  19. lemma OAI.ExactQuantumFactoring.OrderTrial.retentions_fixedDenominator line 104
  20. lemma OAI.ExactQuantumFactoring.OrderTrial.retained_numerator line 112