ASPBE Lean Blueprint

10.66. QuantumBlockEncoding/StoredHermiteSharedTables.lean🔗

26 explicit public declarations, in source order.

Definition10.66.1
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “inverse powers”. Cache '1 / 2^j' by one real division per extension, with full-copy writes.

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. Cache '1 / 2^j' by one real division per extension, with full-copy writes.

Declaration kind. def.

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

Lean code for Definition10.66.1●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    def QuantumBlockEncoding.StoredHermiteSharedTables.inversePowers (d : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (d + 1))
    def QuantumBlockEncoding.StoredHermiteSharedTables.inversePowers
  (d : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (d + 1))
    Cache `1 / 2^j` by one real division per extension, with full-copy writes.
Theorem10.66.2
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “inverse powers 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/StoredHermiteSharedTables.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.66.2●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.inversePowers_value
  (d : ℕ) (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.inversePowers
          d).value[↑i] =
    1 / 2 ^ ↑i
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.inversePowers_value
  (d : ℕ) (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.inversePowers
          d).value[↑i] =
    1 / 2 ^ ↑i
Definition10.66.3
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.66.3●1 definition
  • structure(2 fields)defined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    structure QuantumBlockEncoding.StoredHermiteSharedTables.Tables (d : ℕ) : Type
    structure QuantumBlockEncoding.StoredHermiteSharedTables.Tables
  (d : ℕ) : Type

    Fields

    falseTable : QuantumBlockEncoding.StoredGivens.StoredMatrix (d + 1) (d + 1)
    trueTable : QuantumBlockEncoding.StoredGivens.StoredMatrix (d + 1) (d + 1)
Definition10.66.4
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.66.4●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    def QuantumBlockEncoding.StoredHermiteSharedTables.falseEntry {d : ℕ}
  (F H : Vector ℝ (d + 1)) (i j : Fin (d + 1)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ
    def QuantumBlockEncoding.StoredHermiteSharedTables.falseEntry
  {d : ℕ} (F H : Vector ℝ (d + 1))
  (i j : Fin (d + 1)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ
Definition10.66.5
uses 0used by 0✓L∃∀N

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

Lean code for Definition10.66.5●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    def QuantumBlockEncoding.StoredHermiteSharedTables.trueEntry {d : ℕ}
  (F H : Vector ℝ (d + 1)) (i j : Fin (d + 1)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ
    def QuantumBlockEncoding.StoredHermiteSharedTables.trueEntry
  {d : ℕ} (F H : Vector ℝ (d + 1))
  (i j : Fin (d + 1)) :
  QuantumBlockEncoding.StoredGivens.Run ℝ
Theorem10.66.6
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “false 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/StoredHermiteSharedTables.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.66.6●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.falseEntry_value {d : ℕ}
  (F H : Vector ℝ (d + 1))
  (hF : ∀ (i : Fin (d + 1)), F[↑i] = ↑(↑i).factorial)
  (hH : ∀ (i : Fin (d + 1)), H[↑i] = 1 / 2 ^ ↑i) (i j : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.falseEntry F H i
        j).value =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore d false i j
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.falseEntry_value
  {d : ℕ} (F H : Vector ℝ (d + 1))
  (hF :
    ∀ (i : Fin (d + 1)),
      F[↑i] = ↑(↑i).factorial)
  (hH :
    ∀ (i : Fin (d + 1)),
      H[↑i] = 1 / 2 ^ ↑i)
  (i j : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.falseEntry
        F H i j).value =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore
      d false i j
Theorem10.66.7
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.66.7●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.trueEntry_value {d : ℕ}
  (F H : Vector ℝ (d + 1))
  (hF : ∀ (i : Fin (d + 1)), F[↑i] = ↑(↑i).factorial)
  (hH : ∀ (i : Fin (d + 1)), H[↑i] = 1 / 2 ^ ↑i) (i j : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.trueEntry F H i
        j).value =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore d true i j
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.trueEntry_value
  {d : ℕ} (F H : Vector ℝ (d + 1))
  (hF :
    ∀ (i : Fin (d + 1)),
      F[↑i] = ↑(↑i).factorial)
  (hH :
    ∀ (i : Fin (d + 1)),
      H[↑i] = 1 / 2 ^ ↑i)
  (i j : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.trueEntry
        F H i j).value =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore
      d true i j
Definition10.66.8
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “compile”. Both tables share a single factorial table and a single inverse-power table.

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. Both tables share a single factorial table and a single inverse-power table.

Declaration kind. def.

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

Lean code for Definition10.66.8●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    def QuantumBlockEncoding.StoredHermiteSharedTables.compile (d : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredHermiteSharedTables.Tables d)
    def QuantumBlockEncoding.StoredHermiteSharedTables.compile
  (d : ℕ) :
  QuantumBlockEncoding.StoredGivens.Run
    (QuantumBlockEncoding.StoredHermiteSharedTables.Tables
      d)
    Both tables share a single factorial table and a single inverse-power table.
Theorem10.66.9
uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteSharedTables.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.66.9●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.compile_false (d : ℕ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredHermiteSharedTables.compile
            d).value.falseTable =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore d false
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.compile_false
  (d : ℕ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredHermiteSharedTables.compile
            d).value.falseTable =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore
      d false
Theorem10.66.10
uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.66.10●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.compile_true (d : ℕ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredHermiteSharedTables.compile
            d).value.trueTable =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore d true
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.compile_true
  (d : ℕ) :
  QuantumBlockEncoding.StoredGivens.denote
      (QuantumBlockEncoding.StoredHermiteSharedTables.compile
            d).value.trueTable =
    QuantumBlockEncoding.HermiteBoundaryInjection.sharedCore
      d true
Definition10.66.11
uses 0used by 0✓L∃∀N

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

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

Lean code for Definition10.66.11●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    def QuantumBlockEncoding.StoredHermiteSharedTables.withCost {α : Type}
  (extra : QuantumBlockEncoding.StoredGivens.Cost)
  (result : QuantumBlockEncoding.StoredGivens.Run α) :
  QuantumBlockEncoding.StoredGivens.Run α
    def QuantumBlockEncoding.StoredHermiteSharedTables.withCost
  {α : Type}
  (extra :
    QuantumBlockEncoding.StoredGivens.Cost)
  (result :
    QuantumBlockEncoding.StoredGivens.Run
      α) :
  QuantumBlockEncoding.StoredGivens.Run α
Theorem10.66.12
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.66.12●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.withCost_value {α : Type}
  (extra : QuantumBlockEncoding.StoredGivens.Cost)
  (result : QuantumBlockEncoding.StoredGivens.Run α) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.withCost extra
        result).value =
    result.value
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.withCost_value
  {α : Type}
  (extra :
    QuantumBlockEncoding.StoredGivens.Cost)
  (result :
    QuantumBlockEncoding.StoredGivens.Run
      α) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.withCost
        extra result).value =
    result.value
Theorem10.66.13
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “with cost 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/StoredHermiteSharedTables.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.66.13●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.withCost_cost {α : Type}
  (extra : QuantumBlockEncoding.StoredGivens.Cost)
  (result : QuantumBlockEncoding.StoredGivens.Run α)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.withCost extra
          result).cost
      op =
    extra op + result.cost op
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.withCost_cost
  {α : Type}
  (extra :
    QuantumBlockEncoding.StoredGivens.Cost)
  (result :
    QuantumBlockEncoding.StoredGivens.Run
      α)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.withCost
          extra result).cost
      op =
    extra op + result.cost op
Definition10.66.14
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “shifted restriction”. Parameter arithmetic is an explicit, separately reusable supplier.

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. Parameter arithmetic is an explicit, separately reusable supplier.

Declaration kind. def.

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

Lean code for Definition10.66.14●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    def QuantumBlockEncoding.StoredHermiteSharedTables.shiftedRestriction
  {d : ℕ} (xs : Vector ℝ (d + 1)) (childLower childUpper : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (d + 1))
    def QuantumBlockEncoding.StoredHermiteSharedTables.shiftedRestriction
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (childLower childUpper : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (d + 1))
    Parameter arithmetic is an explicit, separately reusable supplier.
Theorem10.66.15
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “shifted restriction 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/StoredHermiteSharedTables.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.66.15●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.shiftedRestriction_value
  {d : ℕ} (xs : Vector ℝ (d + 1)) (c : ℕ → ℝ)
  (hx : ∀ (i : Fin (d + 1)), xs[↑i] = c ↑i) (a b : ℝ)
  (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.shiftedRestriction xs
          a b).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.restrictCoefficients d (1 + a)
      (1 + b) c ↑i
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.shiftedRestriction_value
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (c : ℕ → ℝ)
  (hx :
    ∀ (i : Fin (d + 1)), xs[↑i] = c ↑i)
  (a b : ℝ) (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.shiftedRestriction
          xs a b).value[↑i] =
    QuantumBlockEncoding.HermiteBernstein.restrictCoefficients
      d (1 + a) (1 + b) c ↑i
Theorem10.66.16
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.66.16●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.shiftedRestriction_cost
  {d : ℕ} (xs : Vector ℝ (d + 1)) (a b : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.shiftedRestriction xs
          a b).cost
      op =
    2 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field op +
      (QuantumBlockEncoding.StoredBernstein.restrict xs (1 + a)
            (1 + b)).cost
        op
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.shiftedRestriction_cost
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (a b : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.shiftedRestriction
          xs a b).cost
      op =
    2 *
        QuantumBlockEncoding.StoredGivens.tick
          QuantumBlockEncoding.StoredGivens.Op.field
          op +
      (QuantumBlockEncoding.StoredBernstein.restrict
            xs (1 + a) (1 + b)).cost
        op
Definition10.66.17
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “injection row”. Cached coordinates are real inputs.

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. Cached coordinates are real inputs. Their source construction is separate. The guard is supplied by geometry; it is charged as a control comparison here. Disabled rows still have all zero entries explicitly materialized.

Declaration kind. def.

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

Lean code for Definition10.66.17●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    def QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow {d : ℕ}
  (xs : Vector ℝ (d + 1)) (childLower childUpper : ℝ) (enabled : Bool) :
  QuantumBlockEncoding.StoredGivens.Run (Vector ℝ (d + 1))
    def QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (childLower childUpper : ℝ)
  (enabled : Bool) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector ℝ (d + 1))
    Cached coordinates are real inputs. Their source construction is separate.
The guard is supplied by geometry; it is charged as a control comparison here.
Disabled rows still have all zero entries explicitly materialized.
Theorem10.66.18
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.66.18●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow_value
  {d : ℕ} (xs : Vector ℝ (d + 1)) (c : ℕ → ℝ)
  (hx : ∀ (i : Fin (d + 1)), xs[↑i] = c ↑i) (childLower childUpper : ℝ)
  (enabled : Bool) (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow xs
          childLower childUpper enabled).value[↑i] =
    if enabled = true then
      QuantumBlockEncoding.HermiteBernstein.restrictCoefficients d
        (1 + childLower) (1 + childUpper) c ↑i
    else 0
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow_value
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (c : ℕ → ℝ)
  (hx :
    ∀ (i : Fin (d + 1)), xs[↑i] = c ↑i)
  (childLower childUpper : ℝ)
  (enabled : Bool) (i : Fin (d + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow
          xs childLower childUpper
          enabled).value[↑i] =
    if enabled = true then
      QuantumBlockEncoding.HermiteBernstein.restrictCoefficients
        d (1 + childLower)
        (1 + childUpper) c ↑i
    else 0
Theorem10.66.19
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “injection row eq injection core”; the hypotheses and conclusion in the code panel fix its exact scope. Strong row refinement, with a previously stored source coefficient vector.

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

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

Technical source note. Strong row refinement, with a previously stored source coefficient vector. No source coefficients, dyadic addresses, or real coordinates are regenerated. Geometry separately certifies the valid restriction domain when interpreting this row as a polynomial; algebraic equality of the returned entries is total.

Declaration kind. theorem.

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

Lean code for Theorem10.66.19●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow_eq_injectionCore
  (k : ℕ) (xs : Vector ℝ (2 * k + 1 + 1))
  (hx :
    ∀ (i : Fin (2 * k + 1 + 1)),
      xs[↑i] =
        QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
          k ↑i)
  (origin step : ℝ) (lower upper : ℕ) (schedule : ℕ → ℕ) (r : ℕ)
  (bit : Bool) (childLower childUpper : ℝ) (enabled : Bool)
  (hl :
    childLower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        step
        (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
          schedule r bit))
  (hu :
    childUpper =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        step
        (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
            schedule r bit +
          2 ^ r))
  (he :
    enabled = true ↔
      QuantumBlockEncoding.HermiteBoundaryInjection.Full lower upper
        (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
          schedule r bit)
        (2 ^ r))
  (i : Fin (2 * k + 1 + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow xs
          childLower childUpper enabled).value[↑i] =
    QuantumBlockEncoding.HermiteBoundaryInjection.injectionCore k origin
      step lower upper schedule r bit none (some i)
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow_eq_injectionCore
  (k : ℕ) (xs : Vector ℝ (2 * k + 1 + 1))
  (hx :
    ∀ (i : Fin (2 * k + 1 + 1)),
      xs[↑i] =
        QuantumBlockEncoding.HermiteBernstein.sourceBernsteinCoefficient
          k ↑i)
  (origin step : ℝ) (lower upper : ℕ)
  (schedule : ℕ → ℕ) (r : ℕ) (bit : Bool)
  (childLower childUpper : ℝ)
  (enabled : Bool)
  (hl :
    childLower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin step
        (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
          schedule r bit))
  (hu :
    childUpper =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin step
        (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
            schedule r bit +
          2 ^ r))
  (he :
    enabled = true ↔
      QuantumBlockEncoding.HermiteBoundaryInjection.Full
        lower upper
        (QuantumBlockEncoding.HermiteBoundaryInjection.selectedChild
          schedule r bit)
        (2 ^ r))
  (i : Fin (2 * k + 1 + 1)) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow
          xs childLower childUpper
          enabled).value[↑i] =
    QuantumBlockEncoding.HermiteBoundaryInjection.injectionCore
      k origin step lower upper schedule r
      bit none (some i)
    Strong row refinement, with a previously stored source coefficient vector.
No source coefficients, dyadic addresses, or real coordinates are regenerated.
Geometry separately certifies the valid restriction domain when interpreting
this row as a polynomial; algebraic equality of the returned entries is total.
Theorem10.66.20
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “inverse powers 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/StoredHermiteSharedTables.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.66.20●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.inversePowers_cost_le
  (d : ℕ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.inversePowers d).cost
      op ≤
    8 * (d + 1) ^ 2
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.inversePowers_cost_le
  (d : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.inversePowers
          d).cost
      op ≤
    8 * (d + 1) ^ 2
Theorem10.66.21
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.66.21●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.falseEntry_cost_le
  {d : ℕ} (F H : Vector ℝ (d + 1)) (i j : Fin (d + 1))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.falseEntry F H i
          j).cost
      op ≤
    8
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.falseEntry_cost_le
  {d : ℕ} (F H : Vector ℝ (d + 1))
  (i j : Fin (d + 1))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.falseEntry
          F H i j).cost
      op ≤
    8
Theorem10.66.22
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.66.22●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.trueEntry_cost_le {d : ℕ}
  (F H : Vector ℝ (d + 1)) (i j : Fin (d + 1))
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.trueEntry F H i
          j).cost
      op ≤
    8
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.trueEntry_cost_le
  {d : ℕ} (F H : Vector ℝ (d + 1))
  (i j : Fin (d + 1))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.trueEntry
          F H i j).cost
      op ≤
    8
Theorem10.66.23
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. Quadratic per-counter bound of the actual two-table producer.

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 per-counter bound of the actual two-table producer.

Declaration kind. theorem.

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

Lean code for Theorem10.66.23●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.compile_cost_le (d : ℕ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.compile d).cost op ≤
    50 * (d + 1) ^ 2
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.compile_cost_le
  (d : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.compile
          d).cost
      op ≤
    50 * (d + 1) ^ 2
    Quadratic per-counter bound of the actual two-table producer.
Theorem10.66.24
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “compile total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.66.24●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.compile_total_cost_le
  (d : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteSharedTables.compile d).cost ≤
    400 * (d + 1) ^ 2
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.compile_total_cost_le
  (d : ℕ) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteSharedTables.compile
          d).cost ≤
    400 * (d + 1) ^ 2
Theorem10.66.25
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.66.25●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow_cost_le
  {d : ℕ} (xs : Vector ℝ (d + 1)) (childLower childUpper : ℝ)
  (enabled : Bool) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow xs
          childLower childUpper enabled).cost
      op ≤
    2 * QuantumBlockEncoding.StoredBernstein.edgeBudget d op +
        5 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.compare op
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow_cost_le
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (childLower childUpper : ℝ)
  (enabled : Bool)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow
          xs childLower childUpper
          enabled).cost
      op ≤
    2 *
          QuantumBlockEncoding.StoredBernstein.edgeBudget
            d op +
        5 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field
            op +
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.compare
        op
Theorem10.66.26
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.66.26●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteSharedTables.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow_total_cost_le
  {d : ℕ} (xs : Vector ℝ (d + 1)) (childLower childUpper : ℝ)
  (enabled : Bool) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow xs
          childLower childUpper enabled).cost ≤
    20 * d ^ 3 + 42 * d ^ 2 + 32 * d + 16
    theorem QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow_total_cost_le
  {d : ℕ} (xs : Vector ℝ (d + 1))
  (childLower childUpper : ℝ)
  (enabled : Bool) :
  QuantumBlockEncoding.StoredRectangularGivens.total
      (QuantumBlockEncoding.StoredHermiteSharedTables.injectionRow
          xs childLower childUpper
          enabled).cost ≤
    20 * d ^ 3 + 42 * d ^ 2 + 32 * d + 16