ASPBE Lean Blueprint

10.57. QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean🔗

31 explicit public declarations, in source order.

Definition10.57.1
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.57.1●1 definition
  • defdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    def QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
  {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
    (QuantumBlockEncoding.gridSize qubits)
    (QuantumBlockEncoding.gridSize qubits) ℂ
    def QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  QuantumBlockEncoding.ConcreteSemantics.FiniteMatrix
    (QuantumBlockEncoding.gridSize qubits)
    (QuantumBlockEncoding.gridSize qubits)
    ℂ
Theorem10.57.2
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval primitive circuit le unitary”; 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/StatePreparationPrimitiveRoutes.lean:27. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.2●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE_unitary
  {qubits : ℕ}
  (circuit : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      circuit ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize qubits)) ℂ
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE_unitary
  {qubits : ℕ}
  (circuit :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      circuit ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize
          qubits))
      ℂ
Definition10.57.3
uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “exact primitive state preparation route”. A proposition-valued field is a requirement until a constructor supplies it.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

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

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

Lean code for Definition10.57.3●1 definition
  • structure(4 fields)defined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    structure QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
  (qubits : ℕ) : Type
    structure QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
  (qubits : ℕ) : Type

    Fields

    target : QuantumBlockEncoding.StatePreparationTarget ℂ qubits
    circuit : QuantumBlockEncoding.PrimitiveCircuit qubits
    normalizationProof : self.target.normalization
    preparationProof : QuantumBlockEncoding.ConcreteSemantics.applyVec
    (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE self.circuit)
    (QuantumBlockEncoding.ConcreteSemantics.zeroKet qubits) =
  self.target.amplitudes
Definition10.57.4
uses 0used by 0✓L∃∀N

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

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/StatePreparationPrimitiveRoutes.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.57.4●1 definition
  • defdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    def QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute.cost
  {qubits : ℕ}
  (route :
    QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
      qubits) :
  QuantumBlockEncoding.BlockEncodingCost
    def QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute.cost
  {qubits : ℕ}
  (route :
    QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
      qubits) :
  QuantumBlockEncoding.BlockEncodingCost
Theorem10.57.5
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “unitary”; 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/StatePreparationPrimitiveRoutes.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.57.5●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute.unitary
  {qubits : ℕ}
  (route :
    QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
      qubits) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      route.circuit ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize qubits)) ℂ
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute.unitary
  {qubits : ℕ}
  (route :
    QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
      qubits) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      route.circuit ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize
          qubits))
      ℂ
Definition10.57.6
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.57.6●1 definition
Definition10.57.7
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.57.7●1 definition
Definition10.57.8
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.57.8●1 definition
Theorem10.57.9
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry matrix ry angle 35”; 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/StatePreparationPrimitiveRoutes.lean:93. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.9●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.standardRyMatrix_ryAngle35 :
  QuantumBlockEncoding.standardRyMatrix
      QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle35.eval =
    QuantumBlockEncoding.Robin.ComplexLCU.realOrthogonalRotation
      ↑QuantumBlockEncoding.StatePreparationBenchmarks.cosine35✝
      ↑QuantumBlockEncoding.StatePreparationBenchmarks.sine35✝
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.standardRyMatrix_ryAngle35 :
  QuantumBlockEncoding.standardRyMatrix
      QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle35.eval =
    QuantumBlockEncoding.Robin.ComplexLCU.realOrthogonalRotation
      ↑QuantumBlockEncoding.StatePreparationBenchmarks.cosine35✝
      ↑QuantumBlockEncoding.StatePreparationBenchmarks.sine35✝
Theorem10.57.10
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry matrix ry angle 513”; 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/StatePreparationPrimitiveRoutes.lean:109. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.10●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.standardRyMatrix_ryAngle513 :
  QuantumBlockEncoding.standardRyMatrix
      QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle513.eval =
    QuantumBlockEncoding.Robin.ComplexLCU.realOrthogonalRotation
      ↑QuantumBlockEncoding.StatePreparationBenchmarks.cosine513✝
      ↑QuantumBlockEncoding.StatePreparationBenchmarks.sine513✝
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.standardRyMatrix_ryAngle513 :
  QuantumBlockEncoding.standardRyMatrix
      QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle513.eval =
    QuantumBlockEncoding.Robin.ComplexLCU.realOrthogonalRotation
      ↑QuantumBlockEncoding.StatePreparationBenchmarks.cosine513✝
      ↑QuantumBlockEncoding.StatePreparationBenchmarks.sine513✝
Theorem10.57.11
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “standard ry matrix ry angle 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/StatePreparationPrimitiveRoutes.lean:125. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.11●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.standardRyMatrix_ryAngleZero :
  QuantumBlockEncoding.standardRyMatrix
      QuantumBlockEncoding.StatePreparationBenchmarks.ryAngleZero.eval =
    1
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.standardRyMatrix_ryAngleZero :
  QuantumBlockEncoding.standardRyMatrix
      QuantumBlockEncoding.StatePreparationBenchmarks.ryAngleZero.eval =
    1
Definition10.57.12
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.57.12●1 definition
  • defdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    def QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
  (qubits : ℕ) (index : Fin (QuantumBlockEncoding.gridSize qubits)) :
  QuantumBlockEncoding.PrimitiveBasis qubits
    def QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
  (qubits : ℕ)
  (index :
    Fin
      (QuantumBlockEncoding.gridSize
        qubits)) :
  QuantumBlockEncoding.PrimitiveBasis
    qubits
Theorem10.57.13
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval primitive circuit le append”; 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/StatePreparationPrimitiveRoutes.lean:135. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.13●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE_append
  {qubits : ℕ}
  (left right : QuantumBlockEncoding.PrimitiveCircuit qubits) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      (left ++ right) =
    QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        right *
      QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        left
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE_append
  {qubits : ℕ}
  (left right :
    QuantumBlockEncoding.PrimitiveCircuit
      qubits) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      (left ++ right) =
    QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        right *
      QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        left
Theorem10.57.14
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval primitive circuit le singleton ry 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/StatePreparationPrimitiveRoutes.lean:142. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.14●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE_singleton_ry_apply
  {qubits : ℕ} (target : Fin qubits)
  (angle : QuantumBlockEncoding.ExactAngle)
  (row column : Fin (QuantumBlockEncoding.gridSize qubits)) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      [QuantumBlockEncoding.PrimitiveGate.ry target angle] row column =
    if
        ((QuantumBlockEncoding.splitPrimitiveWire target)
              (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
                qubits row)).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire target)
              (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
                qubits column)).2 then
      QuantumBlockEncoding.standardRyMatrix angle.eval
        (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
          qubits row target)
        (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
          qubits column target)
    else 0
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE_singleton_ry_apply
  {qubits : ℕ} (target : Fin qubits)
  (angle :
    QuantumBlockEncoding.ExactAngle)
  (row column :
    Fin
      (QuantumBlockEncoding.gridSize
        qubits)) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      [QuantumBlockEncoding.PrimitiveGate.ry
          target angle]
      row column =
    if
        ((QuantumBlockEncoding.splitPrimitiveWire
                target)
              (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
                qubits row)).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire
                target)
              (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
                qubits column)).2 then
      QuantumBlockEncoding.standardRyMatrix
        angle.eval
        (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
          qubits row target)
        (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
          qubits column target)
    else 0
Theorem10.57.15
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eval primitive circuit le compile uniformly controlled ry 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/StatePreparationPrimitiveRoutes.lean:157. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.15●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE_compileUniformlyControlledRy_apply
  {qubits controls : ℕ} (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis controls →
      QuantumBlockEncoding.ExactAngle)
  (row column : Fin (QuantumBlockEncoding.gridSize qubits)) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      (QuantumBlockEncoding.compileUniformlyControlledRy controls wires
        target distinct angles)
      row column =
    if
        ((QuantumBlockEncoding.splitPrimitiveWire target)
              (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
                qubits row)).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire target)
              (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
                qubits column)).2 then
      QuantumBlockEncoding.standardRyMatrix
        (angles
            (QuantumBlockEncoding.primitiveControlAssignment wires
              target distinct
              ((QuantumBlockEncoding.splitPrimitiveWire target)
                  (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
                    qubits row)).2)).eval
        (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
          qubits row target)
        (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
          qubits column target)
    else 0
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE_compileUniformlyControlledRy_apply
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target)
  (angles :
    QuantumBlockEncoding.PrimitiveBasis
        controls →
      QuantumBlockEncoding.ExactAngle)
  (row column :
    Fin
      (QuantumBlockEncoding.gridSize
        qubits)) :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      (QuantumBlockEncoding.compileUniformlyControlledRy
        controls wires target distinct
        angles)
      row column =
    if
        ((QuantumBlockEncoding.splitPrimitiveWire
                target)
              (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
                qubits row)).2 =
          ((QuantumBlockEncoding.splitPrimitiveWire
                target)
              (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
                qubits column)).2 then
      QuantumBlockEncoding.standardRyMatrix
        (angles
            (QuantumBlockEncoding.primitiveControlAssignment
              wires target distinct
              ((QuantumBlockEncoding.splitPrimitiveWire
                    target)
                  (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
                    qubits row)).2)).eval
        (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
          qubits row target)
        (QuantumBlockEncoding.StatePreparationBenchmarks.primitiveLEBits
          qubits column target)
    else 0
Definition10.57.16
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “grover rudolph control 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/StatePreparationPrimitiveRoutes.lean:183. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.57.16●1 definition
Theorem10.57.17
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grover rudolph control wire 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/StatePreparationPrimitiveRoutes.lean:185. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.17●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphControlWire_ne_target
  (control : Fin 1) :
  QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphControlWire
      control ≠
    0
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphControlWire_ne_target
  (control : Fin 1) :
  QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphControlWire
      control ≠
    0
Definition10.57.18
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.57.18●1 definition
  • defdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    def QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphConstantAngles :
  QuantumBlockEncoding.PrimitiveBasis 1 →
    QuantumBlockEncoding.ExactAngle
    def QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphConstantAngles :
  QuantumBlockEncoding.PrimitiveBasis 1 →
    QuantumBlockEncoding.ExactAngle
Definition10.57.19
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “grover rudolph tree circuit”. Generic binary-tree route: a root split followed by a one-control UCRY.

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. Generic binary-tree route: a root split followed by a one-control UCRY.

Declaration kind. def.

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

Lean code for Definition10.57.19●1 definition
  • defdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    def QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2
    def QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2
    Generic binary-tree route: a root split followed by a one-control UCRY.
Definition10.57.20
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “grover rudolph factorized circuit”. Product-aware route: the two independent rotations can occupy one layer.

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. Product-aware route: the two independent rotations can occupy one layer.

Declaration kind. def.

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

Lean code for Definition10.57.20●1 definition
  • defdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    def QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2
    def QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2
    Product-aware route: the two independent rotations can occupy one layer.
Theorem10.57.21
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grover rudolph constant ucry 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/StatePreparationPrimitiveRoutes.lean:205. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.21●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphConstantUcry_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy 1
        QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphControlWire
        0
        QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphControlWire_ne_target
        QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphConstantAngles) =
    QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.PrimitiveGate.ry 0
        QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle35)
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphConstantUcry_eval :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy
        1
        QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphControlWire
        0
        QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphControlWire_ne_target
        QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphConstantAngles) =
    QuantumBlockEncoding.evalPrimitiveGate
      (QuantumBlockEncoding.PrimitiveGate.ry
        0
        QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle35)
Theorem10.57.22
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grover rudolph tree eval eq factorized”; 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/StatePreparationPrimitiveRoutes.lean:215. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.22●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTree_eval_eq_factorized :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeCircuit =
    QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedCircuit
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTree_eval_eq_factorized :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeCircuit =
    QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedCircuit
Theorem10.57.23
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grover rudolph tree eval le eq factorized”; 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/StatePreparationPrimitiveRoutes.lean:223. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.23●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTree_evalLE_eq_factorized :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeCircuit =
    QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedCircuit
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTree_evalLE_eq_factorized :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeCircuit =
    QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedCircuit
Theorem10.57.24
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grover rudolph factorized eval le eq matrix”; 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/StatePreparationPrimitiveRoutes.lean:229. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.24●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_evalLE_eq_matrix :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedCircuit =
    QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphProductMatrix
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_evalLE_eq_matrix :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedCircuit =
    QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphProductMatrix
Theorem10.57.25
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grover rudolph factorized 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/StatePreparationPrimitiveRoutes.lean:243. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.25●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphProductTarget.amplitudes
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphProductTarget.amplitudes
Theorem10.57.26
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grover rudolph tree 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/StatePreparationPrimitiveRoutes.lean:249. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.26●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTree_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphProductTarget.amplitudes
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTree_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphProductTarget.amplitudes
Definition10.57.27
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “grover rudolph factorized 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/StatePreparationPrimitiveRoutes.lean:255. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.57.27●1 definition
  • defdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    def QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    2
    def QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    2
Definition10.57.28
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “grover rudolph tree 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/StatePreparationPrimitiveRoutes.lean:262. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.57.28●1 definition
  • defdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    def QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    2
    def QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    2
Theorem10.57.29
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grover rudolph factorized 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/StatePreparationPrimitiveRoutes.lean:269. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.29●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedRoute.cost =
    { auxiliaryQubits := 0, gateCount := 2, depth := 1,
      oracleCalls := 0 }
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedRoute.cost =
    { auxiliaryQubits := 0,
      gateCount := 2, depth := 1,
      oracleCalls := 0 }
Theorem10.57.30
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grover rudolph tree 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/StatePreparationPrimitiveRoutes.lean:274. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.30●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeRoute.cost =
    { auxiliaryQubits := 0, gateCount := 5, depth := 4,
      oracleCalls := 0 }
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeRoute.cost =
    { auxiliaryQubits := 0,
      gateCount := 5, depth := 4,
      oracleCalls := 0 }
Theorem10.57.31
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grover rudolph factorized better than tree”; 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/StatePreparationPrimitiveRoutes.lean:279. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.57.31●1 theorem
  • theoremdefined in QuantumBlockEncoding/StatePreparationPrimitiveRoutes.lean
    complete
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_betterThan_tree :
  QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedRoute.cost.betterThan
    QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeRoute.cost
    theorem QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorized_betterThan_tree :
  QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphFactorizedRoute.cost.betterThan
    QuantumBlockEncoding.StatePreparationBenchmarks.groverRudolphTreeRoute.cost