OAI/Computability/QuantumFactoring/CompletionFilterCircuit.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactQuantumFactoring.Completion.Expressions.ordinaryMass line 21
  2. def OAI.ExactQuantumFactoring.Completion.Expressions.coefficient line 24
  3. def OAI.ExactQuantumFactoring.Completion.Expressions.guess line 28
  4. lemma OAI.ExactQuantumFactoring.Completion.Expressions.ordinaryMass_value line 32
  5. lemma OAI.ExactQuantumFactoring.Completion.Expressions.coefficient_value line 35
  6. lemma OAI.ExactQuantumFactoring.Completion.Expressions.guess_value line 39
  7. def OAI.ExactQuantumFactoring.Completion.filterNet line 50

    Source documentation

    Literal deferred completion filter on retained registers. The input s and canonical-output circuits are to be computed from the verified full log; this compiler does not smuggle those quantities into the preparation.

    def filterNet {v : Type*} {k b W t : ℕ} (d : ℕ)
    (s z : RatExpr v) (vars : v→BooleanNetwork k b)
    (branch : BooleanNetwork k t) (guess canonical : BooleanNetwork k W)
    (coin : NatExpr v) (good : BooleanNetwork k 1) : BooleanNetwork k 1 :=
…

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

  8. lemma OAI.ExactQuantumFactoring.Completion.filterNet_value line 60
  9. theorem OAI.ExactQuantumFactoring.Completion.filterNet_passed line 85

    Source documentation

    On the very same retained record, the gate flag is exactly the §6 event.

    theorem filterNet_passed {α v : Type*} {k b W t d : ℕ}
    (s z : RatExpr v) (vars : v→BooleanNetwork k b)
    (branch : BooleanNetwork k t) (guess canonical : BooleanNetwork k W)
    (coin : NatExpr v) (good : BooleanNetwork k 1) (P : α→Prop)
    (x : Basis k) (r : Raw α W t d) (y₀ : Basis W) (S Z : ℚ)
    (hbranch : branch.eval x=r.1) (hguess : guess.eval x=r.2.2.1)
    (hcanonical : canonical.eval x=y₀)
    (hcoin : coin.eval (fun i=>(bitsValue ((vars i).eval x)).toNat)=(bitsValue r.2.2.2).toNat)
    (hgood : good.eval x 0=true ↔ P r.2.1)
    (hs : s.eval (fun i=>(bitsValue ((vars i).eval x)).toNat)=S)
    (hz : z.eval (fun i=>(bitsValue ((vars i).eval x)).toNat)=Z) :
    (filterNet d s z vars branch guess canonical coin good).eval x 0=true ↔ passed P y₀ S Z r := by
…

    Mentions: OAI.ExactQuantumFactoring.RatExpr, OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.NatExpr, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.Completion.Raw, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.Completion.filterNet, OAI.ExactQuantumFactoring.Completion.passed