10.53. QuantumBlockEncoding/StatePreparationBellRoute.lean🔗

17 explicit public declarations, in source order.

Definition10.53.1

uses 0used by 0✓L∃∀N

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

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/StatePreparationBellRoute.lean:18. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.53.1●1 definition

defdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.bellRyAngle :
  QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.StatePreparationBenchmarks.bellRyAngle :
  QuantumBlockEncoding.ExactAngle

Theorem10.53.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “bell ry angle eval”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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. theorem.

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

Lean code for Theorem10.53.2●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellRyAngle_eval :
  QuantumBlockEncoding.StatePreparationBenchmarks.bellRyAngle.eval =
    Real.pi / 2

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellRyAngle_eval :
  QuantumBlockEncoding.StatePreparationBenchmarks.bellRyAngle.eval =
    Real.pi / 2

Theorem10.53.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry matrix bell ry angle”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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. theorem.

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

Lean code for Theorem10.53.3●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.standardRyMatrix_bellRyAngle :
  QuantumBlockEncoding.standardRyMatrix
      QuantumBlockEncoding.StatePreparationBenchmarks.bellRyAngle.eval =
    QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare

theorem QuantumBlockEncoding.StatePreparationBenchmarks.standardRyMatrix_bellRyAngle :
  QuantumBlockEncoding.standardRyMatrix
      QuantumBlockEncoding.StatePreparationBenchmarks.bellRyAngle.eval =
    QuantumBlockEncoding.Robin.warmRobinUniformBitPrepare

Definition10.53.4

uses 0used by 0✓L∃∀N

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

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/StatePreparationBellRoute.lean:31. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.53.4●1 definition

defdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.bellControl : Fin 2

def QuantumBlockEncoding.StatePreparationBenchmarks.bellControl :
  Fin 2

Definition10.53.5

uses 0used by 0✓L∃∀N

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

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/StatePreparationBellRoute.lean:33. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.53.5●1 definition

defdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.bellTargetWire : Fin 2

def QuantumBlockEncoding.StatePreparationBenchmarks.bellTargetWire :
  Fin 2

Theorem10.53.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “bell control ne target”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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. theorem.

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

Lean code for Theorem10.53.6●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellControl_ne_target :
  QuantumBlockEncoding.StatePreparationBenchmarks.bellControl ≠
    QuantumBlockEncoding.StatePreparationBenchmarks.bellTargetWire

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellControl_ne_target :
  QuantumBlockEncoding.StatePreparationBenchmarks.bellControl ≠
    QuantumBlockEncoding.StatePreparationBenchmarks.bellTargetWire

Definition10.53.7

uses 0used by 0✓L∃∀N

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

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/StatePreparationBellRoute.lean:38. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.53.7●1 definition

defdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.bellRyCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

def QuantumBlockEncoding.StatePreparationBenchmarks.bellRyCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

Definition10.53.8

uses 0used by 0✓L∃∀N

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

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/StatePreparationBellRoute.lean:41. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.53.8●1 definition

defdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.bellCxCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

def QuantumBlockEncoding.StatePreparationBenchmarks.bellCxCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

Definition10.53.9

uses 0used by 0✓L∃∀N

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

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/StatePreparationBellRoute.lean:44. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.53.9●1 definition

defdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.bellPrimitiveCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

def QuantumBlockEncoding.StatePreparationBenchmarks.bellPrimitiveCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

Definition10.53.10

uses 0used by 0✓L∃∀N

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

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/StatePreparationBellRoute.lean:47. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.53.10●1 definition

defdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.bellAfterRy :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    (QuantumBlockEncoding.gridSize 2) ℂ

def QuantumBlockEncoding.StatePreparationBenchmarks.bellAfterRy :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    (QuantumBlockEncoding.gridSize 2) ℂ

Theorem10.53.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval primitive circuit le singleton cx apply”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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. theorem.

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

Lean code for Theorem10.53.11●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE_singleton_cx_apply
  {qubits : ℕ} (control target : Fin qubits)
  (distinct : control ≠ target)
  (row column : Fin (QuantumBlockEncoding.gridSize qubits)) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      [QuantumBlockEncoding.PrimitiveGate.cx control target distinct]
      row column =
    if
        QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
            qubits row =
          (QuantumBlockEncoding.cxBasisEquiv control target distinct)
            (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
              qubits column) then
      1
    else 0

theorem QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE_singleton_cx_apply
  {qubits : ℕ}
  (control target : Fin qubits)
  (distinct : control ≠ target)
  (row column :
    Fin
      (QuantumBlockEncoding.gridSize
        qubits)) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      [QuantumBlockEncoding.PrimitiveGate.cx
          control target distinct]
      row column =
    if
        QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
            qubits row =
          (QuantumBlockEncoding.cxBasisEquiv
              control target distinct)
            (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
              qubits column) then
      1
    else 0

Theorem10.53.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “bell ry col zero”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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. theorem.

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

Lean code for Theorem10.53.12●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellRy_col_zero :
  Matrix.col
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.bellRyCircuit)
      0 =
    QuantumBlockEncoding.StatePreparationBenchmarks.bellAfterRy

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellRy_col_zero :
  Matrix.col
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.bellRyCircuit)
      0 =
    QuantumBlockEncoding.StatePreparationBenchmarks.bellAfterRy

Theorem10.53.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “bell ry prepares”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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. theorem.

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

Lean code for Theorem10.53.13●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellRy_prepares :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.bellRyCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.bellAfterRy

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellRy_prepares :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.bellRyCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.bellAfterRy

Theorem10.53.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “bell cx on after ry”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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. theorem.

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

Lean code for Theorem10.53.14●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellCx_on_afterRy :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.bellCxCircuit)
      QuantumBlockEncoding.StatePreparationBenchmarks.bellAfterRy =
    QuantumBlockEncoding.StatePreparationBenchmarks.bellState

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellCx_on_afterRy :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.bellCxCircuit)
      QuantumBlockEncoding.StatePreparationBenchmarks.bellAfterRy =
    QuantumBlockEncoding.StatePreparationBenchmarks.bellState

Theorem10.53.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “bell primitive prepares target”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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. theorem.

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

Lean code for Theorem10.53.15●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellPrimitive_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.bellPrimitiveCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.bellTarget.amplitudes

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellPrimitive_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.bellPrimitiveCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.bellTarget.amplitudes

Definition10.53.16

uses 0used by 0✓L∃∀N

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

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/StatePreparationBellRoute.lean:254. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.53.16●1 definition

defdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.bellPrimitiveRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    2

def QuantumBlockEncoding.StatePreparationBenchmarks.bellPrimitiveRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    2

Theorem10.53.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “bell verified cost”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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. theorem.

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

Lean code for Theorem10.53.17●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationBellRoute.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.bellPrimitiveRoute.cost =
    { auxiliaryQubits := 0, gateCount := 2, depth := 2,
      oracleCalls := 0 }

theorem QuantumBlockEncoding.StatePreparationBenchmarks.bellVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.bellPrimitiveRoute.cost =
    { auxiliaryQubits := 0,
      gateCount := 2, depth := 2,
      oracleCalls := 0 }