10.58. QuantumBlockEncoding/StoredBernstein.lean🔗

20 explicit public declarations, in source order.

Definition10.58.1

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.58.1●1 definition

defdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

def QuantumBlockEncoding.StoredBernstein.cell {n : ℕ} (xs : Vector ℝ n)
  (u t : ℝ) (i : Fin n) : QuantumBlockEncoding.StoredGivens.Run ℝ

def QuantumBlockEncoding.StoredBernstein.cell
  {n : ℕ} (xs : Vector ℝ n) (u t : ℝ)
  (i : Fin n) :
  QuantumBlockEncoding.StoredGivens.Run ℝ

Definition10.58.2

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “step”. Truncated row; the last entry is zero and is never read by a valid cone.

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. Truncated row; the last entry is zero and is never read by a valid cone.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

def QuantumBlockEncoding.StoredBernstein.step {n : ℕ} (xs : Vector ℝ n)
  (t : ℝ) : QuantumBlockEncoding.StoredGivens.Run (Vector ℝ n)

def QuantumBlockEncoding.StoredBernstein.step
  {n : ℕ} (xs : Vector ℝ n) (t : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ n)

Truncated row; the last entry is zero and is never read by a valid cone.

Theorem10.58.3

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.58.3●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.step_value {n : ℕ}
  (xs : Vector ℝ n) (t : ℝ) (i : Fin n) (hi : ↑i + 1 < n) :
  (QuantumBlockEncoding.StoredBernstein.step xs t).value[↑i] =
    (1 - t) * xs[↑i] + t * xs[↑i + 1]

theorem QuantumBlockEncoding.StoredBernstein.step_value
  {n : ℕ} (xs : Vector ℝ n) (t : ℝ)
  (i : Fin n) (hi : ↑i + 1 < n) :
  (QuantumBlockEncoding.StoredBernstein.step
          xs t).value[↑i] =
    (1 - t) * xs[↑i] + t * xs[↑i + 1]

Definition10.58.4

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “rows”. Every scalar entry of the previous row is cached, not a nested callback.

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. Every scalar entry of the previous row is cached, not a nested callback.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

def QuantumBlockEncoding.StoredBernstein.rows {n : ℕ} (xs : Vector ℝ n)
  (t : ℝ) : ℕ → QuantumBlockEncoding.StoredGivens.Run (Vector ℝ n)

def QuantumBlockEncoding.StoredBernstein.rows
  {n : ℕ} (xs : Vector ℝ n) (t : ℝ) :
  ℕ →
    QuantumBlockEncoding.StoredGivens.Run
      (Vector ℝ n)

Every scalar entry of the previous row is cached, not a nested callback.

Theorem10.58.5

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.58.5●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.casteljau_succ (k : ℕ) (c : ℕ → ℝ)
  (t : ℝ) (i : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.casteljau (k + 1) c t i =
    (1 - t) * QuantumBlockEncoding.HermiteBernstein.casteljau k c t i +
      t * QuantumBlockEncoding.HermiteBernstein.casteljau k c t (i + 1)

theorem QuantumBlockEncoding.StoredBernstein.casteljau_succ
  (k : ℕ) (c : ℕ → ℝ) (t : ℝ) (i : ℕ) :
  QuantumBlockEncoding.HermiteBernstein.casteljau
      (k + 1) c t i =
    (1 - t) *
        QuantumBlockEncoding.HermiteBernstein.casteljau
          k c t i +
      t *
        QuantumBlockEncoding.HermiteBernstein.casteljau
          k c t (i + 1)

Theorem10.58.6

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.58.6●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.rows_value {n : ℕ}
  (xs : Vector ℝ n) (c : ℕ → ℝ) (hx : ∀ (i : Fin n), xs[↑i] = c ↑i)
  (t : ℝ) (k : ℕ) (i : Fin n) (hi : ↑i + k < n) :
  (QuantumBlockEncoding.StoredBernstein.rows xs t k).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.casteljau k c t ↑i

theorem QuantumBlockEncoding.StoredBernstein.rows_value
  {n : ℕ} (xs : Vector ℝ n) (c : ℕ → ℝ)
  (hx : ∀ (i : Fin n), xs[↑i] = c ↑i)
  (t : ℝ) (k : ℕ) (i : Fin n)
  (hi : ↑i + k < n) :
  (QuantumBlockEncoding.StoredBernstein.rows
          xs t k).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.casteljau
      k c t ↑i

Definition10.58.7

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.58.7●1 definition

defdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

def QuantumBlockEncoding.StoredBernstein.rowBudget (n : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredBernstein.rowBudget
  (n : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem10.58.8

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.58.8●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.step_cost_le {n : ℕ}
  (xs : Vector ℝ n) (t : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBernstein.step xs t).cost op ≤
    QuantumBlockEncoding.StoredBernstein.rowBudget n op

theorem QuantumBlockEncoding.StoredBernstein.step_cost_le
  {n : ℕ} (xs : Vector ℝ n) (t : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBernstein.step
          xs t).cost
      op ≤
    QuantumBlockEncoding.StoredBernstein.rowBudget
      n op

Theorem10.58.9

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.58.9●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.rows_cost_le {n : ℕ}
  (xs : Vector ℝ n) (t : ℝ) (k : ℕ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBernstein.rows xs t k).cost op ≤
    k * QuantumBlockEncoding.StoredBernstein.rowBudget n op

theorem QuantumBlockEncoding.StoredBernstein.rows_cost_le
  {n : ℕ} (xs : Vector ℝ n) (t : ℝ)
  (k : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBernstein.rows
          xs t k).cost
      op ≤
    k *
      QuantumBlockEncoding.StoredBernstein.rowBudget
        n op

Definition10.58.10

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.58.10●1 definition

defdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

def QuantumBlockEncoding.StoredBernstein.left {d : ℕ}
  (xs : Vector ℝ (d + 1)) (u : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (d + 1))

def QuantumBlockEncoding.StoredBernstein.left
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (u : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (d + 1))

Definition10.58.11

uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.58.11●1 definition

defdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

def QuantumBlockEncoding.StoredBernstein.right {d : ℕ}
  (xs : Vector ℝ (d + 1)) (u : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (d + 1))

def QuantumBlockEncoding.StoredBernstein.right
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (u : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (d + 1))

Theorem10.58.12

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.58.12●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.left_value {d : ℕ}
  (xs : Vector ℝ (d + 1)) (c : ℕ → ℝ)
  (hx : ∀ (i : Fin (d + 1)), xs[↑i] = c ↑i) (u : ℝ) (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredBernstein.left xs u).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.leftRestriction u c ↑i

theorem QuantumBlockEncoding.StoredBernstein.left_value
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (c : ℕ → ℝ)
  (hx :
    ∀ (i : Fin (d + 1)), xs[↑i] = c ↑i)
  (u : ℝ) (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredBernstein.left
          xs u).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.leftRestriction
      u c ↑i

Theorem10.58.13

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.58.13●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.right_value {d : ℕ}
  (xs : Vector ℝ (d + 1)) (c : ℕ → ℝ)
  (hx : ∀ (i : Fin (d + 1)), xs[↑i] = c ↑i) (u : ℝ) (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredBernstein.right xs u).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.rightRestriction d u c ↑i

theorem QuantumBlockEncoding.StoredBernstein.right_value
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (c : ℕ → ℝ)
  (hx :
    ∀ (i : Fin (d + 1)), xs[↑i] = c ↑i)
  (u : ℝ) (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredBernstein.right
          xs u).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.rightRestriction
      d u c ↑i

Definition10.58.14

uses 0used by 0✓L∃∀N

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

Lean code for Definition10.58.14●1 definition

defdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

def QuantumBlockEncoding.StoredBernstein.edgeBudget (d : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

def QuantumBlockEncoding.StoredBernstein.edgeBudget
  (d : ℕ) :
  QuantumBlockEncoding.StoredGivens.Cost

Theorem10.58.15

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.58.15●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.left_cost_le {d : ℕ}
  (xs : Vector ℝ (d + 1)) (u : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBernstein.left xs u).cost op ≤
    QuantumBlockEncoding.StoredBernstein.edgeBudget d op

theorem QuantumBlockEncoding.StoredBernstein.left_cost_le
  {d : ℕ} (xs : Vector ℝ (d + 1)) (u : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBernstein.left
          xs u).cost
      op ≤
    QuantumBlockEncoding.StoredBernstein.edgeBudget
      d op

Theorem10.58.16

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.58.16●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.right_cost_le {d : ℕ}
  (xs : Vector ℝ (d + 1)) (u : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBernstein.right xs u).cost op ≤
    QuantumBlockEncoding.StoredBernstein.edgeBudget d op

theorem QuantumBlockEncoding.StoredBernstein.right_cost_le
  {d : ℕ} (xs : Vector ℝ (d + 1)) (u : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBernstein.right
          xs u).cost
      op ≤
    QuantumBlockEncoding.StoredBernstein.edgeBudget
      d op

Definition10.58.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “restrict”. The actual two-edge producer, with three charged parameter 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. The actual two-edge producer, with three charged parameter operations.

Declaration kind. def.

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

Lean code for Definition10.58.17●1 definition

defdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

def QuantumBlockEncoding.StoredBernstein.restrict {d : ℕ}
  (xs : Vector ℝ (d + 1)) (u v : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (d + 1))

def QuantumBlockEncoding.StoredBernstein.restrict
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (u v : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (d + 1))

The actual two-edge producer, with three charged parameter operations.

Theorem10.58.18

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.58.18●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.restrict_value {d : ℕ}
  (xs : Vector ℝ (d + 1)) (c : ℕ → ℝ)
  (hx : ∀ (i : Fin (d + 1)), xs[↑i] = c ↑i) (u v : ℝ)
  (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredBernstein.restrict xs u v).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.restrictCoefficients d u v c
      ↑i

theorem QuantumBlockEncoding.StoredBernstein.restrict_value
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (c : ℕ → ℝ)
  (hx :
    ∀ (i : Fin (d + 1)), xs[↑i] = c ↑i)
  (u v : ℝ) (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredBernstein.restrict
          xs u v).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.restrictCoefficients
      d u v c ↑i

Theorem10.58.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “restrict 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/StoredBernstein.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.58.19●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.restrict_cost_le {d : ℕ}
  (xs : Vector ℝ (d + 1)) (u v : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBernstein.restrict xs u v).cost op ≤
    2 * QuantumBlockEncoding.StoredBernstein.edgeBudget d op +
      3 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field op

theorem QuantumBlockEncoding.StoredBernstein.restrict_cost_le
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (u v : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredBernstein.restrict
          xs u v).cost
      op ≤
    2 *
        QuantumBlockEncoding.StoredBernstein.edgeBudget
          d op +
      3 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field
          op

Theorem10.58.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “restrict total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. All eight counted operation classes; source coefficient generation is separate.

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. All eight counted operation classes; source coefficient generation is separate.

Declaration kind. theorem.

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

Lean code for Theorem10.58.20●1 theorem

theoremdefined in QuantumBlockEncoding/StoredBernstein.lean

complete

theorem QuantumBlockEncoding.StoredBernstein.restrict_total_cost_le {d : ℕ}
  (xs : Vector ℝ (d + 1)) (u v : ℝ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredBernstein.restrict xs u v).cost ≤
    20 * d ^ 3 + 42 * d ^ 2 + 32 * d + 13

theorem QuantumBlockEncoding.StoredBernstein.restrict_total_cost_le
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (u v : ℝ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredBernstein.restrict
          xs u v).cost ≤
    20 * d ^ 3 + 42 * d ^ 2 + 32 * d + 13

All eight counted operation classes; source coefficient generation is separate.