OAI/Computability/QuantumFactoring/RetentionExpressions.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.coveringPow line 16

    Source documentation

    Bounded priority search for the least covering power of two. The bounds are compile-time constants, not exponentiation gates with variable exponents.

    def coveringPow (d : NatExpr v) : ℕ → NatExpr v
  | 0 => .const 1
  | k+1 => .iteLe d (.const (2^k)) (coveringPow d k) (.const (2^(k+1)))

    Mentions: OAI.ExactQuantumFactoring.NatExpr

  2. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.coveringPow_correct line 19
  3. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.lambdaE line 35
  4. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.lambdaE_correct line 37
  5. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.coefficientE line 42
  6. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.coefficientE_correct line 45
  7. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.remainderE line 50
  8. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.remainderE_correct line 52
  9. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.discrepancyE line 58
  10. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.discrepancyE_correct line 60
  11. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.thirdRetentionE line 69
  12. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.thirdRetentionE_correct line 71