OAI/Computability/QuantumFactoring/TreeAmplified.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.PhysicalTree.actual_quarter_mass line 20
2. def OAI.ExactQuantumFactoring.PhysicalTree.reflectWork line 31
3. abbrev OAI.ExactQuantumFactoring.PhysicalTree.amplifiedWidth line 33
4. def OAI.ExactQuantumFactoring.PhysicalTree.amplifiedProgram line 35
5. def OAI.ExactQuantumFactoring.PhysicalTree.amplifiedZero line 38
6. def OAI.ExactQuantumFactoring.PhysicalTree.amplifiedOutput line 40
7. theorem OAI.ExactQuantumFactoring.PhysicalTree.amplifiedProgram_state line 45

   Source documentation

   An unconditional physical amplification identity for the actual program. The only hypotheses are the manuscript's padded length and valid input.

   theorem amplifiedProgram_state {n N : ℕ} (hn : 128≤n) (hN : 2≤N) (hb : N<2^n) :
       (programMatrix (amplifiedProgram n (by omega))).mulVec
         (basisVector (amplifiedZero n N (by omega))) =
         encodeState (fun x=>packed (reflectWork n (by omega)) x (fun _ : Fin 1=>false))
           (fun x=> -2*goodPart (fun y=>(quarterFlag n (by omega)).eval y 0=true)
             ((programMatrix (quarterProgram n)).mulVec (basisVector (quarterZero n N))) x) := by
   …

   Mentions: OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.PhysicalTree.amplifiedProgram, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.PhysicalTree.amplifiedZero, OAI.ExactQuantumFactoring.encodeState, OAI.ExactQuantumFactoring.PhysicalTree.reflectWork, OAI.ExactQuantumFactoring.PhysicalTree.quarterFlag, OAI.ExactQuantumFactoring.PhysicalTree.quarterProgram, OAI.ExactQuantumFactoring.PhysicalTree.quarterZero

8. lemma OAI.ExactQuantumFactoring.PhysicalTree.prepared_nonzero_encoding line 58
9. lemma OAI.ExactQuantumFactoring.PhysicalTree.quarterFlag_output_on_support line 66
10. theorem OAI.ExactQuantumFactoring.PhysicalTree.amplified_output_on_support line 78

    Source documentation

    Exact support on complete sorted factorizations, for the actual finite fixed-gate program and a literal Boolean readout. This is a necessary main proof dependency, not the missing polynomial/uniform circuit-family theorem.

    theorem amplified_output_on_support {n N : ℕ} (hn : 128≤n) (hN : 2≤N) (hb : N<2^n)
        (x : Basis (amplifiedWidth n (by omega)))
        (hx : ((programMatrix (amplifiedProgram n (by omega))).mulVec
          (basisVector (amplifiedZero n N (by omega)))) x≠0) :
        CorrectEncoding N n (guessWords n ((amplifiedOutput n (by omega)).eval x)) := by
    …

    Mentions: OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.PhysicalTree.amplifiedWidth, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.PhysicalTree.amplifiedProgram, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.PhysicalTree.amplifiedZero, OAI.ExactQuantumFactoring.CorrectEncoding, OAI.ExactQuantumFactoring.guessWords, OAI.ExactQuantumFactoring.PhysicalTree.amplifiedOutput

11. lemma OAI.ExactQuantumFactoring.PhysicalTree.amplified_mass_one line 105