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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. abbrev.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:22. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:25. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:28. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:41. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:70. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:81. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:89. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:96. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. 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'.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Rational quaternion completion with first column '(39,52,60,144)/169'.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:107. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:139. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:151. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. 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'.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. 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 | 2, 0 => (60 : ℂ) / 169 | 2, 1 => (144 : ℂ) / 169 | 2, 2 => (39 : ℂ) / 169 | 2, 3 => -(52 : ℂ) / 169 | 3, 0 => (144 : ℂ) / 169 | 3, 1 => -(60 : ℂ) / 169 | 3, 2 => (52 : ℂ) / 169 | _, _ => (39 : ℂ) / 169 theorem mottonenDenseMatrix_unitary : mottonenDenseMatrix ∈ _root_.Matrix.unitaryGroup (Fin (gridSize 2)) ℂ := by rw [_root_.Matrix.mem_unitaryGroup_iff'] ext row column fin_cases row <;> fin_cases column <;> rw [_root_.Matrix.mul_apply, Finset.sum_fin_eq_sum_range] <;> norm_num [mottonenDenseMatrix, Finset.sum_range_succ, gridSize, _root_.Matrix.star_apply] <;> simp only [starRingEnd_apply, star_ofNat] <;> norm_num noncomputable def mottonenDenseGate : ComplexUnitaryGate 2 where matrix := mottonenDenseMatrix unitary := mottonenDenseMatrix_unitary theorem mottonenDenseMatrix_prepares_target : applyVec mottonenDenseMatrix (zeroKet 2) = mottonenDenseTarget.amplitudes := by rw [applyVec_zeroKet] change mottonenDenseMatrix.col (0 : Fin 4) = mottonenDenseState funext row fin_cases row <;> norm_num [mottonenDenseMatrix, mottonenDenseState] noncomputable def mottonenDenseCertificate : ComplexStatePreparationCertificate 2 where target := mottonenDenseTarget gate := mottonenDenseGate normalizationProof := mottonenDenseTarget_normalized preparationProof := mottonenDenseMatrix_prepares_target /-! number number Structured Grover--Rudolph-style product distribution

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:160. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:168. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:180. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:212. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:225. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. 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'.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. 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 | 2, 0 => (60 : ℂ) / 169 | 2, 1 => (144 : ℂ) / 169 | 2, 2 => (39 : ℂ) / 169 | 2, 3 => -(52 : ℂ) / 169 | 3, 0 => (144 : ℂ) / 169 | 3, 1 => -(60 : ℂ) / 169 | 3, 2 => (52 : ℂ) / 169 | _, _ => (39 : ℂ) / 169 theorem mottonenDenseMatrix_unitary : mottonenDenseMatrix ∈ _root_.Matrix.unitaryGroup (Fin (gridSize 2)) ℂ := by rw [_root_.Matrix.mem_unitaryGroup_iff'] ext row column fin_cases row <;> fin_cases column <;> rw [_root_.Matrix.mul_apply, Finset.sum_fin_eq_sum_range] <;> norm_num [mottonenDenseMatrix, Finset.sum_range_succ, gridSize, _root_.Matrix.star_apply] <;> simp only [starRingEnd_apply, star_ofNat] <;> norm_num noncomputable def mottonenDenseGate : ComplexUnitaryGate 2 where matrix := mottonenDenseMatrix unitary := mottonenDenseMatrix_unitary theorem mottonenDenseMatrix_prepares_target : applyVec mottonenDenseMatrix (zeroKet 2) = mottonenDenseTarget.amplitudes := by rw [applyVec_zeroKet] change mottonenDenseMatrix.col (0 : Fin 4) = mottonenDenseState funext row fin_cases row <;> norm_num [mottonenDenseMatrix, mottonenDenseState] noncomputable def mottonenDenseCertificate : ComplexStatePreparationCertificate 2 where target := mottonenDenseTarget gate := mottonenDenseGate normalizationProof := mottonenDenseTarget_normalized preparationProof := mottonenDenseMatrix_prepares_target /-! number number Structured Grover--Rudolph-style product distribution -/ noncomputable def groverRudolphProductState : StateVector (gridSize 2) ℂ := fun index => match index.val with | 0 => (9 : ℂ) / 25 | 1 => (12 : ℂ) / 25 | 2 => (12 : ℂ) / 25 | _ => (16 : ℂ) / 25 noncomputable def groverRudolphProductTarget : StatePreparationTarget ℂ 2 where amplitudes := groverRudolphProductState normalization := ∑ index, Complex.normSq (groverRudolphProductState index) = 1 source := "Grover--Rudolph structured product-distribution benchmark" theorem groverRudolphProductTarget_normalized : groverRudolphProductTarget.normalization := by change ∑ index : Fin 4, Complex.normSq (groverRudolphProductState index) = 1 rw [Finset.sum_fin_eq_sum_range] norm_num [groverRudolphProductState, Complex.normSq_apply, Finset.sum_range_succ] 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 | 2, 0 => (12 : ℂ) / 25 | 2, 1 => -(16 : ℂ) / 25 | 2, 2 => (9 : ℂ) / 25 | 2, 3 => -(12 : ℂ) / 25 | 3, 0 => (16 : ℂ) / 25 | 3, 1 => (12 : ℂ) / 25 | 3, 2 => (12 : ℂ) / 25 | _, _ => (9 : ℂ) / 25 theorem groverRudolphProductMatrix_unitary : groverRudolphProductMatrix ∈ _root_.Matrix.unitaryGroup (Fin (gridSize 2)) ℂ := by rw [_root_.Matrix.mem_unitaryGroup_iff'] ext row column fin_cases row <;> fin_cases column <;> rw [_root_.Matrix.mul_apply, Finset.sum_fin_eq_sum_range] <;> norm_num [groverRudolphProductMatrix, Finset.sum_range_succ, gridSize, _root_.Matrix.star_apply] <;> simp only [starRingEnd_apply, star_ofNat] <;> norm_num noncomputable def groverRudolphProductGate : ComplexUnitaryGate 2 where matrix := groverRudolphProductMatrix unitary := groverRudolphProductMatrix_unitary theorem groverRudolphProductMatrix_prepares_target : applyVec groverRudolphProductMatrix (zeroKet 2) = groverRudolphProductTarget.amplitudes := by rw [applyVec_zeroKet] change groverRudolphProductMatrix.col (0 : Fin 4) = groverRudolphProductState funext row fin_cases row <;> norm_num [groverRudolphProductMatrix, groverRudolphProductState] noncomputable def groverRudolphProductCertificate : ComplexStatePreparationCertificate 2 where target := groverRudolphProductTarget gate := groverRudolphProductGate normalizationProof := groverRudolphProductTarget_normalized preparationProof := groverRudolphProductMatrix_prepares_target /-! number number Fixed three-sparse benchmark

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:234. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:240. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. 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.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Rational orthogonal completion on rows '0,2,4', identity on the complement.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:251. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:283. A commit-pinned external link is added by the publication build when the source exists at the published ref.

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

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. The source declaration has no docstring. The reader cue above is generated from its kind and name and does not replace the Lean signature.

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:294. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Plain-English reading. 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.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

Why it is in this chapter. Paper-facing backend models, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. 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 | 4, 2 => (25 : ℂ) / 65 | 1, 3 => 1 | 3, 4 => 1 | 5, 5 => 1 | 6, 6 => 1 | 7, 7 => 1 | _, _ => 0 set_option maxHeartbeats 1000000 in theorem sparseThreeMatrix_unitary : sparseThreeMatrix ∈ _root_.Matrix.unitaryGroup (Fin (gridSize 3)) ℂ := by rw [_root_.Matrix.mem_unitaryGroup_iff'] ext row column fin_cases row <;> fin_cases column <;> rw [_root_.Matrix.mul_apply, Finset.sum_fin_eq_sum_range] <;> norm_num [sparseThreeMatrix, Finset.sum_range_succ, gridSize, _root_.Matrix.star_apply] <;> simp only [starRingEnd_apply, star_ofNat] <;> norm_num noncomputable def sparseThreeGate : ComplexUnitaryGate 3 where matrix := sparseThreeMatrix unitary := sparseThreeMatrix_unitary theorem sparseThreeMatrix_prepares_target : applyVec sparseThreeMatrix (zeroKet 3) = sparseThreeTarget.amplitudes := by rw [applyVec_zeroKet] change sparseThreeMatrix.col (0 : Fin 8) = sparseThreeState funext row fin_cases row <;> norm_num [sparseThreeMatrix, sparseThreeState] noncomputable def sparseThreeCertificate : ComplexStatePreparationCertificate 3 where target := sparseThreeTarget gate := sparseThreeGate normalizationProof := sparseThreeTarget_normalized preparationProof := sparseThreeMatrix_prepares_target /-! number number Low--Kliuchnikov--Schaeffer SelectSwap resource arithmetic

Declaration kind. def.

Source: QuantumBlockEncoding/StatePreparationBenchmarksCoreFixed.lean:302. A commit-pinned external link is added by the publication build when the source exists at the published ref.