ASPBE Lean Blueprint

10.62. QuantumBlockEncoding/StoredHermiteGeometry.lean🔗

34 explicit public declarations, in source order.

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

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

Lean code for Definition10.62.1●1 definition
  • structure(2 fields)defined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    structure QuantumBlockEncoding.StoredHermiteGeometry.TailLevel : Type
    structure QuantumBlockEncoding.StoredHermiteGeometry.TailLevel :
  Type

    Fields

    width : ℝ
    factor : ℝ
Definition10.62.2
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “append level”. Full-copy persistent extension; each copied record is a stored word.

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 persistent extension; each copied record is a stored word.

Declaration kind. def.

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

Lean code for Definition10.62.2●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    def QuantumBlockEncoding.StoredHermiteGeometry.appendLevel {m : ℕ}
  (xs :
    Vector QuantumBlockEncoding.StoredHermiteGeometry.TailLevel (m + 1))
  (last : QuantumBlockEncoding.StoredHermiteGeometry.TailLevel) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector QuantumBlockEncoding.StoredHermiteGeometry.TailLevel
      (m + 2))
    def QuantumBlockEncoding.StoredHermiteGeometry.appendLevel
  {m : ℕ}
  (xs :
    Vector
      QuantumBlockEncoding.StoredHermiteGeometry.TailLevel
      (m + 1))
  (last :
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel) :
  QuantumBlockEncoding.StoredGivens.Run
    (Vector
      QuantumBlockEncoding.StoredHermiteGeometry.TailLevel
      (m + 2))
    Full-copy persistent extension; each copied record is a stored word.
Theorem10.62.3
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “append level 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/StoredHermiteGeometry.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.62.3●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.appendLevel_value {m : ℕ}
  (xs :
    Vector QuantumBlockEncoding.StoredHermiteGeometry.TailLevel (m + 1))
  (last : QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (i : Fin (m + 2)) :
  (QuantumBlockEncoding.StoredHermiteGeometry.appendLevel xs
          last).value[↑i] =
    if h : ↑i < m + 1 then xs[↑i] else last
    theorem QuantumBlockEncoding.StoredHermiteGeometry.appendLevel_value
  {m : ℕ}
  (xs :
    Vector
      QuantumBlockEncoding.StoredHermiteGeometry.TailLevel
      (m + 1))
  (last :
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (i : Fin (m + 2)) :
  (QuantumBlockEncoding.StoredHermiteGeometry.appendLevel
          xs last).value[↑i] =
    if h : ↑i < m + 1 then xs[↑i]
    else last
Definition10.62.4
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “halve”. Repeated charged division, never an uncharged cast of 2^n.

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. Repeated charged division, never an uncharged cast of 2^n.

Declaration kind. def.

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

Lean code for Definition10.62.4●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    def QuantumBlockEncoding.StoredHermiteGeometry.halve :
  ℕ → ℝ → QuantumBlockEncoding.StoredGivens.Run ℝ
    def QuantumBlockEncoding.StoredHermiteGeometry.halve :
  ℕ →
    ℝ →
      QuantumBlockEncoding.StoredGivens.Run
        ℝ
    Repeated charged division, never an uncharged cast of 2^n.
Theorem10.62.5
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.5●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.halve_value (n : ℕ) (x : ℝ) :
  (QuantumBlockEncoding.StoredHermiteGeometry.halve n x).value =
    x / 2 ^ n
    theorem QuantumBlockEncoding.StoredHermiteGeometry.halve_value
  (n : ℕ) (x : ℝ) :
  (QuantumBlockEncoding.StoredHermiteGeometry.halve
        n x).value =
    x / 2 ^ n
Theorem10.62.6
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.6●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.halve_cost (n : ℕ) (x : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.halve n x).cost op =
    n *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field op
    theorem QuantumBlockEncoding.StoredHermiteGeometry.halve_cost
  (n : ℕ) (x : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.halve
          n x).cost
      op =
    n *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field
        op
Definition10.62.7
uses 0used by 0✓L∃∀N

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

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/StoredHermiteGeometry.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.62.7●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    def QuantumBlockEncoding.StoredHermiteGeometry.step (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ
    def QuantumBlockEncoding.StoredHermiteGeometry.step
  (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredGivens.Run ℝ
Theorem10.62.8
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/StoredHermiteGeometry.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.62.8●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.step_value (n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteGeometry.step n L).value =
    QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L
    theorem QuantumBlockEncoding.StoredHermiteGeometry.step_value
  (n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteGeometry.step
        n L).value =
    QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
      n L
Theorem10.62.9
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.9●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.step_cost (n : ℕ) (L : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.step n L).cost op =
    (n + 1) *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field op
    theorem QuantumBlockEncoding.StoredHermiteGeometry.step_cost
  (n : ℕ) (L : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.step
          n L).cost
      op =
    (n + 1) *
      QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.field
        op
Theorem10.62.10
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “root width”; the hypotheses and conclusion in the code panel fix its exact scope. Public root-width identity for geometry integration.

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. Public root-width identity for geometry integration.

Declaration kind. theorem.

Source: QuantumBlockEncoding/StoredHermiteGeometry.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.62.10●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.root_width (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L * 2 ^ n =
    Real.pi * L
    theorem QuantumBlockEncoding.StoredHermiteGeometry.root_width
  (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
        n L *
      2 ^ n =
    Real.pi * L
    Public root-width identity for geometry integration.
Definition10.62.11
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “tails”. One exponential is evaluated and stored per level.

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. One exponential is evaluated and stored per level. The same factor is shared by the left zero-bit and right one-bit transitions.

Declaration kind. def.

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

Lean code for Definition10.62.11●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    def QuantumBlockEncoding.StoredHermiteGeometry.tails (grid : ℝ) (n : ℕ) :
  QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
    (Vector QuantumBlockEncoding.StoredHermiteGeometry.TailLevel
      (n + 1))
    def QuantumBlockEncoding.StoredHermiteGeometry.tails
  (grid : ℝ) (n : ℕ) :
  QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
    (Vector
      QuantumBlockEncoding.StoredHermiteGeometry.TailLevel
      (n + 1))
    One exponential is evaluated and stored per level. The same factor is
shared by the left zero-bit and right one-bit transitions.
Theorem10.62.12
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.12●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tails_value (grid : ℝ)
  (n : ℕ) (r : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tails grid
                n).run.value[↑r].width =
      grid * 2 ^ ↑r ∧
    (QuantumBlockEncoding.StoredHermiteGeometry.tails grid
                n).run.value[↑r].factor =
      Real.exp (-grid * 2 ^ ↑r)
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tails_value
  (grid : ℝ) (n : ℕ) (r : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tails
                grid
                n).run.value[↑r].width =
      grid * 2 ^ ↑r ∧
    (QuantumBlockEncoding.StoredHermiteGeometry.tails
                grid
                n).run.value[↑r].factor =
      Real.exp (-grid * 2 ^ ↑r)
Theorem10.62.13
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.13●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tails_exponentialCalls
  (grid : ℝ) (n : ℕ) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tails grid
        n).exponentialCalls =
    n + 1
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tails_exponentialCalls
  (grid : ℝ) (n : ℕ) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tails
        grid n).exponentialCalls =
    n + 1
Theorem10.62.14
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “append level 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/StoredHermiteGeometry.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.62.14●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.appendLevel_cost_le {m : ℕ}
  (xs :
    Vector QuantumBlockEncoding.StoredHermiteGeometry.TailLevel (m + 1))
  (last : QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.appendLevel xs last).cost
      op ≤
    6 * (m + 2)
    theorem QuantumBlockEncoding.StoredHermiteGeometry.appendLevel_cost_le
  {m : ℕ}
  (xs :
    Vector
      QuantumBlockEncoding.StoredHermiteGeometry.TailLevel
      (m + 1))
  (last :
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.appendLevel
          xs last).cost
      op ≤
    6 * (m + 2)
Theorem10.62.15
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.15●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tails_cost_le (grid : ℝ)
  (n : ℕ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tails grid n).run.cost
      op ≤
    12 * (n + 1) ^ 2
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tails_cost_le
  (grid : ℝ) (n : ℕ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tails
            grid n).run.cost
      op ≤
    12 * (n + 1) ^ 2
Definition10.62.16
uses 0used by 0✓L∃∀N

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

Formal status. Data contract in the default import surface; proposition-valued fields are obligations, not automatically established facts.

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

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

Declaration kind. structure.

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

Lean code for Definition10.62.16●1 definition
  • structure(3 fields)defined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    structure QuantumBlockEncoding.StoredHermiteGeometry.TailCache (n : ℕ) : Type
    structure QuantumBlockEncoding.StoredHermiteGeometry.TailCache
  (n : ℕ) : Type

    Fields

    cutoff : ℕ
    grid : ℝ
    levels : Vector QuantumBlockEncoding.StoredHermiteGeometry.TailLevel (n + 1)
Definition10.62.17
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “tail cache”. The actual binary-search cutoff and actual width cache are supplied in the same run.

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 binary-search cutoff and actual width cache are supplied in the same run. No precomputed cutoff or coordinate callback is an input.

Declaration kind. def.

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

Lean code for Definition10.62.17●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    def QuantumBlockEncoding.StoredHermiteGeometry.tailCache (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
    (QuantumBlockEncoding.StoredHermiteGeometry.TailCache n)
    def QuantumBlockEncoding.StoredHermiteGeometry.tailCache
  (n : ℕ) (L : ℝ) :
  QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
    (QuantumBlockEncoding.StoredHermiteGeometry.TailCache
      n)
    The actual binary-search cutoff and actual width cache are supplied in
the same run. No precomputed cutoff or coordinate callback is an input.
Theorem10.62.18
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.18●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tailCache_value (n : ℕ)
  (L : ℝ) (hL : 0 < L) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
              L).run.value.cutoff =
      QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L ∧
    (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                L).run.value.grid =
        QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L ∧
      ∀ (r : Fin (n + 1)),
        (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                        L).run.value.levels[↑r].width =
            QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L *
              2 ^ ↑r ∧
          (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                        L).run.value.levels[↑r].factor =
            Real.exp
              (-QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n
                    L *
                2 ^ ↑r)
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tailCache_value
  (n : ℕ) (L : ℝ) (hL : 0 < L) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
              n L).run.value.cutoff =
      QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
        n L ∧
    (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                n L).run.value.grid =
        QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
          n L ∧
      ∀ (r : Fin (n + 1)),
        (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                        n
                        L).run.value.levels[↑r].width =
            QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
                n L *
              2 ^ ↑r ∧
          (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                        n
                        L).run.value.levels[↑r].factor =
            Real.exp
              (-QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
                    n L *
                2 ^ ↑r)
Theorem10.62.19
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tail cache 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/StoredHermiteGeometry.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.62.19●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tailCache_exponentialCalls
  (n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
        L).exponentialCalls =
    n + 1
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tailCache_exponentialCalls
  (n : ℕ) (L : ℝ) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
        n L).exponentialCalls =
    n + 1
Theorem10.62.20
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.20●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tailCache_cost_le (n : ℕ)
  (L : ℝ) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n L).run.cost
      op ≤
    16 * (n + 1) ^ 2
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tailCache_cost_le
  (n : ℕ) (L : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
            n L).run.cost
      op ≤
    16 * (n + 1) ^ 2
Theorem10.62.21
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.21●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tailCache_total_cost_le
  (n : ℕ) (L : ℝ) :
  ∑ op,
      (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
              L).run.cost
        op ≤
    128 * (n + 1) ^ 2
    theorem QuantumBlockEncoding.StoredHermiteGeometry.tailCache_total_cost_le
  (n : ℕ) (L : ℝ) :
  ∑ op,
      (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
              n L).run.cost
        op ≤
    128 * (n + 1) ^ 2
Definition10.62.22
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “at stage”. The cache is physically indexed by r, but consumers use chronological source stage t=0,...,n and access r=n-t with a charged stored-word read.

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 cache is physically indexed by r, but consumers use chronological source stage t=0,...,n and access r=n-t with a charged stored-word read.

Declaration kind. def.

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

Lean code for Definition10.62.22●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    def QuantumBlockEncoding.StoredHermiteGeometry.atStage {n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteGeometry.TailCache n)
  (t : Fin (n + 1)) :
  QuantumBlockEncoding.StoredGivens.Run
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel
    def QuantumBlockEncoding.StoredHermiteGeometry.atStage
  {n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteGeometry.TailCache
      n)
  (t : Fin (n + 1)) :
  QuantumBlockEncoding.StoredGivens.Run
    QuantumBlockEncoding.StoredHermiteGeometry.TailLevel
    The cache is physically indexed by r, but consumers use chronological
source stage t=0,...,n and access r=n-t with a charged stored-word read.
Theorem10.62.23
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “at stage 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/StoredHermiteGeometry.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.62.23●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_value (n : ℕ) (L : ℝ)
  (hL : 0 < L) (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                  L).run.value
            t).value.width =
      QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L *
        2 ^ (n - ↑t) ∧
    (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                  L).run.value
            t).value.factor =
      Real.exp
        (-QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L *
          2 ^ (n - ↑t))
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_value
  (n : ℕ) (L : ℝ) (hL : 0 < L)
  (t : Fin (n + 1)) :
  (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                  n L).run.value
            t).value.width =
      QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
          n L *
        2 ^ (n - ↑t) ∧
    (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                  n L).run.value
            t).value.factor =
      Real.exp
        (-QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
              n L *
          2 ^ (n - ↑t))
Theorem10.62.24
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.24●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_cost {n : ℕ}
  (cache : QuantumBlockEncoding.StoredHermiteGeometry.TailCache n)
  (t : Fin (n + 1)) (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.atStage cache t).cost op =
    QuantumBlockEncoding.StoredGivens.tick
      QuantumBlockEncoding.StoredGivens.Op.read op
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_cost
  {n : ℕ}
  (cache :
    QuantumBlockEncoding.StoredHermiteGeometry.TailCache
      n)
  (t : Fin (n + 1))
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.atStage
          cache t).cost
      op =
    QuantumBlockEncoding.StoredGivens.tick
      QuantumBlockEncoding.StoredGivens.Op.read
      op
Theorem10.62.25
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.25●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_leftFree (n : ℕ)
  (L : ℝ) (hL : 0 < L) (t : Fin (n + 1)) (bit : Bool) :
  (if bit = true then 1
    else
      (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                  L).run.value
            t).value.factor) =
    QuantumBlockEncoding.HermiteBoundaryInjection.leftFree
      (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L)
      (n - ↑t) bit
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_leftFree
  (n : ℕ) (L : ℝ) (hL : 0 < L)
  (t : Fin (n + 1)) (bit : Bool) :
  (if bit = true then 1
    else
      (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                  n L).run.value
            t).value.factor) =
    QuantumBlockEncoding.HermiteBoundaryInjection.leftFree
      (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
        n L)
      (n - ↑t) bit
Theorem10.62.26
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “at stage right free”; 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/StoredHermiteGeometry.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.62.26●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_rightFree (n : ℕ)
  (L : ℝ) (hL : 0 < L) (t : Fin (n + 1)) (bit : Bool) :
  (if bit = true then
      (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                  L).run.value
            t).value.factor
    else 1) =
    QuantumBlockEncoding.HermiteBoundaryInjection.rightFree
      (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L)
      (n - ↑t) bit
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_rightFree
  (n : ℕ) (L : ℝ) (hL : 0 < L)
  (t : Fin (n + 1)) (bit : Bool) :
  (if bit = true then
      (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                  n L).run.value
            t).value.factor
    else 1) =
    QuantumBlockEncoding.HermiteBoundaryInjection.rightFree
      (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
        n L)
      (n - ↑t) bit
Theorem10.62.27
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.27●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_rightCore (n : ℕ)
  (L : ℝ) (hL : 0 < L) (t : Fin (n + 1)) (bit : Bool) :
  (if ↑t = 0 then if bit = true then 1 else 0
    else
      if bit = true then
        (QuantumBlockEncoding.StoredHermiteGeometry.atStage
              (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                    L).run.value
              t).value.factor
      else 1) =
    QuantumBlockEncoding.HermiteBoundaryInjection.rightCore n
      (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L)
      (n - ↑t) bit
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_rightCore
  (n : ℕ) (L : ℝ) (hL : 0 < L)
  (t : Fin (n + 1)) (bit : Bool) :
  (if ↑t = 0 then
      if bit = true then 1 else 0
    else
      if bit = true then
        (QuantumBlockEncoding.StoredHermiteGeometry.atStage
              (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                    n L).run.value
              t).value.factor
      else 1) =
    QuantumBlockEncoding.HermiteBoundaryInjection.rightCore
      n
      (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
        n L)
      (n - ↑t) bit
Theorem10.62.28
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.28●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_bounds (n : ℕ)
  (L : ℝ) (hL : 0 < L) (t : Fin (n + 1)) :
  0 ≤
      (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                  L).run.value
            t).value.factor ∧
    (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache n
                  L).run.value
            t).value.factor ≤
      1
    theorem QuantumBlockEncoding.StoredHermiteGeometry.atStage_bounds
  (n : ℕ) (L : ℝ) (hL : 0 < L)
  (t : Fin (n + 1)) :
  0 ≤
      (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                  n L).run.value
            t).value.factor ∧
    (QuantumBlockEncoding.StoredHermiteGeometry.atStage
            (QuantumBlockEncoding.StoredHermiteGeometry.tailCache
                  n L).run.value
            t).value.factor ≤
      1
Definition10.62.29
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “left injection”. A disabled injection performs no scalar arithmetic and no 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. A disabled injection performs no scalar arithmetic and no exponential. An enabled injection uses the cached child's excluded endpoint minus one grid step. The enabling Full guard is supplied by the geometry cache.

Declaration kind. def.

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

Lean code for Definition10.62.29●1 definition
  • defdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    def QuantumBlockEncoding.StoredHermiteGeometry.leftInjection
  (enabled : Bool) (lower width grid : ℝ) :
  QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun ℝ
    def QuantumBlockEncoding.StoredHermiteGeometry.leftInjection
  (enabled : Bool)
  (lower width grid : ℝ) :
  QuantumBlockEncoding.StoredHermiteCoefficients.SourceRun
    ℝ
    A disabled injection performs no scalar arithmetic and no exponential.
An enabled injection uses the cached child's excluded endpoint minus one
grid step. The enabling Full guard is supplied by the geometry cache.
Theorem10.62.30
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.30●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.leftInjection_value
  (enabled : Bool) (origin grid lower width : ℝ) (first r : ℕ)
  (hl :
    lower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        grid first)
  (hw : width = grid * 2 ^ r) :
  (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection enabled
          lower width grid).run.value =
    if enabled = true then
      QuantumBlockEncoding.HermiteBoundaryInjection.leftInject origin
        grid first r
    else 0
    theorem QuantumBlockEncoding.StoredHermiteGeometry.leftInjection_value
  (enabled : Bool)
  (origin grid lower width : ℝ)
  (first r : ℕ)
  (hl :
    lower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin grid first)
  (hw : width = grid * 2 ^ r) :
  (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection
          enabled lower width
          grid).run.value =
    if enabled = true then
      QuantumBlockEncoding.HermiteBoundaryInjection.leftInject
        origin grid first r
    else 0
Theorem10.62.31
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.31●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.leftInjection_lastPoint
  (origin grid lower width : ℝ) (first r : ℕ)
  (hl :
    lower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        grid first)
  (hw : width = grid * 2 ^ r) :
  (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection true lower
          width grid).run.value =
    Real.exp
      (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint origin
        grid (first + 2 ^ r - 1))
    theorem QuantumBlockEncoding.StoredHermiteGeometry.leftInjection_lastPoint
  (origin grid lower width : ℝ)
  (first r : ℕ)
  (hl :
    lower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin grid first)
  (hw : width = grid * 2 ^ r) :
  (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection
          true lower width
          grid).run.value =
    Real.exp
      (QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        origin grid (first + 2 ^ r - 1))
Theorem10.62.32
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.32●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.leftInjection_exponentialCalls
  (enabled : Bool) (lower width grid : ℝ) :
  (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection enabled
        lower width grid).exponentialCalls =
    if enabled = true then 1 else 0
    theorem QuantumBlockEncoding.StoredHermiteGeometry.leftInjection_exponentialCalls
  (enabled : Bool)
  (lower width grid : ℝ) :
  (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection
        enabled lower width
        grid).exponentialCalls =
    if enabled = true then 1 else 0
Theorem10.62.33
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.33●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.leftInjection_cost
  (enabled : Bool) (lower width grid : ℝ)
  (op : QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection enabled
            lower width grid).run.cost
      op =
    QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.compare op +
      if enabled = true then
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field op
      else 0
    theorem QuantumBlockEncoding.StoredHermiteGeometry.leftInjection_cost
  (enabled : Bool) (lower width grid : ℝ)
  (op :
    QuantumBlockEncoding.StoredGivens.Op) :
  (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection
            enabled lower width
            grid).run.cost
      op =
    QuantumBlockEncoding.StoredGivens.tick
        QuantumBlockEncoding.StoredGivens.Op.compare
        op +
      if enabled = true then
        2 *
          QuantumBlockEncoding.StoredGivens.tick
            QuantumBlockEncoding.StoredGivens.Op.field
            op
      else 0
Theorem10.62.34
uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.62.34●1 theorem
  • theoremdefined in QuantumBlockEncoding/StoredHermiteGeometry.lean
    complete
    theorem QuantumBlockEncoding.StoredHermiteGeometry.leftInjection_bounds (n : ℕ)
  (L : ℝ) (hL : 0 < L) (enabled : Bool) (lower width : ℝ) (first r : ℕ)
  (hl :
    lower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        (-Real.pi * L)
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L)
        first)
  (hw :
    width =
      QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n L *
        2 ^ r)
  (guard :
    enabled = true →
      QuantumBlockEncoding.HermiteBoundaryInjection.Full 0
        (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex n L)
        first (2 ^ r)) :
  0 ≤
      (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection enabled
            lower width
            (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n
              L)).run.value ∧
    (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection enabled
            lower width
            (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep n
              L)).run.value ≤
      1
    theorem QuantumBlockEncoding.StoredHermiteGeometry.leftInjection_bounds
  (n : ℕ) (L : ℝ) (hL : 0 < L)
  (enabled : Bool) (lower width : ℝ)
  (first r : ℕ)
  (hl :
    lower =
      QuantumBlockEncoding.HermiteBoundaryInjection.affinePoint
        (-Real.pi * L)
        (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
          n L)
        first)
  (hw :
    width =
      QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
          n L *
        2 ^ r)
  (guard :
    enabled = true →
      QuantumBlockEncoding.HermiteBoundaryInjection.Full
        0
        (QuantumBlockEncoding.HermiteBoundaryInjection.cutIndex
          n L)
        first (2 ^ r)) :
  0 ≤
      (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection
            enabled lower width
            (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
              n L)).run.value ∧
    (QuantumBlockEncoding.StoredHermiteGeometry.leftInjection
            enabled lower width
            (QuantumBlockEncoding.HermiteBoundaryInjection.gridStep
              n L)).run.value ≤
      1