10.10. QuantumBlockEncoding/HermiteFiniteChain.lean🔗

14 explicit public declarations, in source order.

Definition10.10.1

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.10.1●1 definition

defdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

def QuantumBlockEncoding.HermiteFiniteChain.bondEquiv (k : ℕ) :
  Fin (2 * k + 6) ≃
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k

def QuantumBlockEncoding.HermiteFiniteChain.bondEquiv
  (k : ℕ) :
  Fin (2 * k + 6) ≃
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k

Definition10.10.2

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.10.2●1 definition

defdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

def QuantumBlockEncoding.HermiteFiniteChain.kernel (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.MatrixProductChain.Kernel (2 * k + 6)

def QuantumBlockEncoding.HermiteFiniteChain.kernel
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.MatrixProductChain.Kernel
    (2 * k + 6)

Definition10.10.3

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.10.3●1 definition

defdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

def QuantumBlockEncoding.HermiteFiniteChain.terminal (k : ℕ) :
  Fin (2 * k + 6) → ℝ

def QuantumBlockEncoding.HermiteFiniteChain.terminal
  (k : ℕ) : Fin (2 * k + 6) → ℝ

Definition10.10.4

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.10.4●1 definition

defdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

def QuantumBlockEncoding.HermiteFiniteChain.initial (k n : ℕ) (L : ℝ) :
  Fin (2 * k + 6) → ℝ

def QuantumBlockEncoding.HermiteFiniteChain.initial
  (k n : ℕ) (L : ℝ) : Fin (2 * k + 6) → ℝ

Theorem10.10.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.10.5●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteChain.kernel_readout (k n : ℕ) (L : ℝ)
  (m start : ℕ) (h : start + m = n + 1)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word m)
  (a : Fin (2 * k + 6)) :
  QuantumBlockEncoding.MatrixProductChain.readout
      (QuantumBlockEncoding.HermiteFiniteChain.kernel k n L)
      (QuantumBlockEncoding.HermiteFiniteChain.terminal k) start x a =
    QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel k n
        L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteTerminal k)
      (QuantumBlockEncoding.TensorTrainWord.toBits x)
      ((QuantumBlockEncoding.HermiteFiniteChain.bondEquiv k) a)

theorem QuantumBlockEncoding.HermiteFiniteChain.kernel_readout
  (k n : ℕ) (L : ℝ) (m start : ℕ)
  (h : start + m = n + 1)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      m)
  (a : Fin (2 * k + 6)) :
  QuantumBlockEncoding.MatrixProductChain.readout
      (QuantumBlockEncoding.HermiteFiniteChain.kernel
        k n L)
      (QuantumBlockEncoding.HermiteFiniteChain.terminal
        k)
      start x a =
    QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel
        k n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteTerminal
        k)
      (QuantumBlockEncoding.TensorTrainWord.toBits
        x)
      ((QuantumBlockEncoding.HermiteFiniteChain.bondEquiv
          k)
        a)

Definition10.10.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “source chain”. Actual local cores, with normalization absorbed into the initial row.

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. Actual local cores, with normalization absorbed into the initial row.

Declaration kind. def.

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

Lean code for Definition10.10.6●1 definition

defdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

def QuantumBlockEncoding.HermiteFiniteChain.sourceChain (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1

def QuantumBlockEncoding.HermiteFiniteChain.sourceChain
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
    (n + 1) 1 1

Actual local cores, with normalization absorbed into the initial row.

Theorem10.10.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.10.7●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteChain.sourceChain_contract (k n : ℕ)
  (L : ℝ) (hL : 0 < L)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.HermiteFiniteChain.sourceChain k n L) x 0
      0 =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
        (n + 1) L
        ((QuantumBlockEncoding.TensorTrainWord.sampleEquiv (n + 1)) x) /
      QuantumBlockEncoding.HermiteStatePreparation.sampleNorm k (n + 1)
        L

theorem QuantumBlockEncoding.HermiteFiniteChain.sourceChain_contract
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.HermiteFiniteChain.sourceChain
        k n L)
      x 0 0 =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
        k (n + 1) L
        ((QuantumBlockEncoding.TensorTrainWord.sampleEquiv
            (n + 1))
          x) /
      QuantumBlockEncoding.HermiteStatePreparation.sampleNorm
        k (n + 1) L

Theorem10.10.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.10.8●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteChain.sourceChain_maxBond (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.HermiteFiniteChain.sourceChain k n L) ≤
    2 * k + 6

theorem QuantumBlockEncoding.HermiteFiniteChain.sourceChain_maxBond
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.HermiteFiniteChain.sourceChain
        k n L) ≤
    2 * k + 6

Theorem10.10.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.10.9●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteChain.sourceChain_storage (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.MatrixProductChain.storedScalars
      (QuantumBlockEncoding.HermiteFiniteChain.sourceChain k n L) ≤
    2 * (n + 1) * (2 * k + 6) ^ 2

theorem QuantumBlockEncoding.HermiteFiniteChain.sourceChain_storage
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.MatrixProductChain.storedScalars
      (QuantumBlockEncoding.HermiteFiniteChain.sourceChain
        k n L) ≤
    2 * (n + 1) * (2 * k + 6) ^ 2

Theorem10.10.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.10.10●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteChain.sourceChain_normalized (k n : ℕ)
  (L : ℝ) (hL : 0 < L) :
  ∑ x,
      QuantumBlockEncoding.TensorTrainCanonical.contract
          (QuantumBlockEncoding.HermiteFiniteChain.sourceChain k n L) x
          0 0 ^
        2 =
    1

theorem QuantumBlockEncoding.HermiteFiniteChain.sourceChain_normalized
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  ∑ x,
      QuantumBlockEncoding.TensorTrainCanonical.contract
          (QuantumBlockEncoding.HermiteFiniteChain.sourceChain
            k n L)
          x 0 0 ^
        2 =
    1

Definition10.10.11

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “bond qubits”. Actual binary bond register; its size depends on smoothing order, not the number of data qubits.

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. Actual binary bond register; its size depends on smoothing order, not the number of data qubits.

Declaration kind. def.

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

Lean code for Definition10.10.11●1 definition

defdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

def QuantumBlockEncoding.HermiteFiniteChain.bondQubits (k : ℕ) : ℕ

def QuantumBlockEncoding.HermiteFiniteChain.bondQubits
  (k : ℕ) : ℕ

Actual binary bond register; its size depends on smoothing order, not
the number of data qubits.

Theorem10.10.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.10.12●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteChain.bond_fits (k : ℕ) :
  2 * k + 6 ≤ 2 ^ QuantumBlockEncoding.HermiteFiniteChain.bondQubits k

theorem QuantumBlockEncoding.HermiteFiniteChain.bond_fits
  (k : ℕ) :
  2 * k + 6 ≤
    2 ^
      QuantumBlockEncoding.HermiteFiniteChain.bondQubits
        k

Theorem10.10.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “padded bond le twice”; 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/HermiteFiniteChain.lean:85. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.10.13●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteChain.padded_bond_le_twice (k : ℕ) :
  2 ^ QuantumBlockEncoding.HermiteFiniteChain.bondQubits k ≤
    2 * (2 * k + 6)

theorem QuantumBlockEncoding.HermiteFiniteChain.padded_bond_le_twice
  (k : ℕ) :
  2 ^
      QuantumBlockEncoding.HermiteFiniteChain.bondQubits
        k ≤
    2 * (2 * k + 6)

Theorem10.10.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cubic stage budget”; the hypotheses and conclusion in the code panel fix its exact scope. Algebraic substitution used after the actual stage compiler is supplied.

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. Algebraic substitution used after the actual stage compiler is supplied. This is not itself an existence theorem for the final circuit.

Declaration kind. theorem.

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

Lean code for Theorem10.10.14●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteFiniteChain.lean

complete

theorem QuantumBlockEncoding.HermiteFiniteChain.cubic_stage_budget (k n : ℕ) :
  6 * (n + 1) *
      (2 ^ QuantumBlockEncoding.HermiteFiniteChain.bondQubits k) ^ 3 ≤
    48 * (n + 1) * (2 * k + 6) ^ 3

theorem QuantumBlockEncoding.HermiteFiniteChain.cubic_stage_budget
  (k n : ℕ) :
  6 * (n + 1) *
      (2 ^
          QuantumBlockEncoding.HermiteFiniteChain.bondQubits
            k) ^
        3 ≤
    48 * (n + 1) * (2 * k + 6) ^ 3

Algebraic substitution used after the actual stage compiler is supplied.
This is not itself an existence theorem for the final circuit.