OAI/Computability/QuantumFactoring/RetainedRateExpression.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.Completion.Expressions.orderRate line 23

   Source documentation

   The exact completed-order success expression. Its only runtime inputs are the actual unit order and its totient, both computed from retained rows.

   def orderRate (n K : ℕ) : RatExpr (Fin 2) :=
   …

   Mentions: OAI.ExactQuantumFactoring.RatExpr

2. lemma OAI.ExactQuantumFactoring.Completion.Expressions.orderRate_value line 26
3. def OAI.ExactQuantumFactoring.NodeMachine.orderRateVars line 37
4. lemma OAI.ExactQuantumFactoring.NodeMachine.orderRateVars_exact line 41
5. lemma OAI.ExactQuantumFactoring.NodeMachine.retainedOrderRate_exact line 56