10.9. QuantumBlockEncoding/HermiteExplicitBond.lean🔗

11 explicit public declarations, in source order.

Definition10.9.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “scalar 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/HermiteExplicitBond.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.9.1●1 definition

defdefined in QuantumBlockEncoding/HermiteExplicitBond.lean

complete

def QuantumBlockEncoding.HermiteExplicitBond.scalarEquiv :
  Fin 2 ≃ QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond

def QuantumBlockEncoding.HermiteExplicitBond.scalarEquiv :
  Fin 2 ≃
    QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond

Definition10.9.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “bond equiv”. Layout: two left-tail states, middle boundary then '2*k+2' Bernstein states, and finally the right-tail 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. Layout: two left-tail states, middle boundary then '2*k+2' Bernstein states, and finally the right-tail state. All maps are executable.

Declaration kind. def.

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

Lean code for Definition10.9.2●1 definition

defdefined in QuantumBlockEncoding/HermiteExplicitBond.lean

complete

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

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

Layout: two left-tail states, middle boundary then `2*k+2` Bernstein
states, and finally the right-tail state. All maps are executable.

Definition10.9.3

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

Lean code for Definition10.9.3●1 definition

defdefined in QuantumBlockEncoding/HermiteExplicitBond.lean

complete

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

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

Definition10.9.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/HermiteExplicitBond.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.9.4●1 definition

defdefined in QuantumBlockEncoding/HermiteExplicitBond.lean

complete

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

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

Definition10.9.5

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/HermiteExplicitBond.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.9.5●1 definition

defdefined in QuantumBlockEncoding/HermiteExplicitBond.lean

complete

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

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

Theorem10.9.6

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

Lean code for Theorem10.9.6●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteExplicitBond.lean

complete

theorem QuantumBlockEncoding.HermiteExplicitBond.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.HermiteExplicitBond.kernel k n L)
      (QuantumBlockEncoding.HermiteExplicitBond.terminal k) start x a =
    QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel k n
        L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteTerminal k)
      (QuantumBlockEncoding.TensorTrainWord.toBits x)
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv k) a)

theorem QuantumBlockEncoding.HermiteExplicitBond.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.HermiteExplicitBond.kernel
        k n L)
      (QuantumBlockEncoding.HermiteExplicitBond.terminal
        k)
      start x a =
    QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel
        k n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteTerminal
        k)
      (QuantumBlockEncoding.TensorTrainWord.toBits
        x)
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv
          k)
        a)

Definition10.9.7

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.9.7●1 definition

defdefined in QuantumBlockEncoding/HermiteExplicitBond.lean

complete

def QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain (k n : ℕ)
  (L : ℝ) : QuantumBlockEncoding.TensorTrainCanonical.Chain (n + 1) 1 1

def QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.Chain
    (n + 1) 1 1

Theorem10.9.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “raw 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/HermiteExplicitBond.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.9.8●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteExplicitBond.lean

complete

theorem QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain_contract
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain k n L) x
      0 0 =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
      (n + 1) L
      ((QuantumBlockEncoding.TensorTrainWord.sampleEquiv (n + 1)) x)

theorem QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain_contract
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain
        k n L)
      x 0 0 =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
      k (n + 1) L
      ((QuantumBlockEncoding.TensorTrainWord.sampleEquiv
          (n + 1))
        x)

Theorem10.9.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “same literal source”; the hypotheses and conclusion in the code panel fix its exact scope. Equality of the observable source, not an unproved equality of layouts.

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. Equality of the observable source, not an unproved equality of layouts.

Declaration kind. theorem.

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

Lean code for Theorem10.9.9●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteExplicitBond.lean

complete

theorem QuantumBlockEncoding.HermiteExplicitBond.same_literal_source (k n : ℕ)
  (L : ℝ) (hL : 0 < L)
  (x : QuantumBlockEncoding.TensorTrainCanonical.Word (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain k n L) x
      0 0 =
    QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain k n L) x 0
      0

theorem QuantumBlockEncoding.HermiteExplicitBond.same_literal_source
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (x :
    QuantumBlockEncoding.TensorTrainCanonical.Word
      (n + 1)) :
  QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain
        k n L)
      x 0 0 =
    QuantumBlockEncoding.TensorTrainCanonical.contract
      (QuantumBlockEncoding.HermiteFiniteNorm.rawSourceChain
        k n L)
      x 0 0

Equality of the observable source, not an unproved equality of layouts.

Theorem10.9.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “raw 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/HermiteExplicitBond.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.9.10●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteExplicitBond.lean

complete

theorem QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain_maxBond
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain k n L) ≤
    2 * k + 6

theorem QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain_maxBond
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.TensorTrainCanonical.maxBond
      (QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain
        k n L) ≤
    2 * k + 6

Theorem10.9.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.9.11●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteExplicitBond.lean

complete

theorem QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain_norm (k n : ℕ)
  (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.norm
      (QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain k n L) =
    QuantumBlockEncoding.HermiteStatePreparation.sampleNorm k (n + 1) L

theorem QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain_norm
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.TensorTrainNormEnvironment.norm
      (QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain
        k n L) =
    QuantumBlockEncoding.HermiteStatePreparation.sampleNorm
      k (n + 1) L