10.61. QuantumBlockEncoding/StoredHermiteCoefficients.lean🔗

38 explicit public declarations, in source order.

Definition10.61.1

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “factorial table”. 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/StoredHermiteCoefficients.lean:26. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.61.1●1 definition

structure(2 fields)defined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

structure QuantumBlockEncoding.StoredHermiteCoefficients.FactorialTable (n : ℕ) :
  Type

structure QuantumBlockEncoding.StoredHermiteCoefficients.FactorialTable
  (n : ℕ) : Type

Fields

values : Vector ℝ (n + 1)

next : ℝ

Definition10.61.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “extend”. Full-copy table extension, including one index comparison per output.

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

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

Technical source note. Full-copy table extension, including one index comparison per output.

Declaration kind. def.

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

Lean code for Definition10.61.2●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

def QuantumBlockEncoding.StoredHermiteCoefficients.extend {n : ℕ}
  (xs : Vector ℝ (n + 1)) (last : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (n + 2))

def QuantumBlockEncoding.StoredHermiteCoefficients.extend
  {n : ℕ} (xs : Vector ℝ (n + 1))
  (last : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (n + 2))

Full-copy table extension, including one index comparison per output.

Theorem10.61.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “extend 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/StoredHermiteCoefficients.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.61.3●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.extend_value {n : ℕ}
  (xs : Vector ℝ (n + 1)) (last : ℝ) (i : Fin (n + 2)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.extend xs
          last).value[↑i] =
    if h : ↑i < n + 1 then xs[↑i] else last

theorem QuantumBlockEncoding.StoredHermiteCoefficients.extend_value
  {n : ℕ} (xs : Vector ℝ (n + 1))
  (last : ℝ) (i : Fin (n + 2)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.extend
          xs last).value[↑i] =
    if h : ↑i < n + 1 then xs[↑i]
    else last

Definition10.61.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “factorials”. The next integer multiplier is itself generated by a charged addition.

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 next integer multiplier is itself generated by a charged addition.

Declaration kind. def.

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

Lean code for Definition10.61.4●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

def QuantumBlockEncoding.StoredHermiteCoefficients.factorials (n : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredHermiteCoefficients.FactorialTable n)

def QuantumBlockEncoding.StoredHermiteCoefficients.factorials
  (n : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredHermiteCoefficients.FactorialTable
      n)

The next integer multiplier is itself generated by a charged addition.

Theorem10.61.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.5●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.factorials_next (n : ℕ) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.factorials
          n).value.next =
    ↑(n + 1)

theorem QuantumBlockEncoding.StoredHermiteCoefficients.factorials_next
  (n : ℕ) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.factorials
          n).value.next =
    ↑(n + 1)

Theorem10.61.6

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “factorials 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/StoredHermiteCoefficients.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.61.6●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.factorials_value (n : ℕ)
  (i : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.factorials
            n).value.values[↑i] =
    ↑(↑i).factorial

theorem QuantumBlockEncoding.StoredHermiteCoefficients.factorials_value
  (n : ℕ) (i : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.factorials
            n).value.values[↑i] =
    ↑(↑i).factorial

Definition10.61.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “choose from”. 'choose' uses three cached factorial entries and two field operations.

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. 'choose' uses three cached factorial entries and two field operations.

Declaration kind. def.

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

Lean code for Definition10.61.7●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

def QuantumBlockEncoding.StoredHermiteCoefficients.chooseFrom {N : ℕ}
  (F : Vector ℝ (N + 1)) (n r : ℕ) (hr : r ≤ n) (hn : n ≤ N) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredHermiteCoefficients.chooseFrom
  {N : ℕ} (F : Vector ℝ (N + 1)) (n r : ℕ)
  (hr : r ≤ n) (hn : n ≤ N) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

`choose` uses three cached factorial entries and two field operations.

Theorem10.61.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “choose from 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/StoredHermiteCoefficients.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.61.8●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.chooseFrom_value {N : ℕ}
  (F : Vector ℝ (N + 1))
  (correct : ∀ (i : Fin (N + 1)), F[↑i] = ↑(↑i).factorial) (n r : ℕ)
  (hr : r ≤ n) (hn : n ≤ N) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.chooseFrom F n r hr
        hn).value =
    ↑(n.choose r)

theorem QuantumBlockEncoding.StoredHermiteCoefficients.chooseFrom_value
  {N : ℕ} (F : Vector ℝ (N + 1))
  (correct :
    ∀ (i : Fin (N + 1)),
      F[↑i] = ↑(↑i).factorial)
  (n r : ℕ) (hr : r ≤ n) (hn : n ≤ N) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.chooseFrom
        F n r hr hn).value =
    ↑(n.choose r)

Definition10.61.9

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.61.9●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

def QuantumBlockEncoding.StoredHermiteCoefficients.sourceEntry (k : ℕ)
  (F : Vector ℝ (2 * k + 2)) (i : Fin (k + 1)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredHermiteCoefficients.sourceEntry
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (i : Fin (k + 1)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Theorem10.61.10

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.10●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.sourceEntry_value (k : ℕ)
  (F : Vector ℝ (2 * k + 2))
  (correct : ∀ (i : Fin (2 * k + 2)), F[↑i] = ↑(↑i).factorial)
  (i : Fin (k + 1)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.sourceEntry k F
        i).value =
    QuantumBlockEncoding.HermiteBernstein.sourceCoefficient k ↑i

theorem QuantumBlockEncoding.StoredHermiteCoefficients.sourceEntry_value
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (correct :
    ∀ (i : Fin (2 * k + 2)),
      F[↑i] = ↑(↑i).factorial)
  (i : Fin (k + 1)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.sourceEntry
        k F i).value =
    QuantumBlockEncoding.HermiteBernstein.sourceCoefficient
      k ↑i

Definition10.61.11

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.61.11●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

def QuantumBlockEncoding.StoredHermiteCoefficients.sources (k : ℕ)
  (F : Vector ℝ (2 * k + 2)) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (k + 1))

def QuantumBlockEncoding.StoredHermiteCoefficients.sources
  (k : ℕ) (F : Vector ℝ (2 * k + 2)) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (k + 1))

Theorem10.61.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “sources 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/StoredHermiteCoefficients.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.61.12●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.sources_value (k : ℕ)
  (F : Vector ℝ (2 * k + 2))
  (correct : ∀ (i : Fin (2 * k + 2)), F[↑i] = ↑(↑i).factorial)
  (i : Fin (k + 1)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.sources k
          F).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.sourceCoefficient k ↑i

theorem QuantumBlockEncoding.StoredHermiteCoefficients.sources_value
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (correct :
    ∀ (i : Fin (2 * k + 2)),
      F[↑i] = ↑(↑i).factorial)
  (i : Fin (k + 1)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.sources
          k F).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.sourceCoefficient
      k ↑i

Definition10.61.13

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.61.13●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

def QuantumBlockEncoding.StoredHermiteCoefficients.leftTerm (k : ℕ)
  (F : Vector ℝ (2 * k + 2)) (a : Vector ℝ (k + 1)) (denominator : ℝ)
  (r : Fin (2 * k + 2)) (i : Fin (k + 1)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredHermiteCoefficients.leftTerm
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (a : Vector ℝ (k + 1)) (denominator : ℝ)
  (r : Fin (2 * k + 2))
  (i : Fin (k + 1)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Definition10.61.14

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.61.14●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

def QuantumBlockEncoding.StoredHermiteCoefficients.leftEntry (k : ℕ)
  (F : Vector ℝ (2 * k + 2)) (a : Vector ℝ (k + 1))
  (r : Fin (2 * k + 2)) : QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredHermiteCoefficients.leftEntry
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (a : Vector ℝ (k + 1))
  (r : Fin (2 * k + 2)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Theorem10.61.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “left 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/StoredHermiteCoefficients.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.61.15●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.leftEntry_value (k : ℕ)
  (F : Vector ℝ (2 * k + 2))
  (hF : ∀ (i : Fin (2 * k + 2)), F[↑i] = ↑(↑i).factorial)
  (a : Vector ℝ (k + 1))
  (ha :
    ∀ (i : Fin (k + 1)),
      a[↑i] =
        QuantumBlockEncoding.HermiteBernstein.sourceCoefficient k ↑i)
  (r : Fin (2 * k + 2)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.leftEntry k F a
        r).value =
    QuantumBlockEncoding.HermiteBernstein.leftCoefficient k ↑r

theorem QuantumBlockEncoding.StoredHermiteCoefficients.leftEntry_value
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (hF :
    ∀ (i : Fin (2 * k + 2)),
      F[↑i] = ↑(↑i).factorial)
  (a : Vector ℝ (k + 1))
  (ha :
    ∀ (i : Fin (k + 1)),
      a[↑i] =
        QuantumBlockEncoding.HermiteBernstein.sourceCoefficient
          k ↑i)
  (r : Fin (2 * k + 2)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.leftEntry
        k F a r).value =
    QuantumBlockEncoding.HermiteBernstein.leftCoefficient
      k ↑r

Definition10.61.16

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.61.16●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

def QuantumBlockEncoding.StoredHermiteCoefficients.lefts (k : ℕ)
  (F : Vector ℝ (2 * k + 2)) (a : Vector ℝ (k + 1)) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (2 * k + 2))

def QuantumBlockEncoding.StoredHermiteCoefficients.lefts
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (a : Vector ℝ (k + 1)) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (2 * k + 2))

Theorem10.61.17

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.17●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.lefts_value (k : ℕ)
  (F : Vector ℝ (2 * k + 2))
  (hF : ∀ (i : Fin (2 * k + 2)), F[↑i] = ↑(↑i).factorial)
  (a : Vector ℝ (k + 1))
  (ha :
    ∀ (i : Fin (k + 1)),
      a[↑i] =
        QuantumBlockEncoding.HermiteBernstein.sourceCoefficient k ↑i)
  (r : Fin (2 * k + 2)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.lefts k F
          a).value[↑r] =
    QuantumBlockEncoding.HermiteBernstein.leftCoefficient k ↑r

theorem QuantumBlockEncoding.StoredHermiteCoefficients.lefts_value
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (hF :
    ∀ (i : Fin (2 * k + 2)),
      F[↑i] = ↑(↑i).factorial)
  (a : Vector ℝ (k + 1))
  (ha :
    ∀ (i : Fin (k + 1)),
      a[↑i] =
        QuantumBlockEncoding.HermiteBernstein.sourceCoefficient
          k ↑i)
  (r : Fin (2 * k + 2)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.lefts
          k F a).value[↑r] =
    QuantumBlockEncoding.HermiteBernstein.leftCoefficient
      k ↑r

Definition10.61.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “from constant”. All shared intermediate arrays are materialized before they are consumed.

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. All shared intermediate arrays are materialized before they are consumed.

Declaration kind. def.

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

Lean code for Definition10.61.18●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

def QuantumBlockEncoding.StoredHermiteCoefficients.fromConstant (k : ℕ)
  (e : ℝ) : QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (2 * k + 2))

def QuantumBlockEncoding.StoredHermiteCoefficients.fromConstant
  (k : ℕ) (e : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (2 * k + 2))

All shared intermediate arrays are materialized before they are consumed.

Theorem10.61.19

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.19●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.fromConstant_value
  (k : ℕ) (e : ℝ) (r : Fin (2 * k + 2)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.fromConstant k
          e).value[↑r] =
    e * QuantumBlockEncoding.HermiteBernstein.leftCoefficient k ↑r +
      QuantumBlockEncoding.HermiteBernstein.leftCoefficient k
        (2 * k + 1 - ↑r)

theorem QuantumBlockEncoding.StoredHermiteCoefficients.fromConstant_value
  (k : ℕ) (e : ℝ) (r : Fin (2 * k + 2)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.fromConstant
          k e).value[↑r] =
    e *
        QuantumBlockEncoding.HermiteBernstein.leftCoefficient
          k ↑r +
      QuantumBlockEncoding.HermiteBernstein.leftCoefficient
        k (2 * k + 1 - ↑r)

Definition10.61.20

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “source run”. A proposition-valued field is a requirement until a constructor supplies it. Extra source primitive accounting, deliberately separate from 'Op'.

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. Extra source primitive accounting, deliberately separate from 'Op'.

Declaration kind. structure.

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

Lean code for Definition10.61.20●1 definition

structure(2 fields)defined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

structure QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun (α : Type) :
  Type

structure QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
  (α : Type) : Type

Extra source primitive accounting, deliberately separate from `Op`.

Fields

run : QuantumBlockEncoding.StoredGivens.Run α

exponentialCalls : ℕ

Definition10.61.21

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.61.21●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

def QuantumBlockEncoding.StoredHermiteCoefficients.exponential (x : ℝ) :
  QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun ℝ

def QuantumBlockEncoding.StoredHermiteCoefficients.exponential
  (x : ℝ) :
  QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
    ℝ

Definition10.61.22

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.61.22●1 definition

defdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

def QuantumBlockEncoding.StoredHermiteCoefficients.compile (k : ℕ) :
  QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
    (Vector ℝ (2 * k + 2))

def QuantumBlockEncoding.StoredHermiteCoefficients.compile
  (k : ℕ) :
  QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
    (Vector ℝ (2 * k + 2))

Theorem10.61.23

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.23●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_value (k : ℕ)
  (r : Fin (2 * k + 2)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.compile
            k).run.value[↑r] =
    QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient k
      ↑r

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_value
  (k : ℕ) (r : Fin (2 * k + 2)) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.compile
            k).run.value[↑r] =
    QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
      k ↑r

Theorem10.61.24

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.24●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_nonneg (k : ℕ)
  (r : Fin (2 * k + 2)) :
  0 ≤
    (QuantumBlockEncoding.StoredHermiteCoefficients.compile
            k).run.value[↑r]

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_nonneg
  (k : ℕ) (r : Fin (2 * k + 2)) :
  0 ≤
    (QuantumBlockEncoding.StoredHermiteCoefficients.compile
            k).run.value[↑r]

Theorem10.61.25

uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.leftCoefficient_pos
  (k r : ℕ) (hr : r ≤ k) :
  0 < QuantumBlockEncoding.HermiteBernstein.leftCoefficient k r

theorem QuantumBlockEncoding.StoredHermiteCoefficients.leftCoefficient_pos
  (k r : ℕ) (hr : r ≤ k) :
  0 <
    QuantumBlockEncoding.HermiteBernstein.leftCoefficient
      k r

Theorem10.61.26

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile pos”; the hypotheses and conclusion in the code panel fix its exact scope. Every returned source coefficient is strictly positive, including k=0.

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 returned source coefficient is strictly positive, including k=0.

Declaration kind. theorem.

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

Lean code for Theorem10.61.26●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_pos (k : ℕ)
  (r : Fin (2 * k + 2)) :
  0 <
    (QuantumBlockEncoding.StoredHermiteCoefficients.compile
            k).run.value[↑r]

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_pos
  (k : ℕ) (r : Fin (2 * k + 2)) :
  0 <
    (QuantumBlockEncoding.StoredHermiteCoefficients.compile
            k).run.value[↑r]

Every returned source coefficient is strictly positive, including k=0.

Theorem10.61.27

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

Lean code for Theorem10.61.27●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_exponentialCalls
  (k : ℕ) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.compile
        k).exponentialCalls =
    1

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_exponentialCalls
  (k : ℕ) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.compile
        k).exponentialCalls =
    1

Theorem10.61.28

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.28●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.extend_cost_le {n : ℕ}
  (xs : Vector ℝ (n + 1)) (last : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.extend xs last).cost
      op ≤
    6 * (n + 2)

theorem QuantumBlockEncoding.StoredHermiteCoefficients.extend_cost_le
  {n : ℕ} (xs : Vector ℝ (n + 1))
  (last : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.extend
          xs last).cost
      op ≤
    6 * (n + 2)

Theorem10.61.29

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.29●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.factorials_cost_le
  (n : ℕ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.factorials n).cost
      op ≤
    10 * (n + 1) ^ 2

theorem QuantumBlockEncoding.StoredHermiteCoefficients.factorials_cost_le
  (n : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.factorials
          n).cost
      op ≤
    10 * (n + 1) ^ 2

Theorem10.61.30

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.30●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.chooseFrom_cost {N : ℕ}
  (F : Vector ℝ (N + 1)) (n r : ℕ) (hr : r ≤ n) (hn : n ≤ N)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.chooseFrom F n r hr
          hn).cost
      op =
    3 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.read op +
      2 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field op

theorem QuantumBlockEncoding.StoredHermiteCoefficients.chooseFrom_cost
  {N : ℕ} (F : Vector ℝ (N + 1)) (n r : ℕ)
  (hr : r ≤ n) (hn : n ≤ N)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.chooseFrom
          F n r hr hn).cost
      op =
    3 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.read
          op +
      2 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field
          op

Theorem10.61.31

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.31●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.sourceEntry_cost_le
  (k : ℕ) (F : Vector ℝ (2 * k + 2)) (i : Fin (k + 1))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.sourceEntry k F
          i).cost
      op ≤
    8 * (k + 1)

theorem QuantumBlockEncoding.StoredHermiteCoefficients.sourceEntry_cost_le
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (i : Fin (k + 1))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.sourceEntry
          k F i).cost
      op ≤
    8 * (k + 1)

Theorem10.61.32

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.32●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.sources_cost_le (k : ℕ)
  (F : Vector ℝ (2 * k + 2))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.sources k F).cost op ≤
    12 * (k + 1) ^ 2

theorem QuantumBlockEncoding.StoredHermiteCoefficients.sources_cost_le
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.sources
          k F).cost
      op ≤
    12 * (k + 1) ^ 2

Theorem10.61.33

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.33●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.leftTerm_cost_le (k : ℕ)
  (F : Vector ℝ (2 * k + 2)) (a : Vector ℝ (k + 1)) (denominator : ℝ)
  (r : Fin (2 * k + 2)) (i : Fin (k + 1))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.leftTerm k F a
          denominator r i).cost
      op ≤
    10

theorem QuantumBlockEncoding.StoredHermiteCoefficients.leftTerm_cost_le
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (a : Vector ℝ (k + 1)) (denominator : ℝ)
  (r : Fin (2 * k + 2)) (i : Fin (k + 1))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.leftTerm
          k F a denominator r i).cost
      op ≤
    10

Theorem10.61.34

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.34●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.leftEntry_cost_le (k : ℕ)
  (F : Vector ℝ (2 * k + 2)) (a : Vector ℝ (k + 1))
  (r : Fin (2 * k + 2)) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.leftEntry k F a
          r).cost
      op ≤
    16 * (k + 1)

theorem QuantumBlockEncoding.StoredHermiteCoefficients.leftEntry_cost_le
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (a : Vector ℝ (k + 1))
  (r : Fin (2 * k + 2))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.leftEntry
          k F a r).cost
      op ≤
    16 * (k + 1)

Theorem10.61.35

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.61.35●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.lefts_cost_le (k : ℕ)
  (F : Vector ℝ (2 * k + 2)) (a : Vector ℝ (k + 1))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.lefts k F a).cost op ≤
    40 * (k + 1) ^ 2

theorem QuantumBlockEncoding.StoredHermiteCoefficients.lefts_cost_le
  (k : ℕ) (F : Vector ℝ (2 * k + 2))
  (a : Vector ℝ (k + 1))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.lefts
          k F a).cost
      op ≤
    40 * (k + 1) ^ 2

Theorem10.61.36

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “from constant cost le”; the hypotheses and conclusion in the code panel fix its exact scope. Quadratic bound for every ordinary operation category of the same run.

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. Quadratic bound for every ordinary operation category of the same run.

Declaration kind. theorem.

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

Lean code for Theorem10.61.36●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.fromConstant_cost_le
  (k : ℕ) (e : ℝ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.fromConstant k e).cost
      op ≤
    108 * (k + 1) ^ 2

theorem QuantumBlockEncoding.StoredHermiteCoefficients.fromConstant_cost_le
  (k : ℕ) (e : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.fromConstant
          k e).cost
      op ≤
    108 * (k + 1) ^ 2

Quadratic bound for every ordinary operation category of the same run.

Theorem10.61.37

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

Lean code for Theorem10.61.37●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_cost_le (k : ℕ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.compile k).run.cost
      op ≤
    108 * (k + 1) ^ 2

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_cost_le
  (k : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteCoefficients.compile
            k).run.cost
      op ≤
    108 * (k + 1) ^ 2

Theorem10.61.38

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. The separate exponential count is exactly one and is not in this sum.

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 separate exponential count is exactly one and is not in this sum.

Declaration kind. theorem.

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

Lean code for Theorem10.61.38●1 theorem

theoremdefined in QuantumBlockEncoding/StoredHermiteCoefficients.lean

complete

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_total_cost_le
  (k : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteCoefficients.compile
            k).run.cost ≤
    864 * (k + 1) ^ 2

theorem QuantumBlockEncoding.StoredHermiteCoefficients.compile_total_cost_le
  (k : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteCoefficients.compile
            k).run.cost ≤
    864 * (k + 1) ^ 2

The separate exponential count is exactly one and is not in this sum.