OAI/Computability/QuantumFactoring/PhysicalNodeOutput.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.PhysicalNode.resultField line 20
2. def OAI.ExactQuantumFactoring.PhysicalNode.sortedOutput line 24
3. def OAI.ExactQuantumFactoring.PhysicalNode.shrink line 27
4. lemma OAI.ExactQuantumFactoring.PhysicalNode.resultField_pack line 29
5. lemma OAI.ExactQuantumFactoring.PhysicalNode.shrink_zero line 34
6. lemma OAI.ExactQuantumFactoring.PhysicalNode.sortedOutput_pack line 40
7. lemma OAI.ExactQuantumFactoring.PhysicalNode.shrink_values line 49
8. theorem OAI.ExactQuantumFactoring.PhysicalNode.complete_output line 59

   Source documentation

   The actual retained node configuration admits an explicit polynomial Boolean sorting/readout network. Its output is the LITERAL main-theorem encoding, with exactly n fields, zero padding and multiplicities.

   theorem complete_output {n N : ℕ} (hn : 128 ≤ n) (hN : 2 ≤ N) (hb : N<2^n)
       (h : SplitMachine.Trace n (2*n))
       (hp : (machine n (2*n)).passed (NodeStateCircuit.pack [natBasis (n+1) N] [] false) (2*n) h) :
       ∃ zs : List (Basis n), zs.length=n ∧ CorrectEncoding N n (SortedWords.numbers zs) ∧
         (sortedOutput n).eval
           ((machine n (2*n)).config (NodeStateCircuit.pack [natBasis (n+1) N] [] false) (2*n) h)=
             SortedWords.layout n n zs := by
   …

   Mentions: OAI.ExactQuantumFactoring.SplitMachine.Trace, OAI.ExactQuantumFactoring.PhysicalNode.machine, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.CorrectEncoding, OAI.ExactQuantumFactoring.PhysicalNode.sortedOutput