OAI/Computability/QuantumFactoring/RetentionCircuit.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.NatExpr.isOne_shared_count line 21
2. def OAI.ExactQuantumFactoring.retentionNet line 34

   Source documentation

   Compile the dyadic threshold to a finite Boolean network. All arithmetic, including signed rational division and floor, is reduced to bounded word gates.

   def retentionNet {v : Type*} {k b : ℕ} (T : ℕ) (p : RatExpr v) (coin : NatExpr v)
       (vars : v → BooleanNetwork k b) : BooleanNetwork k 1 :=
   …

   Mentions: OAI.ExactQuantumFactoring.RatExpr, OAI.ExactQuantumFactoring.NatExpr, OAI.ExactQuantumFactoring.BooleanNetwork

3. lemma OAI.ExactQuantumFactoring.retentionNet_value line 37
4. lemma OAI.ExactQuantumFactoring.retentionNet_count line 43
5. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.firstE line 55
6. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.secondE line 57
7. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.lastE line 59
8. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.firstE_value line 62
9. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.secondE_value line 66
10. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.lastE_value line 73
11. def OAI.ExactQuantumFactoring.OrderTrial.Expressions.modeRetentionNet line 81

    Source documentation

    The three actual source retentions. Each net is total also at malformed labels; the separately compiled label guard suppresses those outputs.

    def modeRetentionNet {k b : ℕ} (n : ℕ) (mode : Fin 3) (d j t coin : NatExpr v)
        (vars : v → BooleanNetwork k b) : BooleanNetwork k 1 :=
    …

    Mentions: OAI.ExactQuantumFactoring.NatExpr, OAI.ExactQuantumFactoring.BooleanNetwork

12. lemma OAI.ExactQuantumFactoring.OrderTrial.Expressions.modeRetentionNet_value line 86