OAI/Computability/QuantumFactoring/RationalPowerCircuit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.NatExpr.pow_size line 18
2. lemma OAI.ExactQuantumFactoring.NatExpr.pow_sharedCost line 22
3. lemma OAI.ExactQuantumFactoring.NatExpr.pow_maxConst line 27
4. def OAI.ExactQuantumFactoring.IntExpr.signedPower line 39

   Source documentation

   Power of a balanced signed integer without the exponentially expanding positive/negative multiplication tree. The sign test is static in parity and uses only absolute value and linear-length natural-power expressions.

   def signedPower (a : IntExpr v) (k : ℕ) : IntExpr v :=
   …

   Mentions: OAI.ExactQuantumFactoring.IntExpr

5. lemma OAI.ExactQuantumFactoring.IntExpr.eval_signedPower line 43
6. lemma OAI.ExactQuantumFactoring.IntExpr.signedPower_size line 61
7. lemma OAI.ExactQuantumFactoring.IntExpr.signedPower_sharedCost line 69
8. lemma OAI.ExactQuantumFactoring.IntExpr.signedPower_maxConst line 77
9. def OAI.ExactQuantumFactoring.RatExpr.signedPower line 98

   Source documentation

   Exact rational power, with polynomial syntax in k, including zero unreduced denominators. Existing pow and its semantics are not changed.

   def signedPower (a : RatExpr v) (k : ℕ) : RatExpr v :=
   …

   Mentions: OAI.ExactQuantumFactoring.RatExpr

10. lemma OAI.ExactQuantumFactoring.RatExpr.eval_signedPower line 101
11. def OAI.ExactQuantumFactoring.RatExpr.repeatedSuccess line 108

    Source documentation

    The repeated-success expression used by both real transitions, without an exponentially expanded balanced-integer numerator syntax.

    def repeatedSuccess (a : RatExpr v) (K : ℕ) : RatExpr v :=
    …

    Mentions: OAI.ExactQuantumFactoring.RatExpr

12. lemma OAI.ExactQuantumFactoring.RatExpr.repeatedSuccess_value line 110