10.64. QuantumBlockEncoding/StoredHermiteRawCost.lean🔗

31 explicit public declarations, in source order.

Definition10.64.1

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.64.1●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

def QuantumBlockEncoding.StoredHermiteRawCost.ordinary
  (cost : QuantumBlockEncoding.StoredGivens.Cost) : ℕ

def QuantumBlockEncoding.StoredHermiteRawCost.ordinary
  (cost :
    QuantumBlockEncoding.StoredGivens.Cost) :
  ℕ

Theorem10.64.2

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “ordinary eq total”; the hypotheses and conclusion in the code panel fix its exact scope. Eight-operation enumeration adapter; no producer or counter is altered.

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. Eight-operation enumeration adapter; no producer or counter is altered.

Declaration kind. theorem.

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

Lean code for Theorem10.64.2●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.ordinary_eq_total
  (cost : QuantumBlockEncoding.StoredGivens.Cost) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary cost =
    QuantumBlockEncoding.StoredRectangularGivens.total cost

theorem QuantumBlockEncoding.StoredHermiteRawCost.ordinary_eq_total
  (cost :
    QuantumBlockEncoding.StoredGivens.Cost) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      cost =
    QuantumBlockEncoding.StoredRectangularGivens.total
      cost

Eight-operation enumeration adapter; no producer or counter is altered.

Theorem10.64.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.3●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.ordinary_add
  (a b : QuantumBlockEncoding.StoredGivens.Cost) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary (a + b) =
    QuantumBlockEncoding.StoredHermiteRawCost.ordinary a +
      QuantumBlockEncoding.StoredHermiteRawCost.ordinary b

theorem QuantumBlockEncoding.StoredHermiteRawCost.ordinary_add
  (a b :
    QuantumBlockEncoding.StoredGivens.Cost) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (a + b) =
    QuantumBlockEncoding.StoredHermiteRawCost.ordinary
        a +
      QuantumBlockEncoding.StoredHermiteRawCost.ordinary
        b

Theorem10.64.4

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.4●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.ordinary_zero :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary 0 = 0

theorem QuantumBlockEncoding.StoredHermiteRawCost.ordinary_zero :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      0 =
    0

Theorem10.64.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.5●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.ordinary_tick
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredGivens.tick op) =
    1

theorem QuantumBlockEncoding.StoredHermiteRawCost.ordinary_tick
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredGivens.tick
        op) =
    1

Definition10.64.6

uses 0used by 0✓L∃∀N

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

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/StoredHermiteRawCost.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.64.6●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

def QuantumBlockEncoding.StoredHermiteRawCost.stageBudget (k : ℕ) : ℕ

def QuantumBlockEncoding.StoredHermiteRawCost.stageBudget
  (k : ℕ) : ℕ

Theorem10.64.7

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.7●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.stage_total_cost_le {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n)
  (t : Fin (n + 1)) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredHermiteRawSource.stage cache
            t).run.cost ≤
    QuantumBlockEncoding.StoredHermiteRawCost.stageBudget k

theorem QuantumBlockEncoding.StoredHermiteRawCost.stage_total_cost_le
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n)
  (t : Fin (n + 1)) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredHermiteRawSource.stage
            cache t).run.cost ≤
    QuantumBlockEncoding.StoredHermiteRawCost.stageBudget
      k

Theorem10.64.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.8●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.stage_exponentialCalls
  {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n)
  (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteRawSource.stage cache
        t).exponentialCalls =
    ∑ bit,
      if
          (QuantumBlockEncoding.StoredHermiteStageInput.input cache
                        t).run.value.children[↑bit].leftFull =
            true then
        1
      else 0

theorem QuantumBlockEncoding.StoredHermiteRawCost.stage_exponentialCalls
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n)
  (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteRawSource.stage
        cache t).exponentialCalls =
    ∑ bit,
      if
          (QuantumBlockEncoding.StoredHermiteStageInput.input
                        cache
                        t).run.value.children[↑bit].leftFull =
            true then
        1
      else 0

Theorem10.64.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.9●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.stage_exponentialCalls_le
  {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n)
  (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteRawSource.stage cache
        t).exponentialCalls ≤
    2

theorem QuantumBlockEncoding.StoredHermiteRawCost.stage_exponentialCalls_le
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n)
  (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteRawSource.stage
        cache t).exponentialCalls ≤
    2

Theorem10.64.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.stage_integerAdditions
  {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n)
  (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteRawSource.stage cache
        t).integerAdditions =
    4

theorem QuantumBlockEncoding.StoredHermiteRawCost.stage_integerAdditions
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n)
  (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteRawSource.stage
        cache t).integerAdditions =
    4

Theorem10.64.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “collect stages cost”; the hypotheses and conclusion in the code panel fix its exact scope. The ledger table is materialized once.

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 ledger table is materialized once. Its projection adds exactly three reads and three writes per stage, including its initial stored record.

Declaration kind. theorem.

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

Lean code for Theorem10.64.11●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.collectStages_cost {α : Type}
  {m : ℕ}
  (f : Fin m → QuantumBlockEncoding.StoredHermiteRawSource.StageRun α)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteRawSource.collectStages f).run.cost
      op =
    ∑ i, (f i).run.cost op +
      m *
        (3 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read op +
          3 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write op)

theorem QuantumBlockEncoding.StoredHermiteRawCost.collectStages_cost
  {α : Type} {m : ℕ}
  (f :
    Fin m →
      QuantumBlockEncoding.StoredHermiteRawSource.StageRun
        α)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteRawSource.collectStages
            f).run.cost
      op =
    ∑ i, (f i).run.cost op +
      m *
        (3 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.read
              op +
          3 *
            QuantumBlockEncoding.StoredGivens.tick
              QuantumBlockEncoding.StoredGivens.Op.write
              op)

The ledger table is materialized once. Its projection adds exactly three
reads and three writes per stage, including its initial stored record.

Theorem10.64.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.12●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.collectStages_total_cost
  {α : Type} {m : ℕ}
  (f : Fin m → QuantumBlockEncoding.StoredHermiteRawSource.StageRun α) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredHermiteRawSource.collectStages
            f).run.cost =
    ∑ i,
        QuantumBlockEncoding.StoredHermiteRawCost.ordinary
          (f i).run.cost +
      6 * m

theorem QuantumBlockEncoding.StoredHermiteRawCost.collectStages_total_cost
  {α : Type} {m : ℕ}
  (f :
    Fin m →
      QuantumBlockEncoding.StoredHermiteRawSource.StageRun
        α) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredHermiteRawSource.collectStages
            f).run.cost =
    ∑ i,
        QuantumBlockEncoding.StoredHermiteRawCost.ordinary
          (f i).run.cost +
      6 * m

Theorem10.64.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “collect stages 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/StoredHermiteRawCost.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.64.13●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.collectStages_exponentialCalls
  {α : Type} {m : ℕ}
  (f : Fin m → QuantumBlockEncoding.StoredHermiteRawSource.StageRun α) :
  (QuantumBlockEncoding.StoredHermiteRawSource.collectStages
        f).exponentialCalls =
    ∑ i, (f i).exponentialCalls

theorem QuantumBlockEncoding.StoredHermiteRawCost.collectStages_exponentialCalls
  {α : Type} {m : ℕ}
  (f :
    Fin m →
      QuantumBlockEncoding.StoredHermiteRawSource.StageRun
        α) :
  (QuantumBlockEncoding.StoredHermiteRawSource.collectStages
        f).exponentialCalls =
    ∑ i, (f i).exponentialCalls

Theorem10.64.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.14●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.collectStages_integerAdditions
  {α : Type} {m : ℕ}
  (f : Fin m → QuantumBlockEncoding.StoredHermiteRawSource.StageRun α) :
  (QuantumBlockEncoding.StoredHermiteRawSource.collectStages
        f).integerAdditions =
    ∑ i, (f i).integerAdditions

theorem QuantumBlockEncoding.StoredHermiteRawCost.collectStages_integerAdditions
  {α : Type} {m : ℕ}
  (f :
    Fin m →
      QuantumBlockEncoding.StoredHermiteRawSource.StageRun
        α) :
  (QuantumBlockEncoding.StoredHermiteRawSource.collectStages
        f).integerAdditions =
    ∑ i, (f i).integerAdditions

Theorem10.64.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.15●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.tables_total_cost_le {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredHermiteRawSource.tables
            cache).run.cost ≤
    (n + 1) *
      (QuantumBlockEncoding.StoredHermiteRawCost.stageBudget k + 6)

theorem QuantumBlockEncoding.StoredHermiteRawCost.tables_total_cost_le
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredHermiteRawSource.tables
            cache).run.cost ≤
    (n + 1) *
      (QuantumBlockEncoding.StoredHermiteRawCost.stageBudget
          k +
        6)

Theorem10.64.16

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.16●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.tables_exponentialCalls_le
  {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n) :
  (QuantumBlockEncoding.StoredHermiteRawSource.tables
        cache).exponentialCalls ≤
    2 * (n + 1)

theorem QuantumBlockEncoding.StoredHermiteRawCost.tables_exponentialCalls_le
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n) :
  (QuantumBlockEncoding.StoredHermiteRawSource.tables
        cache).exponentialCalls ≤
    2 * (n + 1)

Theorem10.64.17

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tables integer additions”; 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/StoredHermiteRawCost.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.64.17●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.tables_integerAdditions
  {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n) :
  (QuantumBlockEncoding.StoredHermiteRawSource.tables
        cache).integerAdditions =
    4 * (n + 1)

theorem QuantumBlockEncoding.StoredHermiteRawCost.tables_integerAdditions
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n) :
  (QuantumBlockEncoding.StoredHermiteRawSource.tables
        cache).integerAdditions =
    4 * (n + 1)

Theorem10.64.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “boundary 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/StoredHermiteRawCost.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.64.18●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.boundaryInputs_cost {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteRawSource.boundaryInputs
          cache).cost
      op =
    4 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.read op

theorem QuantumBlockEncoding.StoredHermiteRawCost.boundaryInputs_cost
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteRawSource.boundaryInputs
          cache).cost
      op =
    4 *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.read
        op

Theorem10.64.19

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.19●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.boundaries_total_cost
  {k n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteSourceCache.Cache k n) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredHermiteRawSource.boundaries
          cache).cost =
    32 * (2 * k + 6) + 6

theorem QuantumBlockEncoding.StoredHermiteRawCost.boundaries_total_cost
  {k n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteSourceCache.Cache
      k n) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredHermiteRawSource.boundaries
          cache).cost =
    32 * (2 * k + 6) + 6

Definition10.64.20

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.64.20●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

def QuantumBlockEncoding.StoredHermiteRawCost.rawBudget (k n : ℕ) : ℕ

def QuantumBlockEncoding.StoredHermiteRawCost.rawBudget
  (k n : ℕ) : ℕ

Theorem10.64.21

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “raw total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Every summand is a proved cost of a subrun actually used by raw.

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 summand is a proved cost of a subrun actually used by raw. No dimension-only or hypothetical source-entry budget is substituted.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_total_cost_le (k n : ℕ)
  (L : ℝ) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredHermiteRawSource.raw k n L).run.cost ≤
    QuantumBlockEncoding.StoredHermiteRawCost.rawBudget k n

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_total_cost_le
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredHermiteRawCost.ordinary
      (QuantumBlockEncoding.StoredHermiteRawSource.raw
            k n L).run.cost ≤
    QuantumBlockEncoding.StoredHermiteRawCost.rawBudget
      k n

Every summand is a proved cost of a subrun actually used by raw. No
dimension-only or hypothetical source-entry budget is substituted.

Theorem10.64.22

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.22●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_stored_total_cost_le
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteRawSource.raw k n L).run.cost ≤
    QuantumBlockEncoding.StoredHermiteRawCost.rawBudget k n

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_stored_total_cost_le
  (k n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteRawSource.raw
            k n L).run.cost ≤
    QuantumBlockEncoding.StoredHermiteRawCost.rawBudget
      k n

Theorem10.64.23

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.23●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_cost_le (k n : ℕ) (L : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw k n L).run.cost op ≤
    QuantumBlockEncoding.StoredHermiteRawCost.rawBudget k n

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_cost_le
  (k n : ℕ) (L : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw
            k n L).run.cost
      op ≤
    QuantumBlockEncoding.StoredHermiteRawCost.rawBudget
      k n

Theorem10.64.24

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “raw exponential calls”; the hypotheses and conclusion in the code panel fix its exact scope. Exact exponential ledger: one coefficient call, n+1 cached tail calls, and the actual stage injection calls (zero on disabled Full guards).

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 exponential ledger: one coefficient call, n+1 cached tail calls, and the actual stage injection calls (zero on disabled Full guards).

Declaration kind. theorem.

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

Lean code for Theorem10.64.24●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_exponentialCalls (k n : ℕ)
  (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
        L).exponentialCalls =
    n + 2 +
      ∑ t,
        (QuantumBlockEncoding.StoredHermiteRawSource.stage
            (QuantumBlockEncoding.StoredHermiteSourceCache.compile k n
                  L).run.value
            t).exponentialCalls

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_exponentialCalls
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw
        k n L).exponentialCalls =
    n + 2 +
      ∑ t,
        (QuantumBlockEncoding.StoredHermiteRawSource.stage
            (QuantumBlockEncoding.StoredHermiteSourceCache.compile
                  k n L).run.value
            t).exponentialCalls

Exact exponential ledger: one coefficient call, n+1 cached tail calls,
and the actual stage injection calls (zero on disabled Full guards).

Theorem10.64.25

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.25●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_exponentialCalls_le
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
        L).exponentialCalls ≤
    3 * (n + 1) + 1

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_exponentialCalls_le
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw
        k n L).exponentialCalls ≤
    3 * (n + 1) + 1

Theorem10.64.26

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.26●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_quotientCalls (k n : ℕ)
  (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
        L).quotientCalls =
    (n + 1) * (n + 2)

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_quotientCalls
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw
        k n L).quotientCalls =
    (n + 1) * (n + 2)

Theorem10.64.27

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.27●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_remainderCalls (k n : ℕ)
  (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
        L).remainderCalls =
    (n + 1) ^ 2

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_remainderCalls
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw
        k n L).remainderCalls =
    (n + 1) ^ 2

Theorem10.64.28

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.28●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_integerDoublings (k n : ℕ)
  (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
        L).integerDoublings =
    n

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_integerDoublings
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw
        k n L).integerDoublings =
    n

Theorem10.64.29

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.64.29●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_integerAdditions (k n : ℕ)
  (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
        L).integerAdditions =
    4 * (n + 1)

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_integerAdditions
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw
        k n L).integerAdditions =
    4 * (n + 1)

Theorem10.64.30

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “raw selected integer total”; the hypotheses and conclusion in the code panel fix its exact scope. Sum of precisely the four named integer counters, not all integer work.

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. Sum of precisely the four named integer counters, not all integer work.

Declaration kind. theorem.

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

Lean code for Theorem10.64.30●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_selected_integer_total
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
              L).quotientCalls +
          (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
              L).remainderCalls +
        (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
            L).integerDoublings +
      (QuantumBlockEncoding.StoredHermiteRawSource.raw k n
          L).integerAdditions =
    2 * n ^ 2 + 10 * n + 7

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_selected_integer_total
  (k n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteRawSource.raw
              k n L).quotientCalls +
          (QuantumBlockEncoding.StoredHermiteRawSource.raw
              k n L).remainderCalls +
        (QuantumBlockEncoding.StoredHermiteRawSource.raw
            k n L).integerDoublings +
      (QuantumBlockEncoding.StoredHermiteRawSource.raw
          k n L).integerAdditions =
    2 * n ^ 2 + 10 * n + 7

Sum of precisely the four named integer counters, not all integer work.

Theorem10.64.31

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “raw certified”; the hypotheses and conclusion in the code panel fix its exact scope. Same-run source equality, polynomial ordinary work, exponential cap, and the four accurately scoped integer counters.

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. Same-run source equality, polynomial ordinary work, exponential cap, and the four accurately scoped integer counters. This is an unnormalized source.

Declaration kind. theorem.

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

Lean code for Theorem10.64.31●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteRawCost.lean

complete

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_certified (k n : ℕ)
  (L : ℝ) (hL : 0 < L) :
  have result := QuantumBlockEncoding.StoredHermiteRawSource.raw k n L;
  QuantumBlockEncoding.StoredTensorTrain.denoteChain result.run.value =
      QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain k n L ∧
    QuantumBlockEncoding.StoredHermiteRawCost.ordinary result.run.cost ≤
        QuantumBlockEncoding.StoredHermiteRawCost.rawBudget k n ∧
      result.exponentialCalls ≤ 3 * (n + 1) + 1 ∧
        result.quotientCalls = (n + 1) * (n + 2) ∧
          result.remainderCalls = (n + 1) ^ 2 ∧
            result.integerDoublings = n ∧
              result.integerAdditions = 4 * (n + 1)

theorem QuantumBlockEncoding.StoredHermiteRawCost.raw_certified
  (k n : ℕ) (L : ℝ) (hL : 0 < L) :
  have result :=
    QuantumBlockEncoding.StoredHermiteRawSource.raw
      k n L;
  QuantumBlockEncoding.StoredTensorTrain.denoteChain
        result.run.value =
      QuantumBlockEncoding.HermiteExplicitBond.rawSourceChain
        k n L ∧
    QuantumBlockEncoding.StoredHermiteRawCost.ordinary
          result.run.cost ≤
        QuantumBlockEncoding.StoredHermiteRawCost.rawBudget
          k n ∧
      result.exponentialCalls ≤
          3 * (n + 1) + 1 ∧
        result.quotientCalls =
            (n + 1) * (n + 2) ∧
          result.remainderCalls =
              (n + 1) ^ 2 ∧
            result.integerDoublings = n ∧
              result.integerAdditions =
                4 * (n + 1)

Same-run source equality, polynomial ordinary work, exponential cap, and
the four accurately scoped integer counters. This is an unnormalized source.