QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean

This abbreviation gives a shorter name to the type or expression used for “bell amplitude”.

noncomputable abbrev bellAmplitude : ℂ :=
  TextbookStatePreparation.invSqrtTwo

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “bell state”.

noncomputable def bellState : StateVector (gridSize 2) ℂ := fun index =>
  if index.val = 0 ∨ index.val = 3 then bellAmplitude else 0

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “bell target”.

noncomputable def bellTarget : StatePreparationTarget ℂ 2 where
  amplitudes := bellState
  normalization := ∑ index, Complex.normSq (bellState index) = 1
  source := "Bell-state textbook benchmark"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “bell target normalized”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem bellTarget_normalized : bellTarget.normalization := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “bell matrix”.

noncomputable def bellMatrix : FiniteMatrix (gridSize 2) (gridSize 2) ℂ :=
  fun row column =>
    match row.val, column.val with
    | 0, 0 => bellAmplitude
    | 0, 3 => bellAmplitude
    | 1, 1 => bellAmplitude
    | 1, 2 => bellAmplitude
    | 2, 1 => bellAmplitude
    | 2, 2 => -bellAmplitude
    | 3, 0 => bellAmplitude
    | 3, 3 => -bellAmplitude

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “star bell matrix”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem star_bellMatrix : star bellMatrix = bellMatrix := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “bell matrix unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem bellMatrix_unitary :
    bellMatrix ∈ _root_.Matrix.unitaryGroup (Fin (gridSize 2)) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “bell gate”.

noncomputable def bellGate : ComplexUnitaryGate 2 where
  matrix := bellMatrix
  unitary := bellMatrix_unitary

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “bell matrix prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem bellMatrix_prepares_target :
    applyVec bellMatrix (zeroKet 2) = bellTarget.amplitudes := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “bell certificate”.

noncomputable def bellCertificate : ComplexStatePreparationCertificate 2 where
  target := bellTarget
  gate := bellGate
  normalizationProof := bellTarget_normalized
  preparationProof := bellMatrix_prepares_target

/-! ## Dense Möttönen-style benchmark -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “mottonen dense state”.

noncomputable def mottonenDenseState : StateVector (gridSize 2) ℂ := fun index =>
  match index.val with
  | 0 => (39 : ℂ) / 169
  | 1 => (52 : ℂ) / 169
  | 2 => (60 : ℂ) / 169
  | _ => (144 : ℂ) / 169

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “mottonen dense target”.

noncomputable def mottonenDenseTarget : StatePreparationTarget ℂ 2 where
  amplitudes := mottonenDenseState
  normalization := ∑ index, Complex.normSq (mottonenDenseState index) = 1
  source := "Möttönen-style dense two-qubit nested-Pythagorean benchmark"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mottonen dense target normalized”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem mottonenDenseTarget_normalized : mottonenDenseTarget.normalization := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “mottonen dense matrix”. Rational quaternion completion with first column '(39,52,60,144)/169'.

noncomputable def mottonenDenseMatrix :
    FiniteMatrix (gridSize 2) (gridSize 2) ℂ := fun row column =>
  match row.val, column.val with
  | 0, 0 => (39 : ℂ) / 169
  | 0, 1 => -(52 : ℂ) / 169
  | 0, 2 => -(60 : ℂ) / 169
  | 0, 3 => -(144 : ℂ) / 169
  | 1, 0 => (52 : ℂ) / 169
  | 1, 1 => (39 : ℂ) / 169
  | 1, 2 => -(144 : ℂ) / 169
  | 1, 3 => (60 : ℂ) / 169

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mottonen dense matrix unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem mottonenDenseMatrix_unitary :
    mottonenDenseMatrix ∈
      _root_.Matrix.unitaryGroup (Fin (gridSize 2)) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “mottonen dense gate”.

noncomputable def mottonenDenseGate : ComplexUnitaryGate 2 where
  matrix := mottonenDenseMatrix
  unitary := mottonenDenseMatrix_unitary

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “mottonen dense matrix prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem mottonenDenseMatrix_prepares_target :
    applyVec mottonenDenseMatrix (zeroKet 2) =
      mottonenDenseTarget.amplitudes := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “mottonen dense certificate”.

noncomputable def mottonenDenseCertificate :
    ComplexStatePreparationCertificate 2 where
  target := mottonenDenseTarget
  gate := mottonenDenseGate
  normalizationProof := mottonenDenseTarget_normalized
  preparationProof := mottonenDenseMatrix_prepares_target

/-! ## Structured Grover--Rudolph-style product distribution -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “grover rudolph product state”. Rational quaternion completion with first column '(39,52,60,144)/169'.

noncomputable def groverRudolphProductState : StateVector (gridSize 2) ℂ :=
  fun index =>
    match index.val with
    | 0 => (9 : ℂ) / 25
    | 1 => (12 : ℂ) / 25
    | 2 => (12 : ℂ) / 25
    | _ => (16 : ℂ) / 25

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “grover rudolph product target”.

noncomputable def groverRudolphProductTarget : StatePreparationTarget ℂ 2 where
  amplitudes := groverRudolphProductState
  normalization := ∑ index, Complex.normSq (groverRudolphProductState index) = 1
  source := "Grover--Rudolph structured product-distribution benchmark"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grover rudolph product target normalized”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem groverRudolphProductTarget_normalized :
    groverRudolphProductTarget.normalization := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “grover rudolph product matrix”.

noncomputable def groverRudolphProductMatrix :
    FiniteMatrix (gridSize 2) (gridSize 2) ℂ := fun row column =>
  match row.val, column.val with
  | 0, 0 => (9 : ℂ) / 25
  | 0, 1 => -(12 : ℂ) / 25
  | 0, 2 => -(12 : ℂ) / 25
  | 0, 3 => (16 : ℂ) / 25
  | 1, 0 => (12 : ℂ) / 25
  | 1, 1 => (9 : ℂ) / 25
  | 1, 2 => -(16 : ℂ) / 25
  | 1, 3 => -(12 : ℂ) / 25

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grover rudolph product matrix unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem groverRudolphProductMatrix_unitary :
    groverRudolphProductMatrix ∈
      _root_.Matrix.unitaryGroup (Fin (gridSize 2)) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “grover rudolph product gate”.

noncomputable def groverRudolphProductGate : ComplexUnitaryGate 2 where
  matrix := groverRudolphProductMatrix
  unitary := groverRudolphProductMatrix_unitary

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “grover rudolph product matrix prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem groverRudolphProductMatrix_prepares_target :
    applyVec groverRudolphProductMatrix (zeroKet 2) =
      groverRudolphProductTarget.amplitudes := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “grover rudolph product certificate”.

noncomputable def groverRudolphProductCertificate :
    ComplexStatePreparationCertificate 2 where
  target := groverRudolphProductTarget
  gate := groverRudolphProductGate
  normalizationProof := groverRudolphProductTarget_normalized
  preparationProof := groverRudolphProductMatrix_prepares_target

/-! ## Fixed three-sparse benchmark -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse three state”. Rational quaternion completion with first column '(39,52,60,144)/169'.

noncomputable def sparseThreeState : StateVector (gridSize 3) ℂ := fun index =>
  if index.val = 0 then (3 : ℂ) / 13
  else if index.val = 2 then (4 : ℂ) / 13
  else if index.val = 4 then (12 : ℂ) / 13
  else 0

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse three target”.

noncomputable def sparseThreeTarget : StatePreparationTarget ℂ 3 where
  amplitudes := sparseThreeState
  normalization := ∑ index, Complex.normSq (sparseThreeState index) = 1
  source := "Li--Luo sparse-state finite witness of Eq. (2), n=3 and d=3"

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse three target normalized”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseThreeTarget_normalized : sparseThreeTarget.normalization := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse three matrix”. Rational orthogonal completion on rows '0,2,4', identity on the complement.

noncomputable def sparseThreeMatrix :
    FiniteMatrix (gridSize 3) (gridSize 3) ℂ := fun row column =>
  match row.val, column.val with
  | 0, 0 => (3 : ℂ) / 13
  | 0, 1 => -(4 : ℂ) / 5
  | 0, 2 => -(36 : ℂ) / 65
  | 2, 0 => (4 : ℂ) / 13
  | 2, 1 => (3 : ℂ) / 5
  | 2, 2 => -(48 : ℂ) / 65
  | 4, 0 => (12 : ℂ) / 13
  | 4, 1 => 0

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse three matrix unitary”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseThreeMatrix_unitary :
    sparseThreeMatrix ∈
      _root_.Matrix.unitaryGroup (Fin (gridSize 3)) ℂ := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse three gate”.

noncomputable def sparseThreeGate : ComplexUnitaryGate 3 where
  matrix := sparseThreeMatrix
  unitary := sparseThreeMatrix_unitary

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “sparse three matrix prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sparseThreeMatrix_prepares_target :
    applyVec sparseThreeMatrix (zeroKet 3) = sparseThreeTarget.amplitudes := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “sparse three certificate”.

noncomputable def sparseThreeCertificate : ComplexStatePreparationCertificate 3 where
  target := sparseThreeTarget
  gate := sparseThreeGate
  normalizationProof := sparseThreeTarget_normalized
  preparationProof := sparseThreeMatrix_prepares_target

/-! ## Low--Kliuchnikov--Schaeffer SelectSwap resource arithmetic -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “select swap clean t count”. Rational orthogonal completion on rows '0,2,4', identity on the complement.

def selectSwapCleanTCount (N b lambda : Nat) : Nat :=
  4 * ((N + lambda - 1) / lambda) + 8 * b * lambda

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “select swap clean t count 16 1 1”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem selectSwapCleanTCount_16_1_1 :
    selectSwapCleanTCount 16 1 1 = 72 := by decide

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “select swap clean t count 16 1 4”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem selectSwapCleanTCount_16_1_4 :
    selectSwapCleanTCount 16 1 4 = 48 := by decide

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “select swap clean t count lambda 4 better lambda 1”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem selectSwapCleanTCount_lambda4_better_lambda1 :
    selectSwapCleanTCount 16 1 4 < selectSwapCleanTCount 16 1 1 := by decide

commit-pinned source · Verso Blueprint panel