OAI/Computability/QuantumFactoring/CircuitFinalEmission.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.unaryMax line 14
2. lemma OAI.ExactQuantumFactoring.BitStackProgram.Emits.range line 18
3. lemma OAI.ExactQuantumFactoring.CircuitEmission.OpsEmits.place line 26
4. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.relocateValP line 40
5. theorem OAI.ExactQuantumFactoring.UniformResources.PhysicalTree.uniform_of_quarter_emitters line 68

   Source documentation

   A precise remaining syntax boundary. All post-quarter amplification, clean oracle synthesis, readout, relocation, and unary serialization are actual charged finite-stack procedures; none is a generation-time oracle.

   theorem uniform_of_quarter_emitters
       (hw : Emits unaryCode unaryCode (fun l=>quarterWidth (paddedLength l)))
       (hp : OpsEmits unaryCode (fun l=>quarterProgram (paddedLength l)))
       (hf : NetEmits unaryCode (fun l=>quarterFlag (paddedLength l) (paddedLength_pos l)))
       (hz : NetEmits unaryCode (fun l=>zeroNet (paddedLength l)))
       (ho : NetEmits unaryCode (fun l=>quarterOutputNet (paddedLength l))) :
       Uniform finalCircuit:=by
   …

   Mentions: OAI.ExactQuantumFactoring.paddedLength, OAI.ExactQuantumFactoring.Uniform