OAI/Computability/QuantumFactoring/ContinuedFractionCircuit.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ExactQuantumFactoring.BitArithmetic.cfWidth line 16
2. def OAI.ExactQuantumFactoring.BitArithmetic.cfHead line 18
3. def OAI.ExactQuantumFactoring.BitArithmetic.cfTail line 19
4. def OAI.ExactQuantumFactoring.BitArithmetic.cfP line 20
5. def OAI.ExactQuantumFactoring.BitArithmetic.cfQ line 21
6. def OAI.ExactQuantumFactoring.BitArithmetic.cfProduct line 22
7. def OAI.ExactQuantumFactoring.BitArithmetic.cfCombine line 24
8. def OAI.ExactQuantumFactoring.BitArithmetic.convergentNet line 29
9. lemma OAI.ExactQuantumFactoring.BitArithmetic.cfHead_eval line 35
10. lemma OAI.ExactQuantumFactoring.BitArithmetic.cfTail_eval line 39
11. lemma OAI.ExactQuantumFactoring.BitArithmetic.cfP_eval line 43
12. lemma OAI.ExactQuantumFactoring.BitArithmetic.cfQ_eval line 46
13. lemma OAI.ExactQuantumFactoring.BitArithmetic.cfProduct_value line 50
14. lemma OAI.ExactQuantumFactoring.BitArithmetic.cfCombine_value line 56
15. lemma OAI.ExactQuantumFactoring.BitArithmetic.convergentNet_value line 79

    Source documentation

    One recursive circuit is used once per Euclidean level; no exponential syntax duplication of earlier convergents.

    lemma convergentNet_value {s w : ℕ} (k : ℕ) (hw : cfWidth s k ≤ w)
        (a b : Basis w) (ha : (bitsValue a).toNat<2^s) (hb : (bitsValue b).toNat<2^s) :
        ∃ p q : Basis w,
          (convergentNet w k).eval (Fin.append a b)=Fin.append p q ∧
          ((bitsValue p).toNat,(bitsValue q).toNat)=convergentPair (bitsValue a).toNat (bitsValue b).toNat k := by
    …

    Mentions: OAI.ExactQuantumFactoring.BitArithmetic.cfWidth, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.BitArithmetic.convergentNet

16. lemma OAI.ExactQuantumFactoring.BitArithmetic.cfProduct_count line 125
17. lemma OAI.ExactQuantumFactoring.BitArithmetic.cfCombine_count line 132
18. lemma OAI.ExactQuantumFactoring.BitArithmetic.convergentNet_count line 140