10.56. QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean🔗

34 explicit public declarations, in source order.

Definition10.56.1

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.1●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.mottonenConditionalAngles :
  QuantumBlockEncoding.PrimitiveBasis 1 →
    QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.StatePreparationBenchmarks.mottonenConditionalAngles :
  QuantumBlockEncoding.PrimitiveBasis 1 →
    QuantumBlockEncoding.ExactAngle

Definition10.56.2

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.2●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseUcryCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

def QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseUcryCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

Definition10.56.3

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.3●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitiveCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

def QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitiveCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 2

Definition10.56.4

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.4●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

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

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

Theorem10.56.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.5●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.mottonenRootRy_col_zero :
  Matrix.col
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        [QuantumBlockEncoding.PrimitiveGate.ry 1
            QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle513])
      0 =
    QuantumBlockEncoding.StatePreparationBenchmarks.mottonenRootState

theorem QuantumBlockEncoding.StatePreparationBenchmarks.mottonenRootRy_col_zero :
  Matrix.col
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        [QuantumBlockEncoding.PrimitiveGate.ry
            1
            QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle513])
      0 =
    QuantumBlockEncoding.StatePreparationBenchmarks.mottonenRootState

Theorem10.56.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.6●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.mottonenRootRy_prepares :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        [QuantumBlockEncoding.PrimitiveGate.ry 1
            QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle513])
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.mottonenRootState

theorem QuantumBlockEncoding.StatePreparationBenchmarks.mottonenRootRy_prepares :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        [QuantumBlockEncoding.PrimitiveGate.ry
            1
            QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle513])
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.mottonenRootState

Theorem10.56.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “mottonen dense ucry on root”; 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/StatePreparationPaperRoutesCompact.lean:180. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.56.7●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseUcry_on_root :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseUcryCircuit)
      QuantumBlockEncoding.StatePreparationBenchmarks.mottonenRootState =
    QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseState

theorem QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseUcry_on_root :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseUcryCircuit)
      QuantumBlockEncoding.StatePreparationBenchmarks.mottonenRootState =
    QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseState

Theorem10.56.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.8●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitive_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitiveCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseTarget.amplitudes

theorem QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitive_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitiveCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        2) =
    QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseTarget.amplitudes

Definition10.56.9

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.9●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitiveRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    2

def QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitiveRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    2

Theorem10.56.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.10●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitiveRoute.cost =
    { auxiliaryQubits := 0, gateCount := 5, depth := 4,
      oracleCalls := 0 }

theorem QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDenseVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.mottonenDensePrimitiveRoute.cost =
    { auxiliaryQubits := 0,
      gateCount := 5, depth := 4,
      oracleCalls := 0 }

Theorem10.56.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “zero angle compiled ucry eval eq one”; 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/StatePreparationPaperRoutesCompact.lean:255. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.56.11●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.zeroAngleCompiledUcry_eval_eq_one
  {qubits controls : ℕ} (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct : ∀ (control : Fin controls), wires control ≠ target) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy controls wires
        target distinct fun x =>
        QuantumBlockEncoding.StatePreparationBenchmarks.ryAngleZero) =
    1

theorem QuantumBlockEncoding.StatePreparationBenchmarks.zeroAngleCompiledUcry_eval_eq_one
  {qubits controls : ℕ}
  (wires : Fin controls → Fin qubits)
  (target : Fin qubits)
  (distinct :
    ∀ (control : Fin controls),
      wires control ≠ target) :
  QuantumBlockEncoding.evalPrimitiveCircuit
      (QuantumBlockEncoding.compileUniformlyControlledRy
        controls wires target distinct
        fun x =>
        QuantumBlockEncoding.StatePreparationBenchmarks.ryAngleZero) =
    1

Definition10.56.12

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.12●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseControlWire :
  Fin 1 → Fin 3

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseControlWire :
  Fin 1 → Fin 3

Theorem10.56.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.13●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseControlWire_ne_target
  (control : Fin 1) :
  QuantumBlockEncoding.StatePreparationBenchmarks.sparseControlWire
      control ≠
    1

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseControlWire_ne_target
  (control : Fin 1) :
  QuantumBlockEncoding.StatePreparationBenchmarks.sparseControlWire
      control ≠
    1

Definition10.56.14

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.14●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseConditionalAngles :
  QuantumBlockEncoding.PrimitiveBasis 1 →
    QuantumBlockEncoding.ExactAngle

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseConditionalAngles :
  QuantumBlockEncoding.PrimitiveBasis 1 →
    QuantumBlockEncoding.ExactAngle

Definition10.56.15

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.15●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedUcryCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

def QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedUcryCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

Definition10.56.16

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.16●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

def QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

Definition10.56.17

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.17●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootState :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    (QuantumBlockEncoding.gridSize 3) ℂ

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootState :
  QuantumBlockEncoding.ConcreteSemantics.StateVector
    (QuantumBlockEncoding.gridSize 3) ℂ

Theorem10.56.18

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.18●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootRy_col_zero :
  Matrix.col
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        [QuantumBlockEncoding.PrimitiveGate.ry 2
            QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle513])
      0 =
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootState

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootRy_col_zero :
  Matrix.col
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        [QuantumBlockEncoding.PrimitiveGate.ry
            2
            QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle513])
      0 =
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootState

Theorem10.56.19

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.19●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootRy_prepares :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        [QuantumBlockEncoding.PrimitiveGate.ry 2
            QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle513])
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 3) =
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootState

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootRy_prepares :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        [QuantumBlockEncoding.PrimitiveGate.ry
            2
            QuantumBlockEncoding.StatePreparationBenchmarks.ryAngle513])
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        3) =
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootState

Theorem10.56.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse pruned ucry on root”; 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/StatePreparationPaperRoutesCompact.lean:497. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.56.20●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedUcry_on_root :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedUcryCircuit)
      QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootState =
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeState

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedUcry_on_root :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedUcryCircuit)
      QuantumBlockEncoding.StatePreparationBenchmarks.sparseRootState =
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeState

Theorem10.56.21

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.21●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparsePruned_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 3) =
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeTarget.amplitudes

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparsePruned_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        3) =
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeTarget.amplitudes

Definition10.56.22

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.22●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    3

def QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    3

Definition10.56.23

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.56.23●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseControlWires :
  Fin 2 → Fin 3

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseControlWires :
  Fin 2 → Fin 3

Theorem10.56.24

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse dense control wires 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/StatePreparationPaperRoutesCompact.lean:602. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.56.24●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseControlWires_ne_target
  (control : Fin 2) :
  QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseControlWires
      control ≠
    0

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseControlWires_ne_target
  (control : Fin 2) :
  QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseControlWires
      control ≠
    0

Definition10.56.25

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.25●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseZeroFillCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseZeroFillCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

Definition10.56.26

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.26●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeCircuit :
  QuantumBlockEncoding.PrimitiveCircuit 3

Theorem10.56.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse zero fill eval eq one”; 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/StatePreparationPaperRoutesCompact.lean:614. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.56.27●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseZeroFill_eval_eq_one :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.StatePreparationBenchmarks.sparseZeroFillCircuit =
    1

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseZeroFill_eval_eq_one :
  QuantumBlockEncoding.evalPrimitiveCircuit
      QuantumBlockEncoding.StatePreparationBenchmarks.sparseZeroFillCircuit =
    1

Theorem10.56.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse zero fill eval le eq one”; 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/StatePreparationPaperRoutesCompact.lean:620. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.56.28●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseZeroFill_evalLE_eq_one :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.sparseZeroFillCircuit =
    1

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseZeroFill_evalLE_eq_one :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.sparseZeroFillCircuit =
    1

Theorem10.56.29

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.29●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTree_evalLE_eq_pruned :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeCircuit =
    QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedCircuit

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTree_evalLE_eq_pruned :
  QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeCircuit =
    QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
      QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedCircuit

Theorem10.56.30

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.30●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTree_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet 3) =
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeTarget.amplitudes

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTree_prepares_target :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.StatePreparationBenchmarks.evalPrimitiveCircuitLE
        QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeCircuit)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        3) =
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseThreeTarget.amplitudes

Definition10.56.31

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.56.31●1 definition

defdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    3

def QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeRoute :
  QuantumBlockEncoding.StatePreparationBenchmarks.ExactPrimitiveStatePreparationRoute
    3

Theorem10.56.32

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.32●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedRoute.cost =
    { auxiliaryQubits := 0, gateCount := 5, depth := 4,
      oracleCalls := 0 }

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedRoute.cost =
    { auxiliaryQubits := 0,
      gateCount := 5, depth := 4,
      oracleCalls := 0 }

Theorem10.56.33

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.56.33●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeRoute.cost =
    { auxiliaryQubits := 0, gateCount := 15, depth := 13,
      oracleCalls := 0 }

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeVerified_cost :
  QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeRoute.cost =
    { auxiliaryQubits := 0,
      gateCount := 15, depth := 13,
      oracleCalls := 0 }

Theorem10.56.34

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sparse pruned better than dense 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/StatePreparationPaperRoutesCompact.lean:655. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.56.34●1 theorem

theoremdefined in QuantumBlockEncoding/StatePreparationPaperRoutesCompact.lean

complete

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparsePruned_betterThan_denseTree :
  QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedRoute.cost.betterThan
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeRoute.cost

theorem QuantumBlockEncoding.StatePreparationBenchmarks.sparsePruned_betterThan_denseTree :
  QuantumBlockEncoding.StatePreparationBenchmarks.sparsePrunedRoute.cost.betterThan
    QuantumBlockEncoding.StatePreparationBenchmarks.sparseDenseTreeRoute.cost