10.67. QuantumBlockEncoding/StoredHermiteSourceCache.lean🔗

22 explicit public declarations, in source order.

Definition10.67.1

uses 0used by 0✓L∃∀N

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

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. 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. structure.

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

Lean code for Definition10.67.1●1 definition

structure(6 fields)defined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

structure QuantumBlockEncoding.StoredHermiteSourceCache.Cache (k n : ℕ) : Type

structure QuantumBlockEncoding.StoredHermiteSourceCache.Cache
  (k n : ℕ) : Type

Fields

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

shared : QuantumBlockEncoding.StoredHermiteSharedTables.Tables (2 * k + 1)

tails : QuantumBlockEncoding.StoredHermiteGeometry.TailCache n

origin : ℝ

parents : Vector QuantumBlockEncoding.StoredBinaryCoordinates.Point (n + 1)

spans : Vector ℕ (n + 1)

Definition10.67.2

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “cache run”. A proposition-valued field is a requirement until a constructor supplies it. SourceRun's ordinary and exponential fields are inherited unchanged.

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. SourceRun's ordinary and exponential fields are inherited unchanged. The additional counters describe only selected integer supplier operations.

Declaration kind. structure.

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

structure(extends 1, 5 fields)defined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

structure QuantumBlockEncoding.StoredHermiteSourceCache.CacheRun (α : Type) : Type

structure QuantumBlockEncoding.StoredHermiteSourceCache.CacheRun
  (α : Type) : Type

SourceRun's ordinary and exponential fields are inherited unchanged.
The additional counters describe only selected integer supplier operations.

Extends

QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun α

Fields

run : QuantumBlockEncoding.StoredGivens.Run α

Inherited from

QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun

exponentialCalls : ℕ

Inherited from

QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun

quotientCalls : ℕ

remainderCalls : ℕ

integerDoublings : ℕ

Definition10.67.3

uses 0used by 0✓L∃∀N

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

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. 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. structure.

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

Lean code for Definition10.67.3●1 definition

structure(3 fields)defined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

structure QuantumBlockEncoding.StoredHermiteSourceCache.Inputs : Type

structure QuantumBlockEncoding.StoredHermiteSourceCache.Inputs :
  Type

Fields

origin : ℝ

grid : ℝ

cutoff : ℕ

Definition10.67.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “inputs”. Reuse the actual root-level tail width, never recompute pi*L or cast an integer address.

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. Reuse the actual root-level tail width, never recompute pi*L or cast an integer address. Root/table and numeric payload reads are separately charged.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

def QuantumBlockEncoding.StoredHermiteSourceCache.inputs {n : ℕ}
  (tail : QuantumBlockEncoding.StoredHermiteGeometry.TailCache n) :
  QuantumBlockEncoding.StoredGivens.Run
    QuantumBlockEncoding.StoredHermiteSourceCache.Inputs

def QuantumBlockEncoding.StoredHermiteSourceCache.inputs
  {n : ℕ}
  (tail :
    QuantumBlockEncoding.StoredHermiteGeometry.TailCache
      n) :
  QuantumBlockEncoding.StoredGivens.Run
    QuantumBlockEncoding.StoredHermiteSourceCache.Inputs

Reuse the actual root-level tail width, never recompute pi*L or cast an
integer address. Root/table and numeric payload reads are separately charged.

Theorem10.67.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.5●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.inputs_value (n : ℕ)
  (L : ℝ) (hL : 0 < L) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.inputs
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                  L).run.value).value.origin =
      -Real.pi * L ∧
    (QuantumBlockEncoding.StoredHermiteSourceCache.inputs
              (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                    L).run.value).value.grid =
        QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L ∧
      (QuantumBlockEncoding.StoredHermiteSourceCache.inputs
              (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                    L).run.value).value.cutoff =
        QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L

theorem QuantumBlockEncoding.StoredHermiteSourceCache.inputs_value
  (n : ℕ) (L : ℝ) (hL : 0 < L) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.inputs
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                  n
                  L).run.value).value.origin =
      -Real.pi * L ∧
    (QuantumBlockEncoding.StoredHermiteSourceCache.inputs
              (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                    n
                    L).run.value).value.grid =
        QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
          n L ∧
      (QuantumBlockEncoding.StoredHermiteSourceCache.inputs
              (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                    n
                    L).run.value).value.cutoff =
        QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
          n L

Theorem10.67.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.6●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.inputs_cost {n : ℕ}
  (tail : QuantumBlockEncoding.StoredHermiteGeometry.TailCache n)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.inputs tail).cost op =
    4 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.read op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field op

theorem QuantumBlockEncoding.StoredHermiteSourceCache.inputs_cost
  {n : ℕ}
  (tail :
    QuantumBlockEncoding.StoredHermiteGeometry.TailCache
      n)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.inputs
          tail).cost
      op =
    4 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.read
          op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field
        op

Definition10.67.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “store cache”. Explicit fixed-size record materialization; arrays and tables are already stored and are preserved by reference rather than regenerated.

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. Explicit fixed-size record materialization; arrays and tables are already stored and are preserved by reference rather than regenerated.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

def QuantumBlockEncoding.StoredHermiteSourceCache.storeCache {k n : ℕ}
  (source : Vector ℝ (2 * k + 1 + 1))
  (shared :
    QuantumBlockEncoding.StoredHermiteSharedTables.Tables (2 * k + 1))
  (tails : QuantumBlockEncoding.StoredHermiteGeometry.TailCache n)
  (origin : ℝ)
  (parents :
    Vector QuantumBlockEncoding.StoredBinaryCoordinates.Point (n + 1))
  (spans : Vector ℕ (n + 1)) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n)

def QuantumBlockEncoding.StoredHermiteSourceCache.storeCache
  {k n : ℕ}
  (source : Vector ℝ (2 * k + 1 + 1))
  (shared :
    QuantumBlockEncoding.StoredHermiteSharedTables.Tables
      (2 * k + 1))
  (tails :
    QuantumBlockEncoding.StoredHermiteGeometry.TailCache
      n)
  (origin : ℝ)
  (parents :
    Vector
      QuantumBlockEncoding.StoredBinaryCoordinates.Point
      (n + 1))
  (spans : Vector ℕ (n + 1)) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n)

Explicit fixed-size record materialization; arrays and tables are already
stored and are preserved by reference rather than regenerated.

Definition10.67.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile”. Actual deterministic source cache, with no hypothetical supplier input.

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 deterministic source cache, with no hypothetical supplier input.

Declaration kind. def.

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

Lean code for Definition10.67.8●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

def QuantumBlockEncoding.StoredHermiteSourceCache.compile (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.StoredHermiteSourceCache.CacheRun
    (QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n)

def QuantumBlockEncoding.StoredHermiteSourceCache.compile
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredHermiteSourceCache.CacheRun
    (QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n)

Actual deterministic source cache, with no hypothetical supplier input.

Theorem10.67.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.9●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_source (k n : ℕ)
  (L : ℝ) (i : Fin (2 * k + 1 + 1)) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
              L).run.value.source[↑i] =
    QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient k
      ↑i

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_source
  (k n : ℕ) (L : ℝ)
  (i : Fin (2 * k + 1 + 1)) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile
              k n
              L).run.value.source[↑i] =
    QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
      k ↑i

Theorem10.67.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_shared_false
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                L).run.value.shared.falseTable =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore (2 * k + 1)
      false

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_shared_false
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                k n
                L).run.value.shared.falseTable =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore
      (2 * k + 1) false

Theorem10.67.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile shared true”; 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/StoredHermiteSourceCache.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.67.11●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_shared_true
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                L).run.value.shared.trueTable =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore (2 * k + 1)
      true

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_shared_true
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                k n
                L).run.value.shared.trueTable =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore
      (2 * k + 1) true

Theorem10.67.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.12●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_tails (k n : ℕ)
  (L : ℝ) (hL : 0 < L) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                L).run.value.tails.cutoff =
      QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L ∧
    (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                  L).run.value.tails.grid =
        QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L ∧
      ∀ (r : Fin (n + 1)),
        (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                          L).run.value.tails.levels[↑r].width =
            QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L *
              2 ^ ↑r ∧
          (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                          L).run.value.tails.levels[↑r].factor =
            Real.exp
              (-QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n
                    L *
                2 ^ ↑r)

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_tails
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                k n
                L).run.value.tails.cutoff =
      QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
        n L ∧
    (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                  k n
                  L).run.value.tails.grid =
        QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
          n L ∧
      ∀ (r : Fin (n + 1)),
        (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                          k n
                          L).run.value.tails.levels[↑r].width =
            QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
                n L *
              2 ^ ↑r ∧
          (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                          k n
                          L).run.value.tails.levels[↑r].factor =
            Real.exp
              (-QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
                    n L *
                2 ^ ↑r)

Theorem10.67.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.13●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_origin (k n : ℕ)
  (L : ℝ) (hL : 0 < L) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
            L).run.value.origin =
    -Real.pi * L

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_origin
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile
            k n L).run.value.origin =
    -Real.pi * L

Theorem10.67.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.14●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_parents_first
  (k n : ℕ) (L : ℝ) (hL : 0 < L) (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                L).run.value.parents[↑t].first =
    QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
      (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L)
      (n - ↑t + 1)

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_parents_first
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                k n
                L).run.value.parents[↑t].first =
    QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
      (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
        n L)
      (n - ↑t + 1)

Theorem10.67.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.15●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_parents_lower
  (k n : ℕ) (L : ℝ) (hL : 0 < L) (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                L).run.value.parents[↑t].lower =
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
      (-Real.pi * L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
        (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L)
        (n - ↑t + 1))

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_parents_lower
  (k n : ℕ) (L : ℝ) (hL : 0 < L)
  (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                k n
                L).run.value.parents[↑t].lower =
    QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
      (-Real.pi * L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
        n L)
      (QuantumBlockEncoding.HermiteBoundaryInjection.boundarySchedule
        (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
          n L)
        (n - ↑t + 1))

Theorem10.67.16

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.16●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_spans (k n : ℕ)
  (L : ℝ) (r : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
              L).run.value.spans[↑r] =
    2 ^ ↑r

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_spans
  (k n : ℕ) (L : ℝ) (r : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile
              k n L).run.value.spans[↑r] =
    2 ^ ↑r

Theorem10.67.17

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.17●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_exponentialCalls
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
        L).exponentialCalls =
    n + 2

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_exponentialCalls
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile
        k n L).exponentialCalls =
    n + 2

Theorem10.67.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile quotient calls”; the hypotheses and conclusion in the code panel fix its exact scope. These are the selected calls in the exact parent run stored in compile.

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. These are the selected calls in the exact parent run stored in compile.

Declaration kind. theorem.

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

Lean code for Theorem10.67.18●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_quotientCalls
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
        L).quotientCalls =
    (n + 1) * (n + 2)

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_quotientCalls
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile
        k n L).quotientCalls =
    (n + 1) * (n + 2)

These are the selected calls in the exact parent run stored in compile.

Theorem10.67.19

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.19●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_remainderCalls
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
        L).remainderCalls =
    (n + 1) ^ 2

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_remainderCalls
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile
        k n L).remainderCalls =
    (n + 1) ^ 2

Theorem10.67.20

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.20●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_integerDoublings
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
        L).integerDoublings =
    n

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_integerDoublings
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile
        k n L).integerDoublings =
    n

Theorem10.67.21

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.21●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_cost_le (k n : ℕ)
  (L : ℝ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n L).run.cost
      op ≤
    400 * (k + 1) ^ 2 + 32 * (n + 1) ^ 2

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_cost_le
  (k n : ℕ) (L : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSourceCache.compile
            k n L).run.cost
      op ≤
    400 * (k + 1) ^ 2 + 32 * (n + 1) ^ 2

Theorem10.67.22

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.67.22●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteSourceCache.lean

complete

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_total_cost_le
  (k n : ℕ) (L : ℝ) :
  ∑ op,
      (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
              L).run.cost
        op ≤
    3200 * (k + 1) ^ 2 + 256 * (n + 1) ^ 2

theorem QuantumBlockEncoding.StoredHermiteSourceCache.compile_total_cost_le
  (k n : ℕ) (L : ℝ) :
  ∑ op,
      (QuantumBlockEncoding.StoredHermiteSourceCache.compile
              k n L).run.cost
        op ≤
    3200 * (k + 1) ^ 2 + 256 * (n + 1) ^ 2