Basic.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

def OAI.QAC.rankOne line 11
Source documentation
The orthogonal projection onto a normalized one-qubit vector.
```
def rankOne (v : Bit → ℂ) : QubitOperator := fun x y => v x * star (v y)
```
Mentions: OAI.QAC.Bit, OAI.QAC.QubitOperator
structure OAI.QAC.Count line 15
Source documentation
The same data describe a product projection and its mismatch count. Normalization is exactly the sum of the squared moduli being one.
```
structure Count (N : ℕ) where
…
```
def OAI.QAC.Count.zero line 22
def OAI.QAC.Count.pattern line 27
Source documentation
The orthogonal projection specifying precisely the mismatch set F. It is used only for F contained in the counted support.
```
def pattern {N : ℕ} (M : Count N) (F : Finset (Fin N)) : Operator N :=
…
```
Mentions: OAI.QAC.Count, OAI.QAC.Operator
def OAI.QAC.Count.high line 32
Source documentation
The spectral projection [M ≥ r], explicitly expanded in its product eigenbasis.
```
def high {N : ℕ} (M : Count N) (r : ℝ) : Operator N :=
…
```
Mentions: OAI.QAC.Count, OAI.QAC.Operator
def OAI.QAC.Count.operator line 36
Source documentation
The mismatch operator ∑ᵢ (I - |vᵢ⟩⟨vᵢ|)ᵢ.
```
def operator {N : ℕ} (M : Count N) : Operator N :=
…
```
Mentions: OAI.QAC.Count, OAI.QAC.Operator
abbrev OAI.QAC.LocalLayer line 41
def OAI.QAC.localMatrix line 43
structure OAI.QAC.ReflectionLayer line 47
Source documentation
A parallel layer of product-projection reflections, with disjoint supports.
```
structure ReflectionLayer (N : ℕ) where
…
```
def OAI.QAC.reflectionMatrix line 51

def OAI.QAC.IsCircuit line 56

Source documentation

The enlarged normal form of depth at most d. Identity local and reflection layers are allowed.

def IsCircuit {N : ℕ} : ℕ → Operator N → Prop
  | 0, U => ∃ L : LocalLayer N, U = localMatrix L
  | d + 1, U => ∃ (V : Operator N) (R : ReflectionLayer N) (L : LocalLayer N),
      IsCircuit d V ∧ U = V * reflectionMatrix R * localMatrix L

/-- Full uniform localization theorem, including s = 0 and arbitrary t > s. -/

Mentions: OAI.QAC.Operator, OAI.QAC.LocalLayer, OAI.QAC.localMatrix, OAI.QAC.ReflectionLayer, OAI.QAC.reflectionMatrix, OAI.QAC.localization

def OAI.QAC.LocalizationStatement line 62
Source documentation
Full uniform localization theorem, including s = 0 and arbitrary t > s.
```
def LocalizationStatement : Prop :=
…
```