OAI/Computability/QuantumFactoring/FairOracle.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Actual fair-bit initialization followed by clean reversible Boolean computation. All random bits remain in the returned physical state.

  1. lemma OAI.ExactQuantumFactoring.outcomeMass_encode line 17
  2. def OAI.ExactQuantumFactoring.fairOracle line 36
  3. lemma OAI.ExactQuantumFactoring.fairOracle_length line 40
  4. lemma OAI.ExactQuantumFactoring.fairOracle_state line 47
  5. lemma OAI.ExactQuantumFactoring.fairOracle_embedding line 60
  6. lemma OAI.ExactQuantumFactoring.fairOracle_mass line 66
  7. def OAI.ExactQuantumFactoring.packedOutputBit line 76

    Source documentation

    A designated target bit of the packed clean oracle output.

    def packedOutputBit {n m r : ℕ} (i : Fin m) (x : Basis (n+m+r)) : Bool :=
…

    Mentions: OAI.ExactQuantumFactoring.Basis

  8. lemma OAI.ExactQuantumFactoring.packedOutputBit_eval line 79
  9. lemma OAI.ExactQuantumFactoring.verified_guess_physical_mass line 85

    Source documentation

    The small, everywhere positive branch of Section 6, now with a physical program and the concrete AKS verifier, not an abstract random-guess oracle.

    lemma verified_guess_physical_mass {n r : ℕ} (hn : 128 ≤ n)
    (hr : (guessVerifier n).net.count ≤ r) (a : Basis n)
    (hN : 2 ≤ (bitsValue a).toNat) :
    outcomeMass (fun x => packedOutputBit (n:=n+n*n) (m:=1) (r:=r) 0 x=true)
…

    Mentions: OAI.ExactQuantumFactoring.guessVerifier, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.bitsValue, OAI.ExactQuantumFactoring.packedOutputBit