OAI/Computability/QuantumFactoring/NaturalExpressions.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

A finite straight-line expression language for the exact rational formulas in the manuscript. All values are natural numbers, not unit-cost hidden gates. The following compiler will realize these operations with actual bit networks.

  1. inductive OAI.ExactQuantumFactoring.NatExpr line 14
  2. def OAI.ExactQuantumFactoring.NatExpr.eval line 28
  3. def OAI.ExactQuantumFactoring.NatExpr.size line 38
  4. def OAI.ExactQuantumFactoring.NatExpr.constOK line 43
  5. lemma OAI.ExactQuantumFactoring.NatExpr.size_pos line 49
  6. lemma OAI.ExactQuantumFactoring.NatExpr.value_bound line 51
  7. def OAI.ExactQuantumFactoring.NatExpr.Fits line 92

    Source documentation

    Every intermediate value fits, not merely the eventual answer.

    def Fits (B : ℕ) (x : v → ℕ) (e : NatExpr v) : Prop :=
…

    Mentions: OAI.ExactQuantumFactoring.NatExpr

  8. lemma OAI.ExactQuantumFactoring.NatExpr.Fits.mono line 98
  9. lemma OAI.ExactQuantumFactoring.NatExpr.fits_bound line 107
  10. lemma OAI.ExactQuantumFactoring.NatExpr.fits_bits line 122