10.63. QuantumBlockEncoding/StoredHermiteKernelTable.lean🔗

16 explicit public declarations, in source order.

Definition10.63.1

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “fields”. A proposition-valued field is a requirement until a constructor supplies it. P=2k+2, written in the definitional form used by InjectionBond.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

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

Technical source note. P=2k+2, written in the definitional form used by InjectionBond.

Declaration kind. structure.

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

Lean code for Definition10.63.1●1 definition

structure(7 fields)defined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

structure QuantumBlockEncoding.StoredHermiteKernelTable.Fields (k : ℕ) : Type

structure QuantumBlockEncoding.StoredHermiteKernelTable.Fields
  (k : ℕ) : Type

P=2k+2, written in the definitional form used by InjectionBond.

Fields

leftPartial : Bool

leftInjection : ℝ

leftFree : ℝ

middlePartial : Bool

middleInjection : Vector ℝ (2 * k + 1 + 1)

shared : QuantumBlockEncoding.StoredGivens.StoredMatrix (2 * k + 1 + 1) (2 * k + 1 + 1)

rightCore : ℝ

Definition10.63.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “block view”. Mathematical block interpretation; not used to evaluate stored entries.

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. Mathematical block interpretation; not used to evaluate stored entries.

Declaration kind. def.

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

Lean code for Definition10.63.2●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

def QuantumBlockEncoding.StoredHermiteKernelTable.blockView {k : ℕ}
  (f : QuantumBlockEncoding.StoredHermiteKernelTable.Fields k) :
  QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k →
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k →
      ℝ

def QuantumBlockEncoding.StoredHermiteKernelTable.blockView
  {k : ℕ}
  (f :
    QuantumBlockEncoding.StoredHermiteKernelTable.Fields
      k) :
  QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k →
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
        k →
      ℝ

Mathematical block interpretation; not used to evaluate stored entries.

Definition10.63.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “stored block”. Actual stored-word readers and literal-zero blocks.

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 stored-word readers and literal-zero blocks.

Declaration kind. def.

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

Lean code for Definition10.63.3●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

def QuantumBlockEncoding.StoredHermiteKernelTable.storedBlock {k : ℕ}
  (f : QuantumBlockEncoding.StoredHermiteKernelTable.Fields k)
  (a b :
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredHermiteKernelTable.storedBlock
  {k : ℕ}
  (f :
    QuantumBlockEncoding.StoredHermiteKernelTable.Fields
      k)
  (a b :
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Actual stored-word readers and literal-zero blocks.

Theorem10.63.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.63.4●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

theorem QuantumBlockEncoding.StoredHermiteKernelTable.storedBlock_value {k : ℕ}
  (f : QuantumBlockEncoding.StoredHermiteKernelTable.Fields k)
  (a b :
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k) :
  (QuantumBlockEncoding.StoredHermiteKernelTable.storedBlock f a
        b).value =
    QuantumBlockEncoding.StoredHermiteKernelTable.blockView f a b

theorem QuantumBlockEncoding.StoredHermiteKernelTable.storedBlock_value
  {k : ℕ}
  (f :
    QuantumBlockEncoding.StoredHermiteKernelTable.Fields
      k)
  (a b :
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k) :
  (QuantumBlockEncoding.StoredHermiteKernelTable.storedBlock
        f a b).value =
    QuantumBlockEncoding.StoredHermiteKernelTable.blockView
      f a b

Definition10.63.5

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “decode”. The production explicit equivalence is executable, not a cardinality choice.

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 production explicit equivalence is executable, not a cardinality choice. A fixed overcharge covers its sum and option comparisons.

Declaration kind. def.

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

Lean code for Definition10.63.5●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

def QuantumBlockEncoding.StoredHermiteKernelTable.decode (k : ℕ)
  (a : Fin (2 * k + 6)) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k)

def QuantumBlockEncoding.StoredHermiteKernelTable.decode
  (k : ℕ) (a : Fin (2 * k + 6)) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k)

The production explicit equivalence is executable, not a cardinality
choice. A fixed overcharge covers its sum and option comparisons.

Definition10.63.6

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.63.6●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

def QuantumBlockEncoding.StoredHermiteKernelTable.entry {k : ℕ}
  (fields :
    Vector (QuantumBlockEncoding.StoredHermiteKernelTable.Fields k) 2)
  (a : Fin (2 * k + 6)) (out : Fin 2 × Fin (2 * k + 6)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredHermiteKernelTable.entry
  {k : ℕ}
  (fields :
    Vector
      (QuantumBlockEncoding.StoredHermiteKernelTable.Fields
        k)
      2)
  (a : Fin (2 * k + 6))
  (out : Fin 2 × Fin (2 * k + 6)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Theorem10.63.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.63.7●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

theorem QuantumBlockEncoding.StoredHermiteKernelTable.entry_value {k : ℕ}
  (fields :
    Vector (QuantumBlockEncoding.StoredHermiteKernelTable.Fields k) 2)
  (a : Fin (2 * k + 6)) (out : Fin 2 × Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteKernelTable.entry fields a
        out).value =
    QuantumBlockEncoding.StoredHermiteKernelTable.blockView
      fields[↑out.1]
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv k) a)
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv k) out.2)

theorem QuantumBlockEncoding.StoredHermiteKernelTable.entry_value
  {k : ℕ}
  (fields :
    Vector
      (QuantumBlockEncoding.StoredHermiteKernelTable.Fields
        k)
      2)
  (a : Fin (2 * k + 6))
  (out : Fin 2 × Fin (2 * k + 6)) :
  (QuantumBlockEncoding.StoredHermiteKernelTable.entry
        fields a out).value =
    QuantumBlockEncoding.StoredHermiteKernelTable.blockView
      fields[↑out.1]
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv
          k)
        a)
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv
          k)
        out.2)

Definition10.63.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “assemble”. Output columns are exactly finProdFinEquiv (bit, outgoing bond), as in StoredTensorTrain.denoteCore.

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. Output columns are exactly finProdFinEquiv (bit, outgoing bond), as in StoredTensorTrain.denoteCore. Thus each row stores both bit slices.

Declaration kind. def.

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

Lean code for Definition10.63.8●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

def QuantumBlockEncoding.StoredHermiteKernelTable.assemble {k : ℕ}
  (fields :
    Vector (QuantumBlockEncoding.StoredHermiteKernelTable.Fields k) 2) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.StoredCore (2 * k + 6)
      (2 * k + 6))

def QuantumBlockEncoding.StoredHermiteKernelTable.assemble
  {k : ℕ}
  (fields :
    Vector
      (QuantumBlockEncoding.StoredHermiteKernelTable.Fields
        k)
      2) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredTensorTrain.StoredCore
      (2 * k + 6) (2 * k + 6))

Output columns are exactly finProdFinEquiv (bit, outgoing bond), as in
StoredTensorTrain.denoteCore. Thus each row stores both bit slices.

Theorem10.63.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.63.9●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

theorem QuantumBlockEncoding.StoredHermiteKernelTable.assemble_value {k : ℕ}
  (fields :
    Vector (QuantumBlockEncoding.StoredHermiteKernelTable.Fields k) 2)
  (a : Fin (2 * k + 6)) (out : Fin 2 × Fin (2 * k + 6)) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredHermiteKernelTable.assemble
          fields).value
      a out =
    QuantumBlockEncoding.StoredHermiteKernelTable.blockView
      fields[↑out.1]
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv k) a)
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv k) out.2)

theorem QuantumBlockEncoding.StoredHermiteKernelTable.assemble_value
  {k : ℕ}
  (fields :
    Vector
      (QuantumBlockEncoding.StoredHermiteKernelTable.Fields
        k)
      2)
  (a : Fin (2 * k + 6))
  (out : Fin 2 × Fin (2 * k + 6)) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredHermiteKernelTable.assemble
          fields).value
      a out =
    QuantumBlockEncoding.StoredHermiteKernelTable.blockView
      fields[↑out.1]
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv
          k)
        a)
      ((QuantumBlockEncoding.HermiteExplicitBond.bondEquiv
          k)
        out.2)

Theorem10.63.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.63.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

theorem QuantumBlockEncoding.StoredHermiteKernelTable.storedBlock_cost_le
  {k : ℕ} (f : QuantumBlockEncoding.StoredHermiteKernelTable.Fields k)
  (a b :
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteKernelTable.storedBlock f a b).cost
      op ≤
    12

theorem QuantumBlockEncoding.StoredHermiteKernelTable.storedBlock_cost_le
  {k : ℕ}
  (f :
    QuantumBlockEncoding.StoredHermiteKernelTable.Fields
      k)
  (a b :
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteKernelTable.storedBlock
          f a b).cost
      op ≤
    12

Theorem10.63.11

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.63.11●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

theorem QuantumBlockEncoding.StoredHermiteKernelTable.entry_cost_le {k : ℕ}
  (fields :
    Vector (QuantumBlockEncoding.StoredHermiteKernelTable.Fields k) 2)
  (a : Fin (2 * k + 6)) (out : Fin 2 × Fin (2 * k + 6))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteKernelTable.entry fields a
          out).cost
      op ≤
    29

theorem QuantumBlockEncoding.StoredHermiteKernelTable.entry_cost_le
  {k : ℕ}
  (fields :
    Vector
      (QuantumBlockEncoding.StoredHermiteKernelTable.Fields
        k)
      2)
  (a : Fin (2 * k + 6))
  (out : Fin 2 × Fin (2 * k + 6))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteKernelTable.entry
          fields a out).cost
      op ≤
    29

Theorem10.63.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.63.12●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

theorem QuantumBlockEncoding.StoredHermiteKernelTable.assemble_cost_le {k : ℕ}
  (fields :
    Vector (QuantumBlockEncoding.StoredHermiteKernelTable.Fields k) 2)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteKernelTable.assemble fields).cost
      op ≤
    72 * (2 * k + 6) ^ 2

theorem QuantumBlockEncoding.StoredHermiteKernelTable.assemble_cost_le
  {k : ℕ}
  (fields :
    Vector
      (QuantumBlockEncoding.StoredHermiteKernelTable.Fields
        k)
      2)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteKernelTable.assemble
          fields).cost
      op ≤
    72 * (2 * k + 6) ^ 2

Theorem10.63.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.63.13●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

theorem QuantumBlockEncoding.StoredHermiteKernelTable.assemble_total_cost_le
  {k : ℕ}
  (fields :
    Vector (QuantumBlockEncoding.StoredHermiteKernelTable.Fields k) 2) :
  ∑ op,
      (QuantumBlockEncoding.StoredHermiteKernelTable.assemble
            fields).cost
        op ≤
    576 * (2 * k + 6) ^ 2

theorem QuantumBlockEncoding.StoredHermiteKernelTable.assemble_total_cost_le
  {k : ℕ}
  (fields :
    Vector
      (QuantumBlockEncoding.StoredHermiteKernelTable.Fields
        k)
      2) :
  ∑ op,
      (QuantumBlockEncoding.StoredHermiteKernelTable.assemble
            fields).cost
        op ≤
    576 * (2 * k + 6) ^ 2

Definition10.63.14

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “source correct”. A proposition-valued field is a requirement until a constructor supplies it. Explicit supplier obligations.

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

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

Technical source note. Explicit supplier obligations. Injections must ALREADY contain their Full guard, including zero on disabled children. No source callback is run.

Declaration kind. structure.

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

Lean code for Definition10.63.14●1 definition

structure(7 fields)defined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

structure QuantumBlockEncoding.StoredHermiteKernelTable.SourceCorrect (k n t : ℕ)
  (L : ℝ) (bit : Fin 2)
  (f : QuantumBlockEncoding.StoredHermiteKernelTable.Fields k) : Prop

structure QuantumBlockEncoding.StoredHermiteKernelTable.SourceCorrect
  (k n t : ℕ) (L : ℝ) (bit : Fin 2)
  (f :
    QuantumBlockEncoding.StoredHermiteKernelTable.Fields
      k) :
  Prop

Explicit supplier obligations. Injections must ALREADY contain their
Full guard, including zero on disabled children. No source callback is run.

Fields

leftPartial : f.leftPartial =
  decide
    (QuantumBlockEncoding.HermiteBoundaryInjection.Partial 0
      (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
        (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
          (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L))
        (n - t) (decide (bit = 1)))
      (2 ^ (n - t)))

leftInjection : f.leftInjection =
  if
      QuantumBlockEncoding.HermiteBoundaryInjection.Full 0 (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L)
        (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
          (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
            (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L))
          (n - t) (decide (bit = 1)))
        (2 ^ (n - t)) then
    QuantumBlockEncoding.HermiteBoundaryInjection.leftInject (-Real.pi * L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
        (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
          (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L))
        (n - t) (decide (bit = 1)))
      (n - t)
  else 0

leftFree : f.leftFree =
  QuantumBlockEncoding.HermiteBoundaryInjection.leftFree (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L)
    (n - t) (decide (bit = 1))

middlePartial : f.middlePartial =
  decide
    (QuantumBlockEncoding.HermiteBoundaryInjection.Partial (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L)
      (2 ^ n)
      (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
        (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
          (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L))
        (n - t) (decide (bit = 1)))
      (2 ^ (n - t)))

middleInjection : ∀ (j : Fin (2 * k + 1 + 1)),
  f.middleInjection[↑j] =
    if
        QuantumBlockEncoding.HermiteBoundaryInjection.Full (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L)
          (2 ^ n)
          (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
            (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
              (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L))
            (n - t) (decide (bit = 1)))
          (2 ^ (n - t)) then
      QuantumBlockEncoding.HermiteBoundaryInjection.blockInjectionRow k (-Real.pi * L)
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L)
        (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
          (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
            (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L))
          (n - t) (decide (bit = 1)))
        (n - t) j
    else 0

shared : ∀ (i j : Fin (2 * k + 1 + 1)),
  QuantumBlockEncoding.StoredGivens.denote f.shared i j =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore (2 * k + 1) (decide (bit = 1)) i j

rightCore : f.rightCore =
  QuantumBlockEncoding.HermiteBoundaryInjection.rightCore n (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L)
    (n - t) (decide (bit = 1))

Theorem10.63.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.63.15●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

theorem QuantumBlockEncoding.StoredHermiteKernelTable.blockView_source
  {k n t : ℕ} {L : ℝ} {bit : Fin 2}
  {f : QuantumBlockEncoding.StoredHermiteKernelTable.Fields k}
  (h :
    QuantumBlockEncoding.StoredHermiteKernelTable.SourceCorrect k n t L
      bit f)
  (a b :
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond k) :
  QuantumBlockEncoding.StoredHermiteKernelTable.blockView f a b =
    QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel k n L
      (n - t) (decide (bit = 1)) a b

theorem QuantumBlockEncoding.StoredHermiteKernelTable.blockView_source
  {k n t : ℕ} {L : ℝ} {bit : Fin 2}
  {f :
    QuantumBlockEncoding.StoredHermiteKernelTable.Fields
      k}
  (h :
    QuantumBlockEncoding.StoredHermiteKernelTable.SourceCorrect
      k n t L bit f)
  (a b :
    QuantumBlockEncoding.HermiteBoundaryInjection.HermiteFiniteBond
      k) :
  QuantumBlockEncoding.StoredHermiteKernelTable.blockView
      f a b =
    QuantumBlockEncoding.HermiteBoundaryInjection.hermiteKernel
      k n L (n - t) (decide (bit = 1)) a b

Theorem10.63.16

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “assemble source”; the hypotheses and conclusion in the code panel fix its exact scope. Strong entry refinement to the exact explicit layout kernel.

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. Strong entry refinement to the exact explicit layout kernel. Its seven field hypotheses are supplier obligations, not asserted source generation.

Declaration kind. theorem.

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

Lean code for Theorem10.63.16●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteKernelTable.lean

complete

theorem QuantumBlockEncoding.StoredHermiteKernelTable.assemble_source
  {k n t : ℕ} {L : ℝ}
  (fields :
    Vector (QuantumBlockEncoding.StoredHermiteKernelTable.Fields k) 2)
  (correct :
    ∀ (bit : Fin 2),
      QuantumBlockEncoding.StoredHermiteKernelTable.SourceCorrect k n t
        L bit fields[↑bit])
  (a : Fin (2 * k + 6)) (out : Fin 2 × Fin (2 * k + 6)) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredHermiteKernelTable.assemble
          fields).value
      a out =
    QuantumBlockEncoding.HermiteExplicitBond.kernel k n L t out.1 a
      out.2

theorem QuantumBlockEncoding.StoredHermiteKernelTable.assemble_source
  {k n t : ℕ} {L : ℝ}
  (fields :
    Vector
      (QuantumBlockEncoding.StoredHermiteKernelTable.Fields
        k)
      2)
  (correct :
    ∀ (bit : Fin 2),
      QuantumBlockEncoding.StoredHermiteKernelTable.SourceCorrect
        k n t L bit fields[↑bit])
  (a : Fin (2 * k + 6))
  (out : Fin 2 × Fin (2 * k + 6)) :
  QuantumBlockEncoding.StoredTensorTrain.denoteCore
      (QuantumBlockEncoding.StoredHermiteKernelTable.assemble
          fields).value
      a out =
    QuantumBlockEncoding.HermiteExplicitBond.kernel
      k n L t out.1 a out.2

Strong entry refinement to the exact explicit layout kernel. Its seven
field hypotheses are supplier obligations, not asserted source generation.