10.59. QuantumBlockEncoding/StoredHermiteBoundaries.lean🔗

12 explicit public declarations, in source order.

Definition10.59.1

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.59.1●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

def QuantumBlockEncoding.StoredHermiteBoundaries.initialLiteral {k : ℕ}
  (left middle : Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k → ℝ

def QuantumBlockEncoding.StoredHermiteBoundaries.initialLiteral
  {k : ℕ} (left middle : Bool) :
  QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k →
    ℝ

Definition10.59.2

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.59.2●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

def QuantumBlockEncoding.StoredHermiteBoundaries.terminalLiteral {k : ℕ} :
  QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k → ℝ

def QuantumBlockEncoding.StoredHermiteBoundaries.terminalLiteral
  {k : ℕ} :
  QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k →
    ℝ

Definition10.59.3

uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. def.

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

Lean code for Definition10.59.3●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

def QuantumBlockEncoding.StoredHermiteBoundaries.initial
  (k cut midpoint : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (2 * k + 6))

def QuantumBlockEncoding.StoredHermiteBoundaries.initial
  (k cut midpoint : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (2 * k + 6))

Definition10.59.4

uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. def.

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

Lean code for Definition10.59.4●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

def QuantumBlockEncoding.StoredHermiteBoundaries.terminal (k : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (2 * k + 6))

def QuantumBlockEncoding.StoredHermiteBoundaries.terminal
  (k : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (2 * k + 6))

Theorem10.59.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.59.5●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

theorem QuantumBlockEncoding.StoredHermiteBoundaries.initial_get
  (k cut midpoint : ℕ) (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.initial k cut
          midpoint).value[↑i] =
    QuantumBlockEncoding.StoredHermiteBoundaries.initialLiteral
      (decide (cut ≠ 0)) (decide (cut ≠ midpoint))
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv k) i)

theorem QuantumBlockEncoding.StoredHermiteBoundaries.initial_get
  (k cut midpoint : ℕ)
  (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.initial
          k cut midpoint).value[↑i] =
    QuantumBlockEncoding.StoredHermiteBoundaries.initialLiteral
      (decide (cut ≠ 0))
      (decide (cut ≠ midpoint))
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv
          k)
        i)

Theorem10.59.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.59.6●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

theorem QuantumBlockEncoding.StoredHermiteBoundaries.terminal_get (k : ℕ)
  (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.terminal k).value[↑i] =
    QuantumBlockEncoding.StoredHermiteBoundaries.terminalLiteral
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv k) i)

theorem QuantumBlockEncoding.StoredHermiteBoundaries.terminal_get
  (k : ℕ) (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.terminal
          k).value[↑i] =
    QuantumBlockEncoding.StoredHermiteBoundaries.terminalLiteral
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv
          k)
        i)

Theorem10.59.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.59.7●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

theorem QuantumBlockEncoding.StoredHermiteBoundaries.initial_value (k n : ℕ)
  (L : ℝ) (cut : ℕ)
  (hcut :
    cut = QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L)
  (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.initial k cut
          (2 ^ n)).value[↑i] =
    QuantumBlockEncoding.HermiteExplicitBond.initial k n L i

theorem QuantumBlockEncoding.StoredHermiteBoundaries.initial_value
  (k n : ℕ) (L : ℝ) (cut : ℕ)
  (hcut :
    cut =
      QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
        n L)
  (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.initial
          k cut (2 ^ n)).value[↑i] =
    QuantumBlockEncoding.HermiteExplicitBond.initial
      k n L i

Theorem10.59.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.59.8●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

theorem QuantumBlockEncoding.StoredHermiteBoundaries.terminal_value (k : ℕ)
  (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.terminal k).value[↑i] =
    QuantumBlockEncoding.HermiteExplicitBond.terminal k i

theorem QuantumBlockEncoding.StoredHermiteBoundaries.terminal_value
  (k : ℕ) (i : Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.terminal
          k).value[↑i] =
    QuantumBlockEncoding.HermiteExplicitBond.terminal
      k i

Theorem10.59.9

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “initial cost”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.59.9●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

theorem QuantumBlockEncoding.StoredHermiteBoundaries.initial_cost
  (k cut midpoint : ℕ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.initial k cut
          midpoint).cost
      op =
    2 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare op +
      (2 * k + 6) *
        (12 *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.compare op +
            2 *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.read op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write op)

theorem QuantumBlockEncoding.StoredHermiteBoundaries.initial_cost
  (k cut midpoint : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.initial
          k cut midpoint).cost
      op =
    2 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.compare
          op +
      (2 * k + 6) *
        (12 *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.compare
                op +
            2 *
              QuantumBlockEncoding.StoredGivens.tick
                QuantumBlockEncoding.StoredGivens.Op.read
                op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write
              op)

Theorem10.59.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “terminal cost”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.59.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

theorem QuantumBlockEncoding.StoredHermiteBoundaries.terminal_cost (k : ℕ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.terminal k).cost op =
    (2 * k + 6) *
      (12 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.compare op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write op)

theorem QuantumBlockEncoding.StoredHermiteBoundaries.terminal_cost
  (k : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteBoundaries.terminal
          k).cost
      op =
    (2 * k + 6) *
      (12 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.compare
              op +
          2 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.write
            op)

Theorem10.59.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “initial total cost”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.59.11●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

theorem QuantumBlockEncoding.StoredHermiteBoundaries.initial_total_cost
  (k cut midpoint : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteBoundaries.initial k cut
          midpoint).cost =
    16 * (2 * k + 6) + 2

theorem QuantumBlockEncoding.StoredHermiteBoundaries.initial_total_cost
  (k cut midpoint : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteBoundaries.initial
          k cut midpoint).cost =
    16 * (2 * k + 6) + 2

Theorem10.59.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “terminal total cost”; the hypotheses and conclusion in the code panel fix its exact scope.

Formal status. Compiled theorem in the default ASPBE import surface; the displayed Lean signature is the authoritative claim.

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.59.12●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteBoundaries.lean

complete

theorem QuantumBlockEncoding.StoredHermiteBoundaries.terminal_total_cost
  (k : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteBoundaries.terminal k).cost =
    16 * (2 * k + 6)

theorem QuantumBlockEncoding.StoredHermiteBoundaries.terminal_total_cost
  (k : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteBoundaries.terminal
          k).cost =
    16 * (2 * k + 6)