This definition gives the library's named construction or computation for “last basis equiv”. Adjoin a most-significant bit; existing wire numbers do not change.
def lastBasisEquiv (n : Nat) : PrimitiveBasis (n + 1) ≃ PrimitiveBasis n × Fin 2 :=
(Fin.snocEquiv (fun _ : Fin (n + 1) => Fin 2)).symm.trans (Equiv.prodComm _ _)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “last basis equiv apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem lastBasisEquiv_apply {n : Nat} (b : PrimitiveBasis (n + 1)) :
lastBasisEquiv n b = (Fin.init b, b (Fin.last n)) := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “last basis equiv symm apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem lastBasisEquiv_symm_apply {n : Nat} (b : PrimitiveBasis n) (v : Fin 2) :
(lastBasisEquiv n).symm (b, v) = Fin.snoc b v := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “basis eq iff”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem basis_eq_iff {n : Nat} (a b : PrimitiveBasis (n + 1)) :
a = b ↔ Fin.init a = Fin.init b ∧ a (Fin.last n) = b (Fin.last n) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “lift last matrix”. Tensor a circuit matrix with an untouched highest wire.
noncomputable def liftLastMatrix {n : Nat}
(M : _root_.Matrix (PrimitiveBasis n) (PrimitiveBasis n) ℂ) :
_root_.Matrix (PrimitiveBasis (n + 1)) (PrimitiveBasis (n + 1)) ℂ :=
_root_.Matrix.reindexAlgEquiv ℂ ℂ (lastBasisEquiv n).symm
(M ⊗ₖ (1 : _root_.Matrix (Fin 2) (Fin 2) ℂ))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lift last matrix apply”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem liftLastMatrix_apply {n : Nat}
(M : _root_.Matrix (PrimitiveBasis n) (PrimitiveBasis n) ℂ)
(a b : PrimitiveBasis (n + 1)) :
liftLastMatrix M a b =
if a (Fin.last n) = b (Fin.last n) then M (Fin.init a) (Fin.init b) else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lift last matrix one”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem liftLastMatrix_one (n : Nat) :
liftLastMatrix (1 : _root_.Matrix (PrimitiveBasis n) (PrimitiveBasis n) ℂ) = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lift last matrix mul”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem liftLastMatrix_mul {n : Nat}
(M N : _root_.Matrix (PrimitiveBasis n) (PrimitiveBasis n) ℂ) :
liftLastMatrix (M * N) = liftLastMatrix M * liftLastMatrix N := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “lift gate”. Embed every instruction without changing its original wire number.
def liftGate {n : Nat} : PrimitiveGate n → PrimitiveGate (n + 1)
| .x t => .x t.castSucc
| .ry t a => .ry t.castSucc a
| .rz t a => .rz t.castSucc a
| .cx c t h => .cx c.castSucc t.castSucc (fun e => h (Fin.castSucc_injective _ e))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lift one qubit”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem lift_oneQubit {n : Nat} (t : Fin n)
(M : _root_.Matrix (Fin 2) (Fin 2) ℂ) :
liftPrimitiveOneQubit t.castSucc M = liftLastMatrix (liftPrimitiveOneQubit t M) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval lift gate”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem eval_liftGate {n : Nat} (g : PrimitiveGate n) :
evalPrimitiveGate (liftGate g) = liftLastMatrix (evalPrimitiveGate g) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “eval lift circuit”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem eval_liftCircuit {n : Nat} (c : PrimitiveCircuit n) :
evalPrimitiveCircuit (c.map liftGate) = liftLastMatrix (evalPrimitiveCircuit c) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “pair norm”. Euclidean mass at one binary split.
noncomputable def pairNorm (a b : ℝ) : ℝ := Real.sqrt (a ^ 2 + b ^ 2)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “pair norm nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem pairNorm_nonneg (a b : ℝ) : 0 ≤ pairNorm a b := Real.sqrt_nonneg _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “pair norm sq”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem pairNorm_sq (a b : ℝ) : pairNorm a b ^ 2 = a ^ 2 + b ^ 2 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “split angle”. Twice the signed polar angle, with the zero subtree assigned angle zero.
noncomputable def splitAngle (a b : ℝ) : ExactAngle :=
if pairNorm a b = 0 then .rational 0 else
.real (2 * if b < 0 then -Real.arccos (a / pairNorm a b)
else Real.arccos (a / pairNorm a b))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “split angle first column”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem splitAngle_firstColumn (a b : ℝ) (v : Fin 2) :
standardRyMatrix (splitAngle a b).eval v 0 * (pairNorm a b : ℂ) =
if v = 0 then (a : ℂ) else (b : ℂ) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “marginal”. Marginal amplitudes on all but the highest wire.
noncomputable def marginal {n : Nat} (f : PrimitiveBasis (n + 1) → ℝ) :
PrimitiveBasis n → ℝ := fun b => pairNorm (f (Fin.snoc b 0)) (f (Fin.snoc b 1))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “marginal nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem marginal_nonneg {n : Nat} (f : PrimitiveBasis (n + 1) → ℝ) (b : PrimitiveBasis n) :
0 ≤ marginal f b := pairNorm_nonneg _ _
/-- True squared Euclidean norm of the complete amplitude table. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “norm sq”. True squared Euclidean norm of the complete amplitude table.
noncomputable def normSq {n : Nat} (f : PrimitiveBasis n → ℝ) : ℝ := ∑ b, f b ^ 2
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm sq nonneg”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem normSq_nonneg {n : Nat} (f : PrimitiveBasis n → ℝ) : 0 ≤ normSq f :=
Finset.sum_nonneg (fun _ _ => sq_nonneg _)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm sq marginal”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem normSq_marginal {n : Nat} (f : PrimitiveBasis (n + 1) → ℝ) :
normSq (marginal f) = normSq f := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “prepare circuit”. Chronological low-bit-first binary tree, compiled entirely to RY and CX.
noncomputable def prepareCircuit : (n : Nat) → (PrimitiveBasis n → ℝ) → PrimitiveCircuit n
| 0, _ => []
| n + 1, f =>
(prepareCircuit n (marginal f)).map liftGate ++
compileUniformlyControlledRy n Fin.castSucc (Fin.last n) Fin.castSucc_ne_last
(fun b => splitAngle (f (Fin.snoc b 0)) (f (Fin.snoc b 1)))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare circuit unitary”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem prepareCircuit_unitary {n : Nat} (f : PrimitiveBasis n → ℝ) :
evalPrimitiveCircuit (prepareCircuit n f) ∈
_root_.Matrix.unitaryGroup (PrimitiveBasis n) ℂ :=
evalPrimitiveCircuit_unitary _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “controlled last apply”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem controlledLast_apply {n : Nat} (angles : PrimitiveBasis n → ExactAngle)
(a b : PrimitiveBasis (n + 1)) :
controlledRyBlockMatrix Fin.castSucc (Fin.last n) Fin.castSucc_ne_last angles a b =
if Fin.init a = Fin.init b then
standardRyMatrix (angles (Fin.init a)).eval (a (Fin.last n)) (b (Fin.last n))
else 0 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “controlled last mul lift”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem controlledLast_mul_lift {n : Nat} (angles : PrimitiveBasis n → ExactAngle)
(M : _root_.Matrix (PrimitiveBasis n) (PrimitiveBasis n) ℂ)
(a : PrimitiveBasis (n + 1)) :
(controlledRyBlockMatrix Fin.castSucc (Fin.last n) Fin.castSucc_ne_last angles *
liftLastMatrix M) a (fun _ => 0) =
standardRyMatrix (angles (Fin.init a)).eval (a (Fin.last n)) 0 *
M (Fin.init a) (fun _ => 0) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare circuit first column”; the hypotheses and conclusion in the code panel fix its exact scope. The compiled first column is the normalized input table.
theorem prepareCircuit_firstColumn {n : Nat} (f : PrimitiveBasis n → ℝ)
(nonneg : ∀ b, 0 ≤ f b) (positive : 0 < normSq f) (b : PrimitiveBasis n) :
evalPrimitiveCircuit (prepareCircuit n f) b (fun _ => 0) =
((f b / Real.sqrt (normSq f) : ℝ) : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “normalized sum sq”; the hypotheses and conclusion in the code panel fix its exact scope. Normalization is the actual sum of squared amplitudes, not a certificate flag.
theorem normalized_sum_sq {n : Nat} (f : PrimitiveBasis n → ℝ)
(positive : 0 < normSq f) :
(∑ b, (f b / Real.sqrt (normSq f)) ^ 2) = 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm sq pos of positive”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem normSq_pos_of_positive {n : Nat} (f : PrimitiveBasis n → ℝ)
(positive : ∀ b, 0 < f b) : 0 < normSq f := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lift circuit ry count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem liftCircuit_ryCount {n : Nat} (c : PrimitiveCircuit n) :
PrimitiveCircuit.ryCount (c.map liftGate) = c.ryCount := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “lift circuit cx count”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem liftCircuit_cxCount {n : Nat} (c : PrimitiveCircuit n) :
PrimitiveCircuit.cxCount (c.map liftGate) = c.cxCount := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare circuit ry count”; the hypotheses and conclusion in the code panel fix its exact scope. The unoptimized reference tree uses exactly one RY per internal tree node.
theorem prepareCircuit_ryCount {n : Nat} (f : PrimitiveBasis n → ℝ) :
(prepareCircuit n f).ryCount = 2 ^ n - 1 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare circuit cx count”; the hypotheses and conclusion in the code panel fix its exact scope. CX count for the recursive reference multiplexor, without Gray-code optimization.
theorem prepareCircuit_cxCount {n : Nat} (f : PrimitiveBasis n → ℝ) :
(prepareCircuit n f).cxCount = 2 * (2 ^ n - 1 - n) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare circuit oracle calls”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem prepareCircuit_oracleCalls {n : Nat} (f : PrimitiveBasis n → ℝ) :
(prepareCircuit n f).resource.oracleCalls = 0 :=
PrimitiveCircuit.resource_oracleCalls_eq_zero _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “primitive basis le zero”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem primitiveBasisLE_zero (n : Nat) :
primitiveBasisLEEquiv n (fun _ => 0) = zeroBasisIndex n := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “primitive basis le zero symm”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem primitiveBasisLE_zero_symm (n : Nat) :
(primitiveBasisLEEquiv n).symm (zeroBasisIndex n) = (fun _ => 0) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “prepare matrix le”. The same circuit matrix on flat little-endian integer indices.
noncomputable def prepareMatrixLE {n : Nat} (f : Fin (gridSize n) → ℝ) :
_root_.Matrix (Fin (gridSize n)) (Fin (gridSize n)) ℂ :=
_root_.Matrix.reindexAlgEquiv ℂ ℂ (primitiveBasisLEEquiv n)
(evalPrimitiveCircuit (prepareCircuit n (fun b => f (primitiveBasisLEEquiv n b))))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare matrix le unitary”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem prepareMatrixLE_unitary {n : Nat} (f : Fin (gridSize n) → ℝ) :
prepareMatrixLE f ∈ _root_.Matrix.unitaryGroup (Fin (gridSize n)) ℂ :=
reindex_unitary _ _ (prepareCircuit_unitary _)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “norm sq reindex”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem normSq_reindex {n : Nat} (f : Fin (gridSize n) → ℝ) :
normSq (fun b => f (primitiveBasisLEEquiv n b)) = ∑ j, f j ^ 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “prepare matrix le first column”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem prepareMatrixLE_firstColumn {n : Nat} (f : Fin (gridSize n) → ℝ)
(positive : ∀ j, 0 < f j) (j : Fin (gridSize n)) :
prepareMatrixLE f j (zeroBasisIndex n) =
((f j / Real.sqrt (∑ i, f i ^ 2) : ℝ) : ℂ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “normalized sum sq le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem normalized_sum_sq_LE {n : Nat} (f : Fin (gridSize n) → ℝ)
(positive : ∀ j, 0 < f j) :
(∑ j, (f j / Real.sqrt (∑ i, f i ^ 2)) ^ 2) = 1 := by
commit-pinned source · Verso Blueprint panel