10.18. QuantumBlockEncoding/HermiteStatePreparation.lean🔗

19 explicit public declarations, in source order.

Definition10.18.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “grid point”. Left-inclusive, right-exclusive grid on '[-πL,πL)' when 'L>0'.

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. Left-inclusive, right-exclusive grid on '[-πL,πL)' when 'L>0'.

Declaration kind. def.

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

Lean code for Definition10.18.1●1 definition

defdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

def QuantumBlockEncoding.HermiteStatePreparation.gridPoint (n : ℕ) (L : ℝ)
  (j : Fin (QuantumBlockEncoding.gridSize n)) : ℝ

def QuantumBlockEncoding.HermiteStatePreparation.gridPoint
  (n : ℕ) (L : ℝ)
  (j :
    Fin
      (QuantumBlockEncoding.gridSize n)) :
  ℝ

Left-inclusive, right-exclusive grid on `[-πL,πL)` when `L>0`.

Definition10.18.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sampled amplitude”. The physical sample, without changing the polynomial on the splice interval.

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 physical sample, without changing the polynomial on the splice interval.

Declaration kind. def.

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

Lean code for Definition10.18.2●1 definition

defdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

def QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude (k n : ℕ)
  (L : ℝ) (j : Fin (QuantumBlockEncoding.gridSize n)) : ℝ

def QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
  (k n : ℕ) (L : ℝ)
  (j :
    Fin
      (QuantumBlockEncoding.gridSize n)) :
  ℝ

The physical sample, without changing the polynomial on the splice interval.

Theorem10.18.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sampled amplitude pos”; 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/HermiteStatePreparation.lean:30. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.18.3●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude_pos
  (k n : ℕ) (L : ℝ) (j : Fin (QuantumBlockEncoding.gridSize n)) :
  0 <
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k n L
      j

theorem QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude_pos
  (k n : ℕ) (L : ℝ)
  (j :
    Fin
      (QuantumBlockEncoding.gridSize n)) :
  0 <
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
      k n L j

Definition10.18.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sample norm”. The true Euclidean normalizer of the complete finite sample table.

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 true Euclidean normalizer of the complete finite sample table.

Declaration kind. def.

Source: QuantumBlockEncoding/HermiteStatePreparation.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.18.4●1 definition

defdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

def QuantumBlockEncoding.HermiteStatePreparation.sampleNorm (k n : ℕ)
  (L : ℝ) : ℝ

def QuantumBlockEncoding.HermiteStatePreparation.sampleNorm
  (k n : ℕ) (L : ℝ) : ℝ

The true Euclidean normalizer of the complete finite sample table.

Theorem10.18.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sample norm pos”; 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/HermiteStatePreparation.lean:37. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.18.5●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.sampleNorm_pos (k n : ℕ)
  (L : ℝ) :
  0 < QuantumBlockEncoding.HermiteStatePreparation.sampleNorm k n L

theorem QuantumBlockEncoding.HermiteStatePreparation.sampleNorm_pos
  (k n : ℕ) (L : ℝ) :
  0 <
    QuantumBlockEncoding.HermiteStatePreparation.sampleNorm
      k n L

Definition10.18.6

uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. def.

Source: QuantumBlockEncoding/HermiteStatePreparation.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.18.6●1 definition

defdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

def QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
  (k n : ℕ) (L : ℝ) (j : Fin (QuantumBlockEncoding.gridSize n)) : ℂ

def QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
  (k n : ℕ) (L : ℝ)
  (j :
    Fin
      (QuantumBlockEncoding.gridSize n)) :
  ℂ

Definition10.18.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “hermite circuit”. An actual list of primitive instructions on precisely 'n' 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. An actual list of primitive instructions on precisely 'n' wires.

Declaration kind. def.

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

Lean code for Definition10.18.7●1 definition

defdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

def QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit (k n : ℕ)
  (L : ℝ) : QuantumBlockEncoding.PrimitiveCircuit n

def QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.PrimitiveCircuit n

An actual list of primitive instructions on precisely `n` wires.

Definition10.18.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “hermite unitary”. The exact primitive denotation, reindexed by little-endian integers.

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 exact primitive denotation, reindexed by little-endian integers.

Declaration kind. def.

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

Lean code for Definition10.18.8●1 definition

defdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

def QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary (k n : ℕ)
  (L : ℝ) :
  Matrix (Fin (QuantumBlockEncoding.gridSize n))
    (Fin (QuantumBlockEncoding.gridSize n)) ℂ

def QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary
  (k n : ℕ) (L : ℝ) :
  Matrix
    (Fin
      (QuantumBlockEncoding.gridSize n))
    (Fin
      (QuantumBlockEncoding.gridSize n))
    ℂ

The exact primitive denotation, reindexed by little-endian integers.

Theorem10.18.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.18.9●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary_eq_circuit
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary k n L =
    (Matrix.reindexAlgEquiv ℂ ℂ
        (QuantumBlockEncoding.primitiveBasisLEEquiv n))
      (QuantumBlockEncoding.evalPrimitiveCircuit
        (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit k n
          L))

theorem QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary_eq_circuit
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary
      k n L =
    (Matrix.reindexAlgEquiv ℂ ℂ
        (QuantumBlockEncoding.primitiveBasisLEEquiv
          n))
      (QuantumBlockEncoding.evalPrimitiveCircuit
        (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit
          k n L))

Theorem10.18.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.18.10●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary_unitary
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary k n L ∈
    Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize n)) ℂ

theorem QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary_unitary
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary
      k n L ∈
    Matrix.unitaryGroup
      (Fin
        (QuantumBlockEncoding.gridSize n))
      ℂ

Theorem10.18.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite first column”; 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/HermiteStatePreparation.lean:65. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.18.11●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_firstColumn
  (k n : ℕ) (L : ℝ) (j : Fin (QuantumBlockEncoding.gridSize n)) :
  QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary k n L j
      (QuantumBlockEncoding.zeroBasisIndex n) =
    QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude k n
      L j

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_firstColumn
  (k n : ℕ) (L : ℝ)
  (j :
    Fin
      (QuantumBlockEncoding.gridSize n)) :
  QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary
      k n L j
      (QuantumBlockEncoding.zeroBasisIndex
        n) =
    QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
      k n L j

Theorem10.18.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite normalized”; the hypotheses and conclusion in the code panel fix its exact scope. Every squared norm is included, including both exponential tails and the splice.

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. Every squared norm is included, including both exponential tails and the splice.

Declaration kind. theorem.

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

Lean code for Theorem10.18.12●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_normalized
  (k n : ℕ) (L : ℝ) :
  ∑ j,
      Complex.normSq
        (QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
          k n L j) =
    1

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_normalized
  (k n : ℕ) (L : ℝ) :
  ∑ j,
      Complex.normSq
        (QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
          k n L j) =
    1

Every squared norm is included, including both exponential tails and the splice.

Theorem10.18.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite state action”; 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/HermiteStatePreparation.lean:75. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.18.13●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_stateAction
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary k n
        L)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet n) =
    QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude k n
      L

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_stateAction
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.ConcreteSemantics.applyVec
      (QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary
        k n L)
      (QuantumBlockEncoding.ConcreteSemantics.zeroKet
        n) =
    QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
      k n L

Theorem10.18.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.18.14●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_ryCount (k n : ℕ)
  (L : ℝ) :
  (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit k n
        L).ryCount =
    2 ^ n - 1

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_ryCount
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit
        k n L).ryCount =
    2 ^ n - 1

Theorem10.18.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite cx count”; 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/HermiteStatePreparation.lean:84. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.18.15●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_cxCount (k n : ℕ)
  (L : ℝ) :
  (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit k n
        L).cxCount =
    2 * (2 ^ n - 1 - n)

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_cxCount
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit
        k n L).cxCount =
    2 * (2 ^ n - 1 - n)

Theorem10.18.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite oracle calls”; 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/HermiteStatePreparation.lean:87. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.18.16●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_oracleCalls
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit k n
          L).resource.oracleCalls =
    0

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_oracleCalls
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit
          k n L).resource.oracleCalls =
    0

Theorem10.18.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite no ancilla”; the hypotheses and conclusion in the code panel fix its exact scope. The circuit has exactly the data register and no allocated ancillary wire.

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 circuit has exactly the data register and no allocated ancillary wire.

Declaration kind. theorem.

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

Lean code for Theorem10.18.17●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_noAncilla (k n : ℕ)
  (L : ℝ) :
  (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit k n
          L).resource.pureAncilla =
    0

theorem QuantumBlockEncoding.HermiteStatePreparation.hermite_noAncilla
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit
          k n L).resource.pureAncilla =
    0

The circuit has exactly the data register and no allocated ancillary wire.

Theorem10.18.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite state preparation complete”; the hypotheses and conclusion in the code panel fix its exact scope. The closed symbolic root: normalization, genuine unitarity, primitive state action and exact reference compiler resources are proved together.

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 closed symbolic root: normalization, genuine unitarity, primitive state action and exact reference compiler resources are proved together.

Declaration kind. theorem.

Source: QuantumBlockEncoding/HermiteStatePreparation.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.18.18●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

theorem QuantumBlockEncoding.HermiteStatePreparation.hermiteStatePreparation_complete
  (k n : ℕ) (L : ℝ) :
  0 < QuantumBlockEncoding.HermiteStatePreparation.sampleNorm k n L ∧
    ∑ j,
          Complex.normSq
            (QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
              k n L j) =
        1 ∧
      QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary k n
            L ∈
          Matrix.unitaryGroup (Fin (QuantumBlockEncoding.gridSize n))
            ℂ ∧
        QuantumBlockEncoding.ConcreteSemantics.applyVec
              (QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary
                k n L)
              (QuantumBlockEncoding.ConcreteSemantics.zeroKet n) =
            QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
              k n L ∧
          (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit k
                  n L).ryCount =
              2 ^ n - 1 ∧
            (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit
                    k n L).cxCount =
                2 * (2 ^ n - 1 - n) ∧
              (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit
                      k n L).resource.oracleCalls =
                0

theorem QuantumBlockEncoding.HermiteStatePreparation.hermiteStatePreparation_complete
  (k n : ℕ) (L : ℝ) :
  0 <
      QuantumBlockEncoding.HermiteStatePreparation.sampleNorm
        k n L ∧
    ∑ j,
          Complex.normSq
            (QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
              k n L j) =
        1 ∧
      QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary
            k n L ∈
          Matrix.unitaryGroup
            (Fin
              (QuantumBlockEncoding.gridSize
                n))
            ℂ ∧
        QuantumBlockEncoding.ConcreteSemantics.applyVec
              (QuantumBlockEncoding.HermiteStatePreparation.hermiteUnitary
                k n L)
              (QuantumBlockEncoding.ConcreteSemantics.zeroKet
                n) =
            QuantumBlockEncoding.HermiteStatePreparation.normalizedAmplitude
              k n L ∧
          (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit
                  k n L).ryCount =
              2 ^ n - 1 ∧
            (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit
                    k n L).cxCount =
                2 * (2 ^ n - 1 - n) ∧
              (QuantumBlockEncoding.HermiteStatePreparation.hermiteCircuit
                      k n
                      L).resource.oracleCalls =
                0

The closed symbolic root: normalization, genuine unitarity, primitive
state action and exact reference compiler resources are proved together.

Definition10.18.19

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “hermite certificate”. Integration into the existing concrete state-preparation certificate API.

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. Integration into the existing concrete state-preparation certificate API.

Declaration kind. def.

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

Lean code for Definition10.18.19●1 definition

defdefined in QuantumBlockEncoding/HermiteStatePreparation.lean

complete

def QuantumBlockEncoding.HermiteStatePreparation.hermiteCertificate
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
    n

def QuantumBlockEncoding.HermiteStatePreparation.hermiteCertificate
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.ConcreteSemantics.ComplexStatePreparationCertificate
    n

Integration into the existing concrete state-preparation certificate API.