PhysicalAmplification.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

def OAI.ExactQuantumFactoring.Supported line 20
Source documentation
A support invariant for a read-only classical input sector.
```
def Supported {ι : Type*} (S : ι → Prop) (v : ι → ℂ) : Prop :=
…
```
def OAI.ExactQuantumFactoring.RespectsSector line 24
Source documentation
Matrix entries cannot change the read-only input.
```
def RespectsSector {ι : Type*} (S : ι → Prop) (U : Matrix ι ι ℂ) : Prop :=
…
```
lemma OAI.ExactQuantumFactoring.RespectsSector.adjoint line 27
lemma OAI.ExactQuantumFactoring.RespectsSector.supported line 33
def OAI.ExactQuantumFactoring.signState line 44
lemma OAI.ExactQuantumFactoring.signState_supported line 47
lemma OAI.ExactQuantumFactoring.signState_eq line 52
lemma OAI.ExactQuantumFactoring.sector_zero_sign line 59
lemma OAI.ExactQuantumFactoring.adjoint_coordinate line 78

lemma OAI.ExactQuantumFactoring.conjugated_zero_sign line 86

Source documentation

The physical sign on zero work, conjugated by a reversible preparation, is minus the reflection about its output, within the invariant input fiber.

lemma conjugated_zero_sign {ι : Type*} [Fintype ι] [DecidableEq ι]
    (U : Matrix ι ι ℂ) (hu : U ∈ Matrix.unitaryGroup ι ℂ)
    (S : ι → Prop) (hS : RespectsSector S U) (z : ι)
    (p : ι → Bool) (hp : ∀ x, S x → (p x=true ↔ x=z))
    (v : ι → ℂ) (hv : Supported S v) :
    U.mulVec (signState p (U.conjTranspose.mulVec v)) =
      -stateReflection (U.mulVec (basisVector z)) v := by
…

Mentions: OAI.ExactQuantumFactoring.RespectsSector, OAI.ExactQuantumFactoring.Supported, OAI.ExactQuantumFactoring.signState, OAI.ExactQuantumFactoring.basisVector

def OAI.ExactQuantumFactoring.amplificationProgram line 104
Source documentation
Five actual programs: prepare, mark good, unprepare, mark zero work, prepare. The two phase predicates share a clean flag and scratch area.
```
def amplificationProgram {n r : ℕ} (ops : List (Instruction n))
    (good zero : BooleanNetwork n 1) (hg : good.net.count ≤ r) (hz : zero.net.count ≤ r) :
    List (Instruction (n+1+r)) :=
…
```
Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.BooleanNetwork
lemma OAI.ExactQuantumFactoring.amplificationProgram_length line 111
lemma OAI.ExactQuantumFactoring.amplificationProgram_state line 121

theorem OAI.ExactQuantumFactoring.physical_quarter_amplification line 140

Source documentation

Exact amplitude amplification implemented over the fixed named gates. The semantic premises are preparation mass and the unchanged-input invariant, not a gate oracle or an assumed reflection.

theorem physical_quarter_amplification {n r : ℕ} (ops : List (Instruction n))
    (good zero : BooleanNetwork n 1) (hg : good.net.count ≤ r) (hz : zero.net.count ≤ r)
    (S : Basis n → Prop) (hS : RespectsSector S (programMatrix ops))
    (z : Basis n) (hstart : S z)
    (hzero : ∀ x, S x → (zero.eval x 0=true ↔ x=z))
    (hquarter : outcomeMass (fun x => good.eval x 0=true)
      ((programMatrix ops).mulVec (basisVector z)) = 1/4) :
    (programMatrix (amplificationProgram ops good zero hg hz)).mulVec
      (basisVector (packed r z (fun _ : Fin 1 => false))) =
      encodeState (fun x => packed r x (fun _ : Fin 1 => false))
        (fun x => -2*goodPart (fun y => good.eval y 0=true)
          ((programMatrix ops).mulVec (basisVector z)) x) := by
…

Mentions: OAI.ExactQuantumFactoring.Instruction, OAI.ExactQuantumFactoring.BooleanNetwork, OAI.ExactQuantumFactoring.Basis, OAI.ExactQuantumFactoring.RespectsSector, OAI.ExactQuantumFactoring.programMatrix, OAI.ExactQuantumFactoring.basisVector, OAI.ExactQuantumFactoring.amplificationProgram, OAI.ExactQuantumFactoring.encodeState