TreeReadout.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.readoutProgram line 20
Source documentation
The readout is a clean reversible Boolean network, not a classical hidden postprocessor. The preparation's complete history is retained.
```
def readoutProgram {q m r : ℕ} (P : List (Instruction q))
    (c : BooleanNetwork q m) (hr : c.net.count≤r) : List (Instruction (q+m+r)) :=
…
```
Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.BooleanNetwork
lemma OAI.ExactQuantumFactoring.readoutProgram_state line 24
lemma OAI.ExactQuantumFactoring.readoutProgram_length line 34
abbrev OAI.ExactQuantumFactoring.PhysicalTree.readoutWork line 42
abbrev OAI.ExactQuantumFactoring.PhysicalTree.readoutWidth line 43
def OAI.ExactQuantumFactoring.PhysicalTree.factoringProgram line 45
def OAI.ExactQuantumFactoring.PhysicalTree.factoringZero line 47
def OAI.ExactQuantumFactoring.PhysicalTree.factoringResult line 49
theorem OAI.ExactQuantumFactoring.PhysicalTree.factoringProgram_exact line 56
Source documentation
Probability ONE of complete factorization for the actual finite physical fixed-gate program, with its clean reversible readout. Polynomial resource bounds and finite-alphabet polynomial-time uniformity are separate properties of the same circuit family.
```
theorem factoringProgram_exact {n N : ℕ} (hn : 128≤n) (hN : 2≤N) (hb : N<2^n) :
    outcomeMass (fun x=>CorrectEncoding N n (guessWords n (factoringResult n (by omega) x)))
      ((programMatrix (factoringProgram n (by omega))).mulVec
        (basisVector (factoringZero n N (by omega))))=1 := by
…
```
Mentions: OAI.ExactQuantumFactoring.CorrectEncoding, OAI.ExactQuantumFactoring.guessWords, OAI.ExactQuantumFactoring.PhysicalTree.factoringResult, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.PhysicalTree.factoringProgram, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.PhysicalTree.factoringZero