OAI/Computability/QuantumFactoring/CompletionPredicateCircuit.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.Completion.predicateFilter line 21

   Source documentation

   A deferred guess predicate, rather than a circuit that constructs the canonical CRT string. Both branches use the same retained completion coin.

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

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

2. lemma OAI.ExactQuantumFactoring.Completion.predicateFilter_value line 31
3. theorem OAI.ExactQuantumFactoring.Completion.predicateFilter_test line 50

   Source documentation

   Exact same-history predicate semantics: this theorem does not supply or assume an algorithm for either of the two input Boolean tests.

   theorem predicateFilter_test {α v : Type*} {k b W t d : ℕ}
       (s z : RatExpr v) (vars : v→BooleanNetwork k b)
       (branch : BooleanNetwork k t) (coin : NatExpr v)
       (good guessGood : BooleanNetwork k 1) (x : Basis k)
       (P : α→Prop) (Q : Basis W→Prop) (r : Raw α W t d) (S Z : ℚ)
       (hbranch : branch.eval x=r.1)
       (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)
       (hguess : guessGood.eval x 0=true ↔ Q r.2.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) :
       (predicateFilter (W:=W) d s z vars branch coin good guessGood).eval x 0=true ↔
   …

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