OAI/Computability/QuantumFactoring/CircuitEmissionEncoding.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.natWordP line 16
2. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.gateViewP line 19
3. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.gatePrimitiveP line 21
4. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.gateInverseP line 23
5. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.gateControlledP line 25
6. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.gateHeaderP line 27
7. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.opViewP line 33
8. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.opGateP line 35
9. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.opWiresP line 37
10. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.wireWordsP line 39
11. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.opEncodeClippedP line 43
12. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.dataViewP line 50
13. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.qubitsP line 52
14. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.opsP line 54
15. def OAI.ExactQuantumFactoring.CircuitEmission.Emission.encodeClippedP line 56
16. theorem OAI.ExactQuantumFactoring.CircuitEmission.uniform_of_emitter line 68

    Source documentation

    This reduction charges all unary description writing, including every wire. It is useful only with an actual finite-stack emitter for the literal erased family.

    theorem uniform_of_emitter (family : ℕ→Circuit)
        (p : Procedure unaryCode dataCode (fun n=>erase (family n))) : Uniform family := by
    …

    Mentions: OAI.ExactQuantumFactoring.Circuit, OAI.ExactQuantumFactoring.CircuitEmission.dataCode, OAI.ExactQuantumFactoring.CircuitEmission.erase, OAI.ExactQuantumFactoring.Uniform