10.7. QuantumBlockEncoding/HermiteBoundaryInjection.lean🔗

121 explicit public declarations, in source order.

Definition10.7.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “word value”. The first list entry is the most significant digit.

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 first list entry is the most significant digit.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.wordValue : List Bool → ℕ

def QuantumBlockEncoding.HermiteBoundaryInjection.wordValue :
  List Bool → ℕ

The first list entry is the most significant digit.

Theorem10.7.2

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.2●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.wordValue_lt
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits <
    2 ^ bits.length

theorem QuantumBlockEncoding.HermiteBoundaryInjection.wordValue_lt
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
      bits <
    2 ^ bits.length

Theorem10.7.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “path coordinate eq word value”; the hypotheses and conclusion in the code panel fix its exact scope. Reconciles the polynomial's real path coordinate with integer bit order.

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. Reconciles the polynomial's real path coordinate with integer bit order.

Declaration kind. theorem.

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

Lean code for Theorem10.7.3●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.pathCoordinate_eq_wordValue
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBernstein.pathCoordinate bits 0 =
    ↑(QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits) /
      2 ^ bits.length

theorem QuantumBlockEncoding.HermiteBoundaryInjection.pathCoordinate_eq_wordValue
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBernstein.pathCoordinate
      bits 0 =
    ↑(QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
          bits) /
      2 ^ bits.length

Reconciles the polynomial's real path coordinate with integer bit order.

Definition10.7.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “full”. A dyadic node lies entirely in the half-open target 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. A dyadic node lies entirely in the half-open target interval.

Declaration kind. def.

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

Lean code for Definition10.7.4●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.Full
  (lower upper first size : ℕ) : Prop

def QuantumBlockEncoding.HermiteBoundaryInjection.Full
  (lower upper first size : ℕ) : Prop

A dyadic node lies entirely in the half-open target interval.

Definition10.7.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “outside”. A dyadic node is disjoint from the half-open target 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. A dyadic node is disjoint from the half-open target interval.

Declaration kind. def.

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

Lean code for Definition10.7.5●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.Outside
  (lower upper first size : ℕ) : Prop

def QuantumBlockEncoding.HermiteBoundaryInjection.Outside
  (lower upper first size : ℕ) : Prop

A dyadic node is disjoint from the half-open target interval.

Definition10.7.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “partial”. A genuinely unresolved interval, not a wholly included or outside node.

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. A genuinely unresolved interval, not a wholly included or outside node.

Declaration kind. def.

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

Lean code for Definition10.7.6●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.Partial
  (lower upper first size : ℕ) : Prop

def QuantumBlockEncoding.HermiteBoundaryInjection.Partial
  (lower upper first size : ℕ) : Prop

A genuinely unresolved interval, not a wholly included or outside node.

Theorem10.7.7

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “partial prefix eq”; the hypotheses and conclusion in the code panel fix its exact scope. At an upper-aligned cut there is only one possible unresolved prefix.

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. At an upper-aligned cut there is only one possible unresolved prefix. The quotient is computed directly; no list of prefixes is constructed.

Declaration kind. theorem.

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

Lean code for Theorem10.7.7●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.partial_prefix_eq
  (lower M B x : ℕ) (hM : 0 < M)
  (hp :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial lower (M * B)
      (M * x) M) :
  x = lower / M

theorem QuantumBlockEncoding.HermiteBoundaryInjection.partial_prefix_eq
  (lower M B x : ℕ) (hM : 0 < M)
  (hp :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial
      lower (M * B) (M * x) M) :
  x = lower / M

At an upper-aligned cut there is only one possible unresolved prefix.
The quotient is computed directly; no list of prefixes is constructed.

Theorem10.7.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.8●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.partial_prefix_unique
  (lower M B x y : ℕ) (hM : 0 < M)
  (hx :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial lower (M * B)
      (M * x) M)
  (hy :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial lower (M * B)
      (M * y) M) :
  x = y

theorem QuantumBlockEncoding.HermiteBoundaryInjection.partial_prefix_unique
  (lower M B x y : ℕ) (hM : 0 < M)
  (hx :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial
      lower (M * B) (M * x) M)
  (hy :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial
      lower (M * B) (M * y) M) :
  x = y

Theorem10.7.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “not partial unit”; the hypotheses and conclusion in the code panel fix its exact scope. The integer endpoint prevents an unresolved state at the last bit.

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 integer endpoint prevents an unresolved state at the last bit.

Declaration kind. theorem.

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

Lean code for Theorem10.7.9●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.not_partial_unit
  (lower upper first : ℕ) :
  ¬QuantumBlockEncoding.HermiteBoundaryInjection.Partial lower upper
      first 1

theorem QuantumBlockEncoding.HermiteBoundaryInjection.not_partial_unit
  (lower upper first : ℕ) :
  ¬QuantumBlockEncoding.HermiteBoundaryInjection.Partial
      lower upper first 1

The integer endpoint prevents an unresolved state at the last bit.

Theorem10.7.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “partial middle prefix unique”; the hypotheses and conclusion in the code panel fix its exact scope. Every cut after the first consumed bit in an 'n+1'-bit middle interval has an upper endpoint aligned with the remaining dyadic block size.

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 cut after the first consumed bit in an 'n+1'-bit middle interval has an upper endpoint aligned with the remaining dyadic block size.

Declaration kind. theorem.

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

Lean code for Theorem10.7.10●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.partial_middle_prefix_unique
  (lower pWidth sWidth x y : ℕ)
  (hx :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial lower
      (2 ^ (pWidth + sWidth)) (2 ^ sWidth * x) (2 ^ sWidth))
  (hy :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial lower
      (2 ^ (pWidth + sWidth)) (2 ^ sWidth * y) (2 ^ sWidth)) :
  x = y

theorem QuantumBlockEncoding.HermiteBoundaryInjection.partial_middle_prefix_unique
  (lower pWidth sWidth x y : ℕ)
  (hx :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial
      lower (2 ^ (pWidth + sWidth))
      (2 ^ sWidth * x) (2 ^ sWidth))
  (hy :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial
      lower (2 ^ (pWidth + sWidth))
      (2 ^ sWidth * y) (2 ^ sWidth)) :
  x = y

Every cut after the first consumed bit in an `n+1`-bit middle interval
has an upper endpoint aligned with the remaining dyadic block size.

Theorem10.7.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “middle root not full”; the hypotheses and conclusion in the code panel fix its exact scope. The initial whole-grid node cannot inject directly: its upper child is outside the middle component.

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 initial whole-grid node cannot inject directly: its upper child is outside the middle component. Thus nonempty traversal begins with a digit.

Declaration kind. theorem.

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

Lean code for Theorem10.7.11●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middle_root_not_full
  (lower n : ℕ) :
  ¬QuantumBlockEncoding.HermiteBoundaryInjection.Full lower (2 ^ n) 0
      (2 ^ (n + 1))

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middle_root_not_full
  (lower n : ℕ) :
  ¬QuantumBlockEncoding.HermiteBoundaryInjection.Full
      lower (2 ^ n) 0 (2 ^ (n + 1))

The initial whole-grid node cannot inject directly: its upper child is
outside the middle component. Thus nonempty traversal begins with a digit.

Definition10.7.12

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “affine point”. Affine source coordinate, also meaningful at a block's excluded endpoint.

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. Affine source coordinate, also meaningful at a block's excluded endpoint.

Declaration kind. def.

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

Lean code for Definition10.7.12●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
  (origin step : ℝ) (j : ℕ) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
  (origin step : ℝ) (j : ℕ) : ℝ

Affine source coordinate, also meaningful at a block's excluded endpoint.

Definition10.7.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “injected readout”. Literal restricted Bernstein row readout for a fully included dyadic node.

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. Literal restricted Bernstein row readout for a fully included dyadic node.

Declaration kind. def.

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

Lean code for Definition10.7.13●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.injectedReadout (k : ℕ)
  (origin step : ℝ) (first : ℕ) (bits : List Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.injectedReadout
  (k : ℕ) (origin step : ℝ) (first : ℕ)
  (bits : List Bool) : ℝ

Literal restricted Bernstein row readout for a fully included dyadic node.

Theorem10.7.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.14●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectedReadout_eq (k : ℕ)
  (origin step : ℝ) (first : ℕ) (bits : List Bool)
  (hfirst :
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        step first ≠
      0) :
  QuantumBlockEncoding.HermiteBoundaryInjection.injectedReadout k origin
      step first bits =
    Polynomial.eval
      (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        step
        (first +
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits))
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectedReadout_eq
  (k : ℕ) (origin step : ℝ) (first : ℕ)
  (bits : List Bool)
  (hfirst :
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin step first ≠
      0) :
  QuantumBlockEncoding.HermiteBoundaryInjection.injectedReadout
      k origin step first bits =
    Polynomial.eval
      (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin step
        (first +
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits))
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)

Definition10.7.15

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “unit coefficient”. A finite coefficient basis vector, extended by zero to the existing Bernstein coefficient 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. A finite coefficient basis vector, extended by zero to the existing Bernstein coefficient API.

Declaration kind. def.

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

Lean code for Definition10.7.15●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.unitCoefficient (d : ℕ)
  (i : Fin (d + 1)) : ℕ → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.unitCoefficient
  (d : ℕ) (i : Fin (d + 1)) : ℕ → ℝ

A finite coefficient basis vector, extended by zero to the existing
Bernstein coefficient API.

Definition10.7.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “shared core”. The actual finite row-update matrix: input coefficient 'i', output 'j'.

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 actual finite row-update matrix: input coefficient 'i', output 'j'. It is the transpose of the usual coefficient-column subdivision matrix.

Declaration kind. def.

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

Lean code for Definition10.7.16●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore (d : ℕ)
  (bit : Bool) : Matrix (Fin (d + 1)) (Fin (d + 1)) ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore
  (d : ℕ) (bit : Bool) :
  Matrix (Fin (d + 1)) (Fin (d + 1)) ℝ

The actual finite row-update matrix: input coefficient `i`, output `j`.
It is the transpose of the usual coefficient-column subdivision matrix.

Theorem10.7.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “shared core false”; the hypotheses and conclusion in the code panel fix its exact scope. The prototype's lower triangular subdivision, transposed for row updates.

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 prototype's lower triangular subdivision, transposed for row updates.

Declaration kind. theorem.

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

Lean code for Theorem10.7.17●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore_false (d : ℕ)
  (i j : Fin (d + 1)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore d false i j =
    if ↑i ≤ ↑j then ↑((↑j).choose ↑i) / 2 ^ ↑j else 0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore_false
  (d : ℕ) (i j : Fin (d + 1)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore
      d false i j =
    if ↑i ≤ ↑j then
      ↑((↑j).choose ↑i) / 2 ^ ↑j
    else 0

The prototype's lower triangular subdivision, transposed for row updates.

Theorem10.7.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “shared core true”; the hypotheses and conclusion in the code panel fix its exact scope. The prototype's upper triangular subdivision, in the same row orientation.

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 prototype's upper triangular subdivision, in the same row orientation.

Declaration kind. theorem.

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

Lean code for Theorem10.7.18●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore_true (d : ℕ)
  (i j : Fin (d + 1)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore d true i j =
    if ↑j ≤ ↑i then ↑((d - ↑j).choose (↑i - ↑j)) / 2 ^ (d - ↑j) else 0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore_true
  (d : ℕ) (i j : Fin (d + 1)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore
      d true i j =
    if ↑j ≤ ↑i then
      ↑((d - ↑j).choose (↑i - ↑j)) /
        2 ^ (d - ↑j)
    else 0

The prototype's upper triangular subdivision, in the same row orientation.

Theorem10.7.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “shared core basis”; the hypotheses and conclusion in the code panel fix its exact scope. One finite core has the Bernstein basis pullback dictated by its bit.

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. One finite core has the Bernstein basis pullback dictated by its bit.

Declaration kind. theorem.

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

Lean code for Theorem10.7.19●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore_basis (d : ℕ)
  (bit : Bool) (i : Fin (d + 1)) (t : ℝ) :
  ∑ j,
      QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore d bit i
          j *
        QuantumBlockEncoding.HermiteBernstein.basis d (↑j) t =
    QuantumBlockEncoding.HermiteBernstein.basis d (↑i)
      (QuantumBlockEncoding.HermiteBernstein.childCoordinate bit t)

theorem QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore_basis
  (d : ℕ) (bit : Bool) (i : Fin (d + 1))
  (t : ℝ) :
  ∑ j,
      QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore
          d bit i j *
        QuantumBlockEncoding.HermiteBernstein.basis
          d (↑j) t =
    QuantumBlockEncoding.HermiteBernstein.basis
      d (↑i)
      (QuantumBlockEncoding.HermiteBernstein.childCoordinate
        bit t)

One finite core has the Bernstein basis pullback dictated by its bit.

Definition10.7.20

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “shared contract”. Backward finite-matrix contraction with the terminal coefficient-zero selector.

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. Backward finite-matrix contraction with the terminal coefficient-zero selector. Every summation has 'd+1' entries, independent of the grid width.

Declaration kind. def.

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

Lean code for Definition10.7.20●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.sharedContract (d : ℕ) :
  List Bool → Fin (d + 1) → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.sharedContract
  (d : ℕ) : List Bool → Fin (d + 1) → ℝ

Backward finite-matrix contraction with the terminal coefficient-zero
selector. Every summation has `d+1` entries, independent of the grid width.

Theorem10.7.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “shared contract eq basis”; the hypotheses and conclusion in the code panel fix its exact scope. All finite shared-core products, with arbitrary MSB-first suffix length.

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. All finite shared-core products, with arbitrary MSB-first suffix length.

Declaration kind. theorem.

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

Lean code for Theorem10.7.21●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.sharedContract_eq_basis
  (d : ℕ) (bits : List Bool) (i : Fin (d + 1)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.sharedContract d bits
      i =
    QuantumBlockEncoding.HermiteBernstein.basis d (↑i)
      (QuantumBlockEncoding.HermiteBernstein.pathCoordinate bits 0)

theorem QuantumBlockEncoding.HermiteBoundaryInjection.sharedContract_eq_basis
  (d : ℕ) (bits : List Bool)
  (i : Fin (d + 1)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.sharedContract
      d bits i =
    QuantumBlockEncoding.HermiteBernstein.basis
      d (↑i)
      (QuantumBlockEncoding.HermiteBernstein.pathCoordinate
        bits 0)

All finite shared-core products, with arbitrary MSB-first suffix length.

Definition10.7.22

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “injected finite readout”. The restricted coefficient row contracted with the finite core matrices.

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 restricted coefficient row contracted with the finite core matrices.

Declaration kind. def.

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

Lean code for Definition10.7.22●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.injectedFiniteReadout
  (k : ℕ) (origin step : ℝ) (first : ℕ) (bits : List Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.injectedFiniteReadout
  (k : ℕ) (origin step : ℝ) (first : ℕ)
  (bits : List Bool) : ℝ

The restricted coefficient row contracted with the finite core matrices.

Theorem10.7.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “injected finite readout eq injected readout”; the hypotheses and conclusion in the code panel fix its exact scope. Matrix-level finite restriction/suffix adapter, not an assumed contract.

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. Matrix-level finite restriction/suffix adapter, not an assumed contract.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectedFiniteReadout_eq_injectedReadout
  (k : ℕ) (origin step : ℝ) (first : ℕ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.injectedFiniteReadout k
      origin step first bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.injectedReadout k
      origin step first bits

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectedFiniteReadout_eq_injectedReadout
  (k : ℕ) (origin step : ℝ) (first : ℕ)
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.injectedFiniteReadout
      k origin step first bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.injectedReadout
      k origin step first bits

Matrix-level finite restriction/suffix adapter, not an assumed contract.

Theorem10.7.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.24●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectedFiniteReadout_eq
  (k : ℕ) (origin step : ℝ) (first : ℕ) (bits : List Bool)
  (hfirst :
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        step first ≠
      0) :
  QuantumBlockEncoding.HermiteBoundaryInjection.injectedFiniteReadout k
      origin step first bits =
    Polynomial.eval
      (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        step
        (first +
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits))
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectedFiniteReadout_eq
  (k : ℕ) (origin step : ℝ) (first : ℕ)
  (bits : List Bool)
  (hfirst :
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin step first ≠
      0) :
  QuantumBlockEncoding.HermiteBoundaryInjection.injectedFiniteReadout
      k origin step first bits =
    Polynomial.eval
      (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin step
        (first +
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits))
      (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
        k)

Definition10.7.25

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “boundary readout”. Follow one query path.

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. Follow one query path. Once injected, remaining digits update only the shared polynomial row. Before injection, only the boundary branch continues.

Declaration kind. def.

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

Lean code for Definition10.7.25●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.boundaryReadout (k : ℕ)
  (origin step : ℝ) (lower upper first : ℕ) (bits : List Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.boundaryReadout
  (k : ℕ) (origin step : ℝ)
  (lower upper first : ℕ)
  (bits : List Bool) : ℝ

Follow one query path. Once injected, remaining digits update only the
shared polynomial row. Before injection, only the boundary branch continues.

Theorem10.7.26

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “boundary readout eq”; the hypotheses and conclusion in the code panel fix its exact scope. Exact traversal semantics.

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. Exact traversal semantics. The sole coordinate hypothesis is a restriction domain condition, not an assumed equality between the source and the cores.

Declaration kind. theorem.

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

Lean code for Theorem10.7.26●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.boundaryReadout_eq (k : ℕ)
  (origin step : ℝ) (lower upper : ℕ)
  (hvalid :
    ∀ (j : ℕ),
      lower ≤ j →
        j < upper →
          QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
              origin step j ≠
            0)
  (first : ℕ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.boundaryReadout k origin
      step lower upper first bits =
    if
        lower ≤
            first +
              QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits ∧
          first +
              QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits <
            upper then
      Polynomial.eval
        (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
          origin step
          (first +
            QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits))
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)
    else 0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.boundaryReadout_eq
  (k : ℕ) (origin step : ℝ)
  (lower upper : ℕ)
  (hvalid :
    ∀ (j : ℕ),
      lower ≤ j →
        j < upper →
          QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
              origin step j ≠
            0)
  (first : ℕ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.boundaryReadout
      k origin step lower upper first
      bits =
    if
        lower ≤
            first +
              QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits ∧
          first +
              QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits <
            upper then
      Polynomial.eval
        (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
          origin step
          (first +
            QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits))
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
          k)
    else 0

Exact traversal semantics. The sole coordinate hypothesis is a restriction
domain condition, not an assumed equality between the source and the cores.

Definition10.7.27

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “injection bond”. One unresolved boundary scalar and one shared degree-sized coefficient 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. One unresolved boundary scalar and one shared degree-sized coefficient row.

Declaration kind. abbrev.

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

Lean code for Definition10.7.27●1 definition

abbrevdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond (k : ℕ) :
  Type

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond
  (k : ℕ) : Type

One unresolved boundary scalar and one shared degree-sized coefficient row.

Definition10.7.28

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “selected child”. First integer index of the selected child; 'r' is its remaining width.

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. First integer index of the selected child; 'r' is its remaining width.

Declaration kind. def.

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

Lean code for Definition10.7.28●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
  (schedule : ℕ → ℕ) (r : ℕ) (bit : Bool) : ℕ

def QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
  (schedule : ℕ → ℕ) (r : ℕ)
  (bit : Bool) : ℕ

First integer index of the selected child; `r` is its remaining width.

Definition10.7.29

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “block injection row”. Full-block injection parameters are exactly 'u=1+origin+step*first' and 'v=1+origin+step*(first+2^r)'.

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. Full-block injection parameters are exactly 'u=1+origin+step*first' and 'v=1+origin+step*(first+2^r)'. This row has only '2*k+2' entries.

Declaration kind. def.

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

Lean code for Definition10.7.29●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.blockInjectionRow (k : ℕ)
  (origin step : ℝ) (first r : ℕ) : Fin (2 * k + 1 + 1) → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.blockInjectionRow
  (k : ℕ) (origin step : ℝ)
  (first r : ℕ) : Fin (2 * k + 1 + 1) → ℝ

Full-block injection parameters are exactly `u=1+origin+step*first` and
`v=1+origin+step*(first+2^r)`. This row has only `2*k+2` entries.

Definition10.7.30

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “injection core”. Actual finite core, with one shared boundary state at every level.

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 finite core, with one shared boundary state at every level. Rows are input states; columns are output states. No prefix-indexed space occurs.

Declaration kind. def.

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

Lean code for Definition10.7.30●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.injectionCore (k : ℕ)
  (origin step : ℝ) (lower upper : ℕ) (schedule : ℕ → ℕ) (r : ℕ)
  (bit : Bool) :
  Matrix (QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond k)
    (QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond k) ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.injectionCore
  (k : ℕ) (origin step : ℝ)
  (lower upper : ℕ) (schedule : ℕ → ℕ)
  (r : ℕ) (bit : Bool) :
  Matrix
    (QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond
      k)
    (QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond
      k)
    ℝ

Actual finite core, with one shared boundary state at every level.
Rows are input states; columns are output states. No prefix-indexed space occurs.

Definition10.7.31

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “injection contract”. Finite matrix contraction, terminating with the coefficient-zero selector.

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. Finite matrix contraction, terminating with the coefficient-zero selector. The level is read from the suffix length, so every word shares one core sequence.

Declaration kind. def.

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

Lean code for Definition10.7.31●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract (k : ℕ)
  (origin step : ℝ) (lower upper : ℕ) (schedule : ℕ → ℕ) :
  List Bool →
    QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond k → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract
  (k : ℕ) (origin step : ℝ)
  (lower upper : ℕ) (schedule : ℕ → ℕ) :
  List Bool →
    QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond
        k →
      ℝ

Finite matrix contraction, terminating with the coefficient-zero selector.
The level is read from the suffix length, so every word shares one core sequence.

Theorem10.7.32

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “injection contract shared”; the hypotheses and conclusion in the code panel fix its exact scope. After injection, the finite contraction never re-enters the boundary state.

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. After injection, the finite contraction never re-enters the boundary state.

Declaration kind. theorem.

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

Lean code for Theorem10.7.32●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract_shared
  (k : ℕ) (origin step : ℝ) (lower upper : ℕ) (schedule : ℕ → ℕ)
  (bits : List Bool) (i : Fin (2 * k + 1 + 1)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract k
      origin step lower upper schedule bits (some i) =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedContract
      (2 * k + 1) bits i

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract_shared
  (k : ℕ) (origin step : ℝ)
  (lower upper : ℕ) (schedule : ℕ → ℕ)
  (bits : List Bool)
  (i : Fin (2 * k + 1 + 1)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract
      k origin step lower upper schedule
      bits (some i) =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedContract
      (2 * k + 1) bits i

After injection, the finite contraction never re-enters the boundary state.

Definition10.7.33

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “schedule valid”. The schedule obligation is purely integer control flow: any partial child must be the unique boundary node used by the next finite matrix.

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 schedule obligation is purely integer control flow: any partial child must be the unique boundary node used by the next finite matrix.

Declaration kind. def.

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

Lean code for Definition10.7.33●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.ScheduleValid
  (lower upper : ℕ) (schedule : ℕ → ℕ) (width : ℕ) : Prop

def QuantumBlockEncoding.HermiteBoundaryInjection.ScheduleValid
  (lower upper : ℕ) (schedule : ℕ → ℕ)
  (width : ℕ) : Prop

The schedule obligation is purely integer control flow: any partial child
must be the unique boundary node used by the next finite matrix.

Theorem10.7.34

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “injection contract boundary”; the hypotheses and conclusion in the code panel fix its exact scope. Finite Option(Fin) contraction equals the verified tree traversal whenever the current node is genuinely partial.

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. Finite Option(Fin) contraction equals the verified tree traversal whenever the current node is genuinely partial. There is no assumed source/core equality.

Declaration kind. theorem.

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

Lean code for Theorem10.7.34●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract_boundary
  (k : ℕ) (origin step : ℝ) (lower upper : ℕ) (schedule : ℕ → ℕ)
  (bits : List Bool)
  (hnext :
    QuantumBlockEncoding.HermiteBoundaryInjection.ScheduleValid lower
      upper schedule bits.length)
  (hp :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial lower upper
      (schedule bits.length) (2 ^ bits.length)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract k
      origin step lower upper schedule bits none =
    QuantumBlockEncoding.HermiteBoundaryInjection.boundaryReadout k
      origin step lower upper (schedule bits.length) bits

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract_boundary
  (k : ℕ) (origin step : ℝ)
  (lower upper : ℕ) (schedule : ℕ → ℕ)
  (bits : List Bool)
  (hnext :
    QuantumBlockEncoding.HermiteBoundaryInjection.ScheduleValid
      lower upper schedule bits.length)
  (hp :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial
      lower upper (schedule bits.length)
      (2 ^ bits.length)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract
      k origin step lower upper schedule
      bits none =
    QuantumBlockEncoding.HermiteBoundaryInjection.boundaryReadout
      k origin step lower upper
      (schedule bits.length) bits

Finite Option(Fin) contraction equals the verified tree traversal whenever
the current node is genuinely partial. There is no assumed source/core equality.

Definition10.7.35

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “boundary schedule”. Closed-form boundary schedule, computed by a single integer quotient per level.

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. Closed-form boundary schedule, computed by a single integer quotient per level.

Declaration kind. def.

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

Lean code for Definition10.7.35●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
  (lower r : ℕ) : ℕ

def QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
  (lower r : ℕ) : ℕ

Closed-form boundary schedule, computed by a single integer quotient per level.

Theorem10.7.36

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.36●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule_child
  (lower r : ℕ) (bit : Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
      (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
        lower)
      r bit =
    2 ^ r * (2 * (lower / 2 ^ (r + 1)) + if bit = true then 1 else 0)

theorem QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule_child
  (lower r : ℕ) (bit : Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
      (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
        lower)
      r bit =
    2 ^ r *
      (2 * (lower / 2 ^ (r + 1)) +
        if bit = true then 1 else 0)

Theorem10.7.37

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “boundary schedule valid”; the hypotheses and conclusion in the code panel fix its exact scope. The upper-half interval makes the quotient schedule valid at every level.

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 upper-half interval makes the quotient schedule valid at every level.

Declaration kind. theorem.

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

Lean code for Theorem10.7.37●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule_valid
  (lower n : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.ScheduleValid lower
    (2 ^ n)
    (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
      lower)
    (n + 1)

theorem QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule_valid
  (lower n : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.ScheduleValid
    lower (2 ^ n)
    (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
      lower)
    (n + 1)

The upper-half interval makes the quotient schedule valid at every level.

Theorem10.7.38

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.38●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule_root
  (lower n : ℕ) (hl : lower ≤ 2 ^ n) :
  QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule lower
      (n + 1) =
    0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule_root
  (lower n : ℕ) (hl : lower ≤ 2 ^ n) :
  QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
      lower (n + 1) =
    0

Theorem10.7.39

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.39●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middle_root_partial
  (lower n : ℕ) (hl : lower < 2 ^ n) :
  QuantumBlockEncoding.HermiteBoundaryInjection.Partial lower (2 ^ n) 0
    (2 ^ (n + 1))

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middle_root_partial
  (lower n : ℕ) (hl : lower < 2 ^ n) :
  QuantumBlockEncoding.HermiteBoundaryInjection.Partial
    lower (2 ^ n) 0 (2 ^ (n + 1))

Theorem10.7.40

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “partial left prefix eq”; the hypotheses and conclusion in the code panel fix its exact scope. A prefix interval '[0,upper)' has one unresolved aligned block as well.

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. A prefix interval '[0,upper)' has one unresolved aligned block as well.

Declaration kind. theorem.

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

Lean code for Theorem10.7.40●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.partial_left_prefix_eq
  (upper M x : ℕ) (hM : 0 < M)
  (hp :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial 0 upper
      (M * x) M) :
  x = upper / M

theorem QuantumBlockEncoding.HermiteBoundaryInjection.partial_left_prefix_eq
  (upper M x : ℕ) (hM : 0 < M)
  (hp :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial
      0 upper (M * x) M) :
  x = upper / M

A prefix interval `[0,upper)` has one unresolved aligned block as well.

Theorem10.7.41

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.41●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule_left_valid
  (upper width : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.ScheduleValid 0 upper
    (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
      upper)
    width

theorem QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule_left_valid
  (upper width : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.ScheduleValid
    0 upper
    (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
      upper)
    width

Definition10.7.42

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “scalar bond”. A scalar free branch needs only the boundary state and one shared 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. A scalar free branch needs only the boundary state and one shared state.

Declaration kind. abbrev.

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

Lean code for Definition10.7.42●1 definition

abbrevdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond : Type

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond :
  Type

A scalar free branch needs only the boundary state and one shared state.

Definition10.7.43

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.43●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
  (free : ℕ → Bool → ℝ) : List Bool → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
  (free : ℕ → Bool → ℝ) : List Bool → ℝ

Definition10.7.44

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.44●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.scalarCore
  (lower upper : ℕ) (schedule : ℕ → ℕ) (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ) (r : ℕ) (bit : Bool) :
  Matrix QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond
    QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.scalarCore
  (lower upper : ℕ) (schedule : ℕ → ℕ)
  (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ) (r : ℕ)
  (bit : Bool) :
  Matrix
    QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond
    QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond
    ℝ

Definition10.7.45

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.45●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract
  (lower upper : ℕ) (schedule : ℕ → ℕ) (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ) :
  List Bool →
    QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract
  (lower upper : ℕ) (schedule : ℕ → ℕ)
  (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ) :
  List Bool →
    QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond →
      ℝ

Theorem10.7.46

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.46●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract_shared
  (lower upper : ℕ) (schedule : ℕ → ℕ) (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract lower
      upper schedule inject free bits (some ()) =
    QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      free bits

theorem QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract_shared
  (lower upper : ℕ) (schedule : ℕ → ℕ)
  (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ)
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract
      lower upper schedule inject free
      bits (some ()) =
    QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      free bits

Definition10.7.47

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.47●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.scalarBoundaryReadout
  (lower upper : ℕ) (inject : ℕ → ℕ → ℝ) (free : ℕ → Bool → ℝ)
  (first : ℕ) (bits : List Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.scalarBoundaryReadout
  (lower upper : ℕ) (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ) (first : ℕ)
  (bits : List Bool) : ℝ

Theorem10.7.48

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scalar boundary readout eq”; the hypotheses and conclusion in the code panel fix its exact scope. A generic scalar source bridge, consumed below with a proved exponential suffix identity.

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. A generic scalar source bridge, consumed below with a proved exponential suffix identity. 'hinject' is local injection algebra, not a target/TT contract.

Declaration kind. theorem.

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

Lean code for Theorem10.7.48●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.scalarBoundaryReadout_eq
  (lower upper : ℕ) (inject : ℕ → ℕ → ℝ) (free : ℕ → Bool → ℝ)
  (target : ℕ → ℝ)
  (hinject :
    ∀ (first : ℕ) (bits : List Bool),
      inject first bits.length *
          QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
            free bits =
        target
          (first +
            QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits))
  (first : ℕ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarBoundaryReadout
      lower upper inject free first bits =
    if
        lower ≤
            first +
              QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits ∧
          first +
              QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits <
            upper then
      target
        (first +
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits)
    else 0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.scalarBoundaryReadout_eq
  (lower upper : ℕ) (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ) (target : ℕ → ℝ)
  (hinject :
    ∀ (first : ℕ) (bits : List Bool),
      inject first bits.length *
          QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
            free bits =
        target
          (first +
            QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits))
  (first : ℕ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarBoundaryReadout
      lower upper inject free first bits =
    if
        lower ≤
            first +
              QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits ∧
          first +
              QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits <
            upper then
      target
        (first +
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits)
    else 0

A generic scalar source bridge, consumed below with a proved exponential
suffix identity. `hinject` is local injection algebra, not a target/TT contract.

Theorem10.7.49

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.49●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract_boundary
  (lower upper : ℕ) (schedule : ℕ → ℕ) (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ) (bits : List Bool)
  (hnext :
    QuantumBlockEncoding.HermiteBoundaryInjection.ScheduleValid lower
      upper schedule bits.length)
  (hp :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial lower upper
      (schedule bits.length) (2 ^ bits.length)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract lower
      upper schedule inject free bits none =
    QuantumBlockEncoding.HermiteBoundaryInjection.scalarBoundaryReadout
      lower upper inject free (schedule bits.length) bits

theorem QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract_boundary
  (lower upper : ℕ) (schedule : ℕ → ℕ)
  (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ) (bits : List Bool)
  (hnext :
    QuantumBlockEncoding.HermiteBoundaryInjection.ScheduleValid
      lower upper schedule bits.length)
  (hp :
    QuantumBlockEncoding.HermiteBoundaryInjection.Partial
      lower upper (schedule bits.length)
      (2 ^ bits.length)) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract
      lower upper schedule inject free
      bits none =
    QuantumBlockEncoding.HermiteBoundaryInjection.scalarBoundaryReadout
      lower upper inject free
      (schedule bits.length) bits

Definition10.7.50

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “left free”. Stable left-tail factors use only nonpositive exponential arguments for positive step.

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. Stable left-tail factors use only nonpositive exponential arguments for positive step. The one digit contributes no factor.

Declaration kind. def.

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

Lean code for Definition10.7.50●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.leftFree (step : ℝ)
  (r : ℕ) (bit : Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.leftFree
  (step : ℝ) (r : ℕ) (bit : Bool) : ℝ

Stable left-tail factors use only nonpositive exponential arguments for
positive step. The one digit contributes no factor.

Definition10.7.51

uses 0used by 0✓L∃∀N

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

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/HermiteBoundaryInjection.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.7.51●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.leftInject
  (origin step : ℝ) (first r : ℕ) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.leftInject
  (origin step : ℝ) (first r : ℕ) : ℝ

Theorem10.7.52

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “left free contract eq”; 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/HermiteBoundaryInjection.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.7.52●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftFreeContract_eq
  (step : ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.leftFree step)
      bits =
    Real.exp
      (-step *
        (2 ^ bits.length - 1 -
          ↑(QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits)))

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftFreeContract_eq
  (step : ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.leftFree
        step)
      bits =
    Real.exp
      (-step *
        (2 ^ bits.length - 1 -
          ↑(QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits)))

Theorem10.7.53

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.53●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftInject_readout
  (origin step : ℝ) (first : ℕ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.leftInject origin step
        first bits.length *
      QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
        (QuantumBlockEncoding.HermiteBoundaryInjection.leftFree step)
        bits =
    Real.exp
      (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        step
        (first +
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits))

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftInject_readout
  (origin step : ℝ) (first : ℕ)
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.leftInject
        origin step first bits.length *
      QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
        (QuantumBlockEncoding.HermiteBoundaryInjection.leftFree
          step)
        bits =
    Real.exp
      (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin step
        (first +
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits))

Theorem10.7.54

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “left inject eq last”; the hypotheses and conclusion in the code panel fix its exact scope. Exact correspondence with the prototype's last included block index.

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. Exact correspondence with the prototype's last included block index.

Declaration kind. theorem.

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

Lean code for Theorem10.7.54●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftInject_eq_last
  (origin step : ℝ) (first r : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.leftInject origin step
      first r =
    Real.exp
      (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        step (first + 2 ^ r - 1))

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftInject_eq_last
  (origin step : ℝ) (first r : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.leftInject
      origin step first r =
    Real.exp
      (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin step (first + 2 ^ r - 1))

Exact correspondence with the prototype's last included block index.

Theorem10.7.55

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.55●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftFree_bounds (step : ℝ)
  (hs : 0 ≤ step) (r : ℕ) (bit : Bool) :
  0 ≤
      QuantumBlockEncoding.HermiteBoundaryInjection.leftFree step r
        bit ∧
    QuantumBlockEncoding.HermiteBoundaryInjection.leftFree step r bit ≤
      1

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftFree_bounds
  (step : ℝ) (hs : 0 ≤ step) (r : ℕ)
  (bit : Bool) :
  0 ≤
      QuantumBlockEncoding.HermiteBoundaryInjection.leftFree
        step r bit ∧
    QuantumBlockEncoding.HermiteBoundaryInjection.leftFree
        step r bit ≤
      1

Definition10.7.56

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “grid step”. The exact grid step on 'n+1' qubits; 'n' may be zero.

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

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

Technical source note. The exact grid step on 'n+1' qubits; 'n' may be zero.

Declaration kind. def.

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

Lean code for Definition10.7.56●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.gridStep (n : ℕ) (L : ℝ) :
  ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
  (n : ℕ) (L : ℝ) : ℝ

The exact grid step on `n+1` qubits; `n` may be zero.

Definition10.7.57

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.57●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat (n : ℕ)
  (L : ℝ) (j : ℕ) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
  (n : ℕ) (L : ℝ) (j : ℕ) : ℝ

Theorem10.7.58

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.58●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridStep_pos (n : ℕ)
  (L : ℝ) (hL : 0 < L) :
  0 < QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridStep_pos
  (n : ℕ) (L : ℝ) (hL : 0 < L) :
  0 <
    QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
      n L

Theorem10.7.59

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.59●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat_eq_gridPoint
  (n : ℕ) (L : ℝ) (j : Fin (QuantumBlockEncoding.gridSize (n + 1))) :
  QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L ↑j =
    QuantumBlockEncoding.HermiteStatePreparation.gridPoint (n + 1) L j

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat_eq_gridPoint
  (n : ℕ) (L : ℝ)
  (j :
    Fin
      (QuantumBlockEncoding.gridSize
        (n + 1))) :
  QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
      n L ↑j =
    QuantumBlockEncoding.HermiteStatePreparation.gridPoint
      (n + 1) L j

Theorem10.7.60

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.60●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat_midpoint
  (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L
      (2 ^ n) =
    0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat_midpoint
  (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
      n L (2 ^ n) =
    0

Theorem10.7.61

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grid point nat strict mono”; 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/HermiteBoundaryInjection.lean:684. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.7.61●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat_strictMono
  (n : ℕ) (L : ℝ) (hL : 0 < L) :
  StrictMono
    (QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L)

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat_strictMono
  (n : ℕ) (L : ℝ) (hL : 0 < L) :
  StrictMono
    (QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
      n L)

Theorem10.7.62

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grid point nat lt zero iff”; 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/HermiteBoundaryInjection.lean:692. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.7.62●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat_lt_zero_iff
  (n : ℕ) (L : ℝ) (hL : 0 < L) (j : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L j < 0 ↔
    j < 2 ^ n

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat_lt_zero_iff
  (n : ℕ) (L : ℝ) (hL : 0 < L) (j : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
        n L j <
      0 ↔
    j < 2 ^ n

Definition10.7.63

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “cut index”. Natural ceiling implements the lower clamp at zero.

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

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

Technical source note. Natural ceiling implements the lower clamp at zero. The upper clamp is redundant for positive 'L', as 'cutIndex_le_midpoint' proves.

Declaration kind. def.

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

Lean code for Definition10.7.63●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex (n : ℕ) (L : ℝ) :
  ℕ

def QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
  (n : ℕ) (L : ℝ) : ℕ

Natural ceiling implements the lower clamp at zero. The upper clamp is
redundant for positive `L`, as `cutIndex_le_midpoint` proves.

Theorem10.7.64

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “grid point nat lt neg one iff”; 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/HermiteBoundaryInjection.lean:702. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.7.64●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat_lt_neg_one_iff
  (n : ℕ) (L : ℝ) (hL : 0 < L) (j : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L j <
      -1 ↔
    j < QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L

theorem QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat_lt_neg_one_iff
  (n : ℕ) (L : ℝ) (hL : 0 < L) (j : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
        n L j <
      -1 ↔
    j <
      QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
        n L

Theorem10.7.65

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.65●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex_le_midpoint
  (n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L ≤ 2 ^ n

theorem QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex_le_midpoint
  (n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
      n L ≤
    2 ^ n

Theorem10.7.66

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “cut index eq clamped”; the hypotheses and conclusion in the code panel fix its exact scope. This is the candidate's exact clamped ceiling, before any rounding of pi.

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. This is the candidate's exact clamped ceiling, before any rounding of pi.

Declaration kind. theorem.

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

Lean code for Theorem10.7.66●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex_eq_clamped
  (n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L =
    min
      ⌈↑(2 ^ n) -
          ↑(QuantumBlockEncoding.gridSize (n + 1)) / (2 * Real.pi * L)⌉₊
      (2 ^ n)

theorem QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex_eq_clamped
  (n : ℕ) (L : ℝ) (hL : 0 < L) :
  QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
      n L =
    min
      ⌈↑(2 ^ n) -
          ↑(QuantumBlockEncoding.gridSize
                (n + 1)) /
            (2 * Real.pi * L)⌉₊
      (2 ^ n)

This is the candidate's exact clamped ceiling, before any rounding of pi.

Theorem10.7.67

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.67●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middle_membership_iff
  (n : ℕ) (L : ℝ) (hL : 0 < L) (j : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L ≤ j ∧
      j < 2 ^ n ↔
    -1 ≤
        QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L
          j ∧
      QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L j <
        0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middle_membership_iff
  (n : ℕ) (L : ℝ) (hL : 0 < L) (j : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
          n L ≤
        j ∧
      j < 2 ^ n ↔
    -1 ≤
        QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
          n L j ∧
      QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
          n L j <
        0

Theorem10.7.68

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “injection domain”; the hypotheses and conclusion in the code panel fix its exact scope. Every actual injected dyadic block has valid de Casteljau parameters, including a block whose excluded endpoint is the zero-coordinate midpoint.

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 actual injected dyadic block has valid de Casteljau parameters, including a block whose excluded endpoint is the zero-coordinate midpoint.

Declaration kind. theorem.

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

Lean code for Theorem10.7.68●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injection_domain (n : ℕ)
  (L : ℝ) (hL : 0 < L) (first size : ℕ) (hs : 0 < size)
  (hf :
    QuantumBlockEncoding.HermiteBoundaryInjection.Full
      (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L)
      (2 ^ n) first size) :
  0 ≤
      1 +
        QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L
          first ∧
    1 +
          QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L
            first <
        1 +
          QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L
            (first + size) ∧
      1 +
          QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L
            (first + size) ≤
        1

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injection_domain
  (n : ℕ) (L : ℝ) (hL : 0 < L)
  (first size : ℕ) (hs : 0 < size)
  (hf :
    QuantumBlockEncoding.HermiteBoundaryInjection.Full
      (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
        n L)
      (2 ^ n) first size) :
  0 ≤
      1 +
        QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
          n L first ∧
    1 +
          QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
            n L first <
        1 +
          QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
            n L (first + size) ∧
      1 +
          QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
            n L (first + size) ≤
        1

Every actual injected dyadic block has valid de Casteljau parameters,
including a block whose excluded endpoint is the zero-coordinate midpoint.

Definition10.7.69

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “middle readout”. The middle component uses the same one-boundary traversal as the prototype.

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 middle component uses the same one-boundary traversal as the prototype.

Declaration kind. def.

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

Lean code for Definition10.7.69●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout (k n : ℕ)
  (L : ℝ) (bits : List Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout
  (k n : ℕ) (L : ℝ) (bits : List Bool) : ℝ

The middle component uses the same one-boundary traversal as the prototype.

Theorem10.7.70

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.70●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout_eq (k n : ℕ)
  (L : ℝ) (hL : 0 < L) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout k n L
      bits =
    if
        -1 ≤
            QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n
              L
              (QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits) ∧
          QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L
              (QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits) <
            0 then
      Polynomial.eval
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L
          (QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits))
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)
    else 0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout_eq
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout
      k n L bits =
    if
        -1 ≤
            QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
              n L
              (QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits) ∧
          QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
              n L
              (QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
                bits) <
            0 then
      Polynomial.eval
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
          n L
          (QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits))
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
          k)
    else 0

Theorem10.7.71

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “middle readout empty”; the hypotheses and conclusion in the code panel fix its exact scope. A cutoff at the midpoint gives the prototype's zero middle component.

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. A cutoff at the midpoint gives the prototype's zero middle component.

Declaration kind. theorem.

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

Lean code for Theorem10.7.71●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout_empty
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (hcut :
    QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L = 2 ^ n)
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout k n L
      bits =
    0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout_empty
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (hcut :
    QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
        n L =
      2 ^ n)
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout
      k n L bits =
    0

A cutoff at the midpoint gives the prototype's zero middle component.

Definition10.7.72

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “word sample index”. Word-to-public-grid adapter, with explicit width equality.

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. Word-to-public-grid adapter, with explicit width equality.

Declaration kind. def.

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

Lean code for Definition10.7.72●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex (n : ℕ)
  (bits : List Bool) (hbits : bits.length = n + 1) :
  Fin (QuantumBlockEncoding.gridSize (n + 1))

def QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex
  (n : ℕ) (bits : List Bool)
  (hbits : bits.length = n + 1) :
  Fin
    (QuantumBlockEncoding.gridSize
      (n + 1))

Word-to-public-grid adapter, with explicit width equality.

Theorem10.7.73

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “middle readout eq masked sample”; the hypotheses and conclusion in the code panel fix its exact scope. All-bit exact source readout on the actual public sample API.

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. All-bit exact source readout on the actual public sample API. The center belongs to the right tail, while the sample at 'p=-1' belongs to this component.

Declaration kind. theorem.

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

Lean code for Theorem10.7.73●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout_eq_masked_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L) (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout k n L
      bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L ≤
            QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits ∧
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits <
            2 ^ n then
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
        (n + 1) L
        (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex n
          bits hbits)
    else 0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout_eq_masked_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout
      k n L bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
              n L ≤
            QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits ∧
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits <
            2 ^ n then
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
        k (n + 1) L
        (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex
          n bits hbits)
    else 0

All-bit exact source readout on the actual public sample API. The center
belongs to the right tail, while the sample at `p=-1` belongs to this component.

Definition10.7.74

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “middle finite readout”. The exact finite middle TT, including the prototype's empty-interval fast path.

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 finite middle TT, including the prototype's empty-interval fast path. Its boundary schedule and all source rows are formula-derived.

Declaration kind. def.

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

Lean code for Definition10.7.74●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout
  (k n : ℕ) (L : ℝ) (bits : List Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout
  (k n : ℕ) (L : ℝ) (bits : List Bool) : ℝ

The exact finite middle TT, including the prototype's empty-interval fast
path. Its boundary schedule and all source rows are formula-derived.

Theorem10.7.75

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “middle finite readout eq middle readout”; the hypotheses and conclusion in the code panel fix its exact scope. Source-derived one-boundary finite TT equals the verified interval traversal.

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. Source-derived one-boundary finite TT equals the verified interval traversal.

Declaration kind. theorem.

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

Lean code for Theorem10.7.75●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout_eq_middleReadout
  (k n : ℕ) (L : ℝ) (hL : 0 < L) (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout k n
      L bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout k n L
      bits

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout_eq_middleReadout
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout
      k n L bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.middleReadout
      k n L bits

Source-derived one-boundary finite TT equals the verified interval traversal.

Theorem10.7.76

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “middle finite readout eq masked sample”; the hypotheses and conclusion in the code panel fix its exact scope. Complete all-bit, actual-grid semantics of the finite middle TT.

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. Complete all-bit, actual-grid semantics of the finite middle TT. Its fixed bond is 'InjectionBond k', of cardinality '2*k+3', at every interior level.

Declaration kind. theorem.

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

Lean code for Theorem10.7.76●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout_eq_masked_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L) (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout k n
      L bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L ≤
            QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits ∧
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits <
            2 ^ n then
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
        (n + 1) L
        (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex n
          bits hbits)
    else 0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout_eq_masked_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout
      k n L bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
              n L ≤
            QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits ∧
          QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits <
            2 ^ n then
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
        k (n + 1) L
        (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex
          n bits hbits)
    else 0

Complete all-bit, actual-grid semantics of the finite middle TT. Its fixed
bond is `InjectionBond k`, of cardinality `2*k+3`, at every interior level.

Definition10.7.77

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.77●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout (n : ℕ)
  (L : ℝ) (bits : List Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout
  (n : ℕ) (L : ℝ) (bits : List Bool) : ℝ

Theorem10.7.78

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.78●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout_eq
  (n : ℕ) (L : ℝ) (hL : 0 < L) (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout n L
      bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits <
          QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n
            L then
      Real.exp
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L
          (QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits))
    else 0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout_eq
  (n : ℕ) (L : ℝ) (hL : 0 < L)
  (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout
      n L bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits <
          QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
            n L then
      Real.exp
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
          n L
          (QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits))
    else 0

Theorem10.7.79

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.79●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftInject_bounds (n : ℕ)
  (L : ℝ) (hL : 0 < L) (first r : ℕ)
  (hf :
    QuantumBlockEncoding.HermiteBoundaryInjection.Full 0
      (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L) first
      (2 ^ r)) :
  0 ≤
      QuantumBlockEncoding.HermiteBoundaryInjection.leftInject
        (-Real.pi * L)
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L)
        first r ∧
    QuantumBlockEncoding.HermiteBoundaryInjection.leftInject
        (-Real.pi * L)
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L)
        first r ≤
      1

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftInject_bounds
  (n : ℕ) (L : ℝ) (hL : 0 < L)
  (first r : ℕ)
  (hf :
    QuantumBlockEncoding.HermiteBoundaryInjection.Full
      0
      (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
        n L)
      first (2 ^ r)) :
  0 ≤
      QuantumBlockEncoding.HermiteBoundaryInjection.leftInject
        (-Real.pi * L)
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
          n L)
        first r ∧
    QuantumBlockEncoding.HermiteBoundaryInjection.leftInject
        (-Real.pi * L)
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
          n L)
        first r ≤
      1

Theorem10.7.80

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.80●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout_eq_masked_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L) (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout n L
      bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits <
          QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n
            L then
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
        (n + 1) L
        (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex n
          bits hbits)
    else 0

theorem QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout_eq_masked_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout
      n L bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits <
          QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
            n L then
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
        k (n + 1) L
        (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex
          n bits hbits)
    else 0

Definition10.7.81

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.81●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.rightFree (step : ℝ)
  (r : ℕ) (bit : Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.rightFree
  (step : ℝ) (r : ℕ) (bit : Bool) : ℝ

Theorem10.7.82

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.82●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.rightFree_bounds
  (step : ℝ) (hs : 0 ≤ step) (r : ℕ) (bit : Bool) :
  0 ≤
      QuantumBlockEncoding.HermiteBoundaryInjection.rightFree step r
        bit ∧
    QuantumBlockEncoding.HermiteBoundaryInjection.rightFree step r bit ≤
      1

theorem QuantumBlockEncoding.HermiteBoundaryInjection.rightFree_bounds
  (step : ℝ) (hs : 0 ≤ step) (r : ℕ)
  (bit : Bool) :
  0 ≤
      QuantumBlockEncoding.HermiteBoundaryInjection.rightFree
        step r bit ∧
    QuantumBlockEncoding.HermiteBoundaryInjection.rightFree
        step r bit ≤
      1

Theorem10.7.83

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.83●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.rightFreeContract_eq
  (step : ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.rightFree step)
      bits =
    Real.exp
      (-step *
        ↑(QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits))

theorem QuantumBlockEncoding.HermiteBoundaryInjection.rightFreeContract_eq
  (step : ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.rightFree
        step)
      bits =
    Real.exp
      (-step *
        ↑(QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits))

Definition10.7.84

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “right core”. Rank-one right component: the first MSB selects the right half; subsequent bits use bounded negative exponential factors.

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. Rank-one right component: the first MSB selects the right half; subsequent bits use bounded negative exponential factors.

Declaration kind. def.

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

Lean code for Definition10.7.84●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.rightCore (n : ℕ)
  (step : ℝ) (r : ℕ) (bit : Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.rightCore
  (n : ℕ) (step : ℝ) (r : ℕ)
  (bit : Bool) : ℝ

Rank-one right component: the first MSB selects the right half; subsequent
bits use bounded negative exponential factors.

Theorem10.7.85

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.85●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.rightCore_suffix (n : ℕ)
  (step : ℝ) (bits : List Bool) (hlen : bits.length ≤ n) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.rightCore n step)
      bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.rightFree step)
      bits

theorem QuantumBlockEncoding.HermiteBoundaryInjection.rightCore_suffix
  (n : ℕ) (step : ℝ) (bits : List Bool)
  (hlen : bits.length ≤ n) :
  QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.rightCore
        n step)
      bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.rightFree
        step)
      bits

Definition10.7.86

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.86●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout (n : ℕ)
  (L : ℝ) (bits : List Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout
  (n : ℕ) (L : ℝ) (bits : List Bool) : ℝ

Theorem10.7.87

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.87●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout_eq
  (n : ℕ) (L : ℝ) (bits : List Bool) (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout n L
      bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits <
          2 ^ n then
      0
    else
      Real.exp
        (-QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat n L
            (QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits))

theorem QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout_eq
  (n : ℕ) (L : ℝ) (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout
      n L bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits <
          2 ^ n then
      0
    else
      Real.exp
        (-QuantumBlockEncoding.HermiteBoundaryInjection.gridPointNat
            n L
            (QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
              bits))

Theorem10.7.88

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.88●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout_eq_masked_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L) (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout n L
      bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.wordValue bits <
          2 ^ n then
      0
    else
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
        (n + 1) L
        (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex n
          bits hbits)

theorem QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout_eq_masked_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout
      n L bits =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.wordValue
            bits <
          2 ^ n then
      0
    else
      QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
        k (n + 1) L
        (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex
          n bits hbits)

Theorem10.7.89

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “three branch readout eq sample”; the hypotheses and conclusion in the code panel fix its exact scope. Exact three-component source action.

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. Exact three-component source action. No cancellation between masked polynomials or out-of-domain exponential evaluations appears in the construction.

Declaration kind. theorem.

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

Lean code for Theorem10.7.89●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.threeBranchReadout_eq_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L) (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout n L
          bits +
        QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout
          k n L bits +
      QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout n
        L bits =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
      (n + 1) L
      (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex n
        bits hbits)

theorem QuantumBlockEncoding.HermiteBoundaryInjection.threeBranchReadout_eq_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout
          n L bits +
        QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout
          k n L bits +
      QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout
        n L bits =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
      k (n + 1) L
      (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex
        n bits hbits)

Exact three-component source action. No cancellation between masked
polynomials or out-of-domain exponential evaluations appears in the construction.

Definition10.7.90

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “kernel”. A common fixed-bond kernel interface.

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. A common fixed-bond kernel interface. The natural level counts unconsumed digits after the current digit; its stage-'t' value is 'n-t' on 'n+1' qubits.

Declaration kind. abbrev.

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

Lean code for Definition10.7.90●1 definition

abbrevdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.Kernel.{u_1}
  (B : Type u_1) : Type u_1

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.Kernel.{u_1}
  (B : Type u_1) : Type u_1

A common fixed-bond kernel interface. The natural level counts unconsumed
digits after the current digit; its stage-`t` value is `n-t` on `n+1` qubits.

Definition10.7.91

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.91●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract.{u_1}
  {B : Type u_1} [Fintype B]
  (K : QuantumBlockEncoding.HermiteBoundaryInjection.Kernel B)
  (right : B → ℝ) : List Bool → B → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract.{u_1}
  {B : Type u_1} [Fintype B]
  (K :
    QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
      B)
  (right : B → ℝ) : List Bool → B → ℝ

Definition10.7.92

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.92●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude.{u_1}
  {B : Type u_1} [Fintype B]
  (K : QuantumBlockEncoding.HermiteBoundaryInjection.Kernel B)
  (left right : B → ℝ) (bits : List Bool) : ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude.{u_1}
  {B : Type u_1} [Fintype B]
  (K :
    QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
      B)
  (left right : B → ℝ)
  (bits : List Bool) : ℝ

Definition10.7.93

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.93●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.sumKernel.{u_1, u_2}
  {B : Type u_1} {C : Type u_2}
  (K : QuantumBlockEncoding.HermiteBoundaryInjection.Kernel B)
  (H : QuantumBlockEncoding.HermiteBoundaryInjection.Kernel C) :
  QuantumBlockEncoding.HermiteBoundaryInjection.Kernel (B ⊕ C)

def QuantumBlockEncoding.HermiteBoundaryInjection.sumKernel.{u_1,
    u_2}
  {B : Type u_1} {C : Type u_2}
  (K :
    QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
      B)
  (H :
    QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
      C) :
  QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
    (B ⊕ C)

Theorem10.7.94

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.94●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract_sum_inl.{u_1,
    u_2}
  {B : Type u_1} {C : Type u_2} [Fintype B] [Fintype C]
  (K : QuantumBlockEncoding.HermiteBoundaryInjection.Kernel B)
  (H : QuantumBlockEncoding.HermiteBoundaryInjection.Kernel C)
  (right : B → ℝ) (last : C → ℝ) (bits : List Bool) (i : B) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.sumKernel K H)
      (Sum.elim right last) bits (Sum.inl i) =
    QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract K right
      bits i

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract_sum_inl.{u_1,
    u_2}
  {B : Type u_1} {C : Type u_2}
  [Fintype B] [Fintype C]
  (K :
    QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
      B)
  (H :
    QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
      C)
  (right : B → ℝ) (last : C → ℝ)
  (bits : List Bool) (i : B) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.sumKernel
        K H)
      (Sum.elim right last) bits
      (Sum.inl i) =
    QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      K right bits i

Theorem10.7.95

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.95●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract_sum_inr.{u_1,
    u_2}
  {B : Type u_1} {C : Type u_2} [Fintype B] [Fintype C]
  (K : QuantumBlockEncoding.HermiteBoundaryInjection.Kernel B)
  (H : QuantumBlockEncoding.HermiteBoundaryInjection.Kernel C)
  (right : B → ℝ) (last : C → ℝ) (bits : List Bool) (i : C) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.sumKernel K H)
      (Sum.elim right last) bits (Sum.inr i) =
    QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract H last
      bits i

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract_sum_inr.{u_1,
    u_2}
  {B : Type u_1} {C : Type u_2}
  [Fintype B] [Fintype C]
  (K :
    QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
      B)
  (H :
    QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
      C)
  (right : B → ℝ) (last : C → ℝ)
  (bits : List Bool) (i : C) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.sumKernel
        K H)
      (Sum.elim right last) bits
      (Sum.inr i) =
    QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      H last bits i

Theorem10.7.96

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.96●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude_sum.{u_1,
    u_2}
  {B : Type u_1} {C : Type u_2} [Fintype B] [Fintype C]
  (K : QuantumBlockEncoding.HermiteBoundaryInjection.Kernel B)
  (H : QuantumBlockEncoding.HermiteBoundaryInjection.Kernel C)
  (left right : B → ℝ) (first last : C → ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
      (QuantumBlockEncoding.HermiteBoundaryInjection.sumKernel K H)
      (Sum.elim left first) (Sum.elim right last) bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude K left
        right bits +
      QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude H
        first last bits

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude_sum.{u_1,
    u_2}
  {B : Type u_1} {C : Type u_2}
  [Fintype B] [Fintype C]
  (K :
    QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
      B)
  (H :
    QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
      C)
  (left right : B → ℝ)
  (first last : C → ℝ)
  (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
      (QuantumBlockEncoding.HermiteBoundaryInjection.sumKernel
        K H)
      (Sum.elim left first)
      (Sum.elim right last) bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
        K left right bits +
      QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
        H first last bits

Definition10.7.97

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.97●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.injectionTerminal
  (k : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond k → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.injectionTerminal
  (k : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond
      k →
    ℝ

Definition10.7.98

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.98●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.scalarTerminal :
  QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.scalarTerminal :
  QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond →
    ℝ

Theorem10.7.99

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.99●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract_injection
  (k : ℕ) (origin step : ℝ) (lower upper : ℕ) (schedule : ℕ → ℕ)
  (bits : List Bool)
  (i : QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond k) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.injectionCore k
        origin step lower upper schedule)
      (QuantumBlockEncoding.HermiteBoundaryInjection.injectionTerminal
        k)
      bits i =
    QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract k
      origin step lower upper schedule bits i

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract_injection
  (k : ℕ) (origin step : ℝ)
  (lower upper : ℕ) (schedule : ℕ → ℕ)
  (bits : List Bool)
  (i :
    QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond
      k) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.injectionCore
        k origin step lower upper
        schedule)
      (QuantumBlockEncoding.HermiteBoundaryInjection.injectionTerminal
        k)
      bits i =
    QuantumBlockEncoding.HermiteBoundaryInjection.injectionContract
      k origin step lower upper schedule
      bits i

Theorem10.7.100

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.100●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract_scalar
  (lower upper : ℕ) (schedule : ℕ → ℕ) (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ) (bits : List Bool)
  (i : QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.scalarCore lower
        upper schedule inject free)
      QuantumBlockEncoding.HermiteBoundaryInjection.scalarTerminal bits
      i =
    QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract lower
      upper schedule inject free bits i

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract_scalar
  (lower upper : ℕ) (schedule : ℕ → ℕ)
  (inject : ℕ → ℕ → ℝ)
  (free : ℕ → Bool → ℝ) (bits : List Bool)
  (i :
    QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (QuantumBlockEncoding.HermiteBoundaryInjection.scalarCore
        lower upper schedule inject free)
      QuantumBlockEncoding.HermiteBoundaryInjection.scalarTerminal
      bits i =
    QuantumBlockEncoding.HermiteBoundaryInjection.scalarContract
      lower upper schedule inject free
      bits i

Theorem10.7.101

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.101●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract_unit
  (free : ℕ → Bool → ℝ) (bits : List Bool) (i : Unit) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (fun r bit x x_1 => free r bit) (fun x => 1) bits i =
    QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      free bits

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract_unit
  (free : ℕ → Bool → ℝ) (bits : List Bool)
  (i : Unit) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelContract
      (fun r bit x x_1 => free r bit)
      (fun x => 1) bits i =
    QuantumBlockEncoding.HermiteBoundaryInjection.scalarFreeContract
      free bits

Definition10.7.102

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.102●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.leftKernel (n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
    QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond

def QuantumBlockEncoding.HermiteBoundaryInjection.leftKernel
  (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
    QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond

Definition10.7.103

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.103●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.middleKernel (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
    (QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond k)

def QuantumBlockEncoding.HermiteBoundaryInjection.middleKernel
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
    (QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond
      k)

Definition10.7.104

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.104●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.rightKernel (n : ℕ)
  (L : ℝ) : QuantumBlockEncoding.HermiteBoundaryInjection.Kernel Unit

def QuantumBlockEncoding.HermiteBoundaryInjection.rightKernel
  (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
    Unit

Definition10.7.105

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.105●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.leftInitial (n : ℕ)
  (L : ℝ) : QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.leftInitial
  (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.ScalarBond →
    ℝ

Definition10.7.106

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.106●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.middleInitial (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond k → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.middleInitial
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond
      k →
    ℝ

Theorem10.7.107

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.107●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude_left
  (n : ℕ) (L : ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
      (QuantumBlockEncoding.HermiteBoundaryInjection.leftKernel n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.leftInitial n L)
      QuantumBlockEncoding.HermiteBoundaryInjection.scalarTerminal
      bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout n L
      bits

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude_left
  (n : ℕ) (L : ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
      (QuantumBlockEncoding.HermiteBoundaryInjection.leftKernel
        n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.leftInitial
        n L)
      QuantumBlockEncoding.HermiteBoundaryInjection.scalarTerminal
      bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.leftFiniteReadout
      n L bits

Theorem10.7.108

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.108●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude_middle
  (k n : ℕ) (L : ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
      (QuantumBlockEncoding.HermiteBoundaryInjection.middleKernel k n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.middleInitial k n
        L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.injectionTerminal
        k)
      bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout k
      n L bits

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude_middle
  (k n : ℕ) (L : ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
      (QuantumBlockEncoding.HermiteBoundaryInjection.middleKernel
        k n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.middleInitial
        k n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.injectionTerminal
        k)
      bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.middleFiniteReadout
      k n L bits

Theorem10.7.109

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.109●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude_right
  (n : ℕ) (L : ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
      (QuantumBlockEncoding.HermiteBoundaryInjection.rightKernel n L)
      (fun x => 1) (fun x => 1) bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout n L
      bits

theorem QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude_right
  (n : ℕ) (L : ℝ) (bits : List Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
      (QuantumBlockEncoding.HermiteBoundaryInjection.rightKernel
        n L)
      (fun x => 1) (fun x => 1) bits =
    QuantumBlockEncoding.HermiteBoundaryInjection.rightFiniteReadout
      n L bits

Definition10.7.110

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “hermite finite bond”. One fixed direct-sum bond, with no state allocated per dyadic prefix.

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. One fixed direct-sum bond, with no state allocated per dyadic prefix.

Declaration kind. abbrev.

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

Lean code for Definition10.7.110●1 definition

abbrevdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
  (k : ℕ) : Type

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
  (k : ℕ) : Type

One fixed direct-sum bond, with no state allocated per dyadic prefix.

Definition10.7.111

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.111●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
    (QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k)

def QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.Kernel
    (QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k)

Definition10.7.112

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.112●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.hermiteInitial (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.hermiteInitial
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k →
    ℝ

Definition10.7.113

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.7.113●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.hermiteTerminal (k : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k → ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.hermiteTerminal
  (k : ℕ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k →
    ℝ

Theorem10.7.114

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite kernel eq sample”; the hypotheses and conclusion in the code panel fix its exact scope. Main exact real-algebra root: one formula-derived fixed-width kernel family and explicit left/right boundaries produce every literal Hermite sample.

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. Main exact real-algebra root: one formula-derived fixed-width kernel family and explicit left/right boundaries produce every literal Hermite sample.

Declaration kind. theorem.

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

Lean code for Theorem10.7.114●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel_eq_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L) (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel k n
        L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteInitial k n
        L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteTerminal k)
      bits =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude k
      (n + 1) L
      (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex n
        bits hbits)

theorem QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel_eq_sample
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (bits : List Bool)
  (hbits : bits.length = n + 1) :
  QuantumBlockEncoding.HermiteBoundaryInjection.kernelAmplitude
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel
        k n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteInitial
        k n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.hermiteTerminal
        k)
      bits =
    QuantumBlockEncoding.HermiteStatePreparation.sampledAmplitude
      k (n + 1) L
      (QuantumBlockEncoding.HermiteBoundaryInjection.wordSampleIndex
        n bits hbits)

Main exact real-algebra root: one formula-derived fixed-width kernel family
and explicit left/right boundaries produce every literal Hermite sample.

Theorem10.7.115

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.115●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.hermiteFiniteBond_card
  (k : ℕ) :
  Fintype.card
      (QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
        k) =
    2 * k + 6

theorem QuantumBlockEncoding.HermiteBoundaryInjection.hermiteFiniteBond_card
  (k : ℕ) :
  Fintype.card
      (QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
        k) =
    2 * k + 6

Definition10.7.116

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “hermite core address”. Address space of the actual two-slice cores on 'n+1' 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. Address space of the actual two-slice cores on 'n+1' qubits. Its size is polynomial; this is a storage count, not a finite-bit arithmetic cost theorem.

Declaration kind. abbrev.

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

Lean code for Definition10.7.116●1 definition

abbrevdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.HermiteCoreAddress
  (k n : ℕ) : Type

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.HermiteCoreAddress
  (k n : ℕ) : Type

Address space of the actual two-slice cores on `n+1` qubits. Its size is
polynomial; this is a storage count, not a finite-bit arithmetic cost theorem.

Definition10.7.117

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.7.117●1 definition

defdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

def QuantumBlockEncoding.HermiteBoundaryInjection.hermiteCoreEntry (k n : ℕ)
  (L : ℝ)
  (a :
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteCoreAddress k
      n) :
  ℝ

def QuantumBlockEncoding.HermiteBoundaryInjection.hermiteCoreEntry
  (k n : ℕ) (L : ℝ)
  (a :
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteCoreAddress
      k n) :
  ℝ

Theorem10.7.118

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.118●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.hermiteCoreAddress_card
  (k n : ℕ) :
  Fintype.card
      (QuantumBlockEncoding.HermiteBoundaryInjection.HermiteCoreAddress
        k n) =
    2 * (n + 1) * (2 * k + 6) ^ 2

theorem QuantumBlockEncoding.HermiteBoundaryInjection.hermiteCoreAddress_card
  (k n : ℕ) :
  Fintype.card
      (QuantumBlockEncoding.HermiteBoundaryInjection.HermiteCoreAddress
        k n) =
    2 * (n + 1) * (2 * k + 6) ^ 2

Theorem10.7.119

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.119●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectionBond_card
  (k : ℕ) :
  Fintype.card
      (QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond k) =
    2 * k + 3

theorem QuantumBlockEncoding.HermiteBoundaryInjection.injectionBond_card
  (k : ℕ) :
  Fintype.card
      (QuantumBlockEncoding.HermiteBoundaryInjection.InjectionBond
        k) =
    2 * k + 3

Definition10.7.120

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “middle bond”. Candidate middle register: one boundary scalar plus the shared coefficients.

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. Candidate middle register: one boundary scalar plus the shared coefficients. The cardinality is not, by itself, a matrix-product realization theorem.

Declaration kind. abbrev.

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

Lean code for Definition10.7.120●1 definition

abbrevdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.MiddleBond (k : ℕ) : Type

abbrev QuantumBlockEncoding.HermiteBoundaryInjection.MiddleBond
  (k : ℕ) : Type

Candidate middle register: one boundary scalar plus the shared coefficients.
The cardinality is not, by itself, a matrix-product realization theorem.

Theorem10.7.121

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.7.121●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteBoundaryInjection.lean

complete

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleBond_card (k : ℕ) :
  Fintype.card
      (QuantumBlockEncoding.HermiteBoundaryInjection.MiddleBond k) =
    2 * k + 3

theorem QuantumBlockEncoding.HermiteBoundaryInjection.middleBond_card
  (k : ℕ) :
  Fintype.card
      (QuantumBlockEncoding.HermiteBoundaryInjection.MiddleBond
        k) =
    2 * k + 3