OAI/Computability/QuantumFactoring/PolynomialTemplateEmission.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits line 15

    Source documentation

    A fixed polynomial syntax skeleton transports literal coefficient emitters through substitution. The outer polynomial's depth is fixed; input coefficients are generated by the supplied charged Boolean-stack procedures.

    def PolyEmits (ea : α→List Bool) (ev : v→List Bool) (f : α→PolyExpr v) : Prop:=
…

    Mentions: OAI.ExactQuantumFactoring.PolyExpr

  2. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.C line 19
  3. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.X line 25
  4. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.add line 26
  5. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.neg line 29
  6. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.sub line 32
  7. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.mul line 34
  8. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.constant line 37
  9. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.pow line 38
  10. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.literal line 43
  11. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.comp_comp line 50
  12. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.comp line 57
  13. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.comp_X line 61
  14. lemma OAI.ExactQuantumFactoring.NetworkEmission.PolyEmits.coeff line 68