ASPBE Lean Blueprint

10.1. QuantumBlockEncoding/Examples/RobinHeat.lean🔗

12 explicit public declarations, in source order.

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

Plain-English reading. This definition gives the library's named construction or computation for “fourth order second derivative”.

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 and concrete Robin-boundary 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/Examples/RobinHeat.lean:18. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.1.1●1 definition
  • defdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    def QuantumBlockEncoding.Examples.RobinHeat.fourthOrderSecondDerivative :
  QuantumBlockEncoding.Stencil
    def QuantumBlockEncoding.Examples.RobinHeat.fourthOrderSecondDerivative :
  QuantumBlockEncoding.Stencil
Definition10.1.2
uses 0used by 0✓L∃∀N

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

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 and concrete Robin-boundary 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/Examples/RobinHeat.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.1.2●1 definition
  • defdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    def QuantumBlockEncoding.Examples.RobinHeat.centralBulkEntries :
  List QuantumBlockEncoding.StencilEntry
    def QuantumBlockEncoding.Examples.RobinHeat.centralBulkEntries :
  List QuantumBlockEncoding.StencilEntry
Definition10.1.3
uses 0used by 0✓L∃∀N

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

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 and concrete Robin-boundary 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/Examples/RobinHeat.lean:33. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.1.3●1 definition
  • defdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    def QuantumBlockEncoding.Examples.RobinHeat.A1dx :
  QuantumBlockEncoding.Coeff
    def QuantumBlockEncoding.Examples.RobinHeat.A1dx :
  QuantumBlockEncoding.Coeff
Definition10.1.4
uses 0used by 0✓L∃∀N

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

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 and concrete Robin-boundary 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/Examples/RobinHeat.lean:34. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.1.4●1 definition
  • defdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    def QuantumBlockEncoding.Examples.RobinHeat.B1dx :
  QuantumBlockEncoding.Coeff
    def QuantumBlockEncoding.Examples.RobinHeat.B1dx :
  QuantumBlockEncoding.Coeff
Definition10.1.5
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “left boundary row 0”. First row after eliminating the left Robin ghost points.

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 and concrete Robin-boundary example artifacts.

Technical source note. First row after eliminating the left Robin ghost points.

Declaration kind. def.

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

Lean code for Definition10.1.5●1 definition
  • defdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    def QuantumBlockEncoding.Examples.RobinHeat.leftBoundaryRow0 :
  List QuantumBlockEncoding.StencilEntry
    def QuantumBlockEncoding.Examples.RobinHeat.leftBoundaryRow0 :
  List QuantumBlockEncoding.StencilEntry
    First row after eliminating the left Robin ghost points.
Definition10.1.6
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “left boundary row 1”. Second row after eliminating the left Robin ghost points.

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 and concrete Robin-boundary example artifacts.

Technical source note. Second row after eliminating the left Robin ghost points.

Declaration kind. def.

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

Lean code for Definition10.1.6●1 definition
  • defdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    def QuantumBlockEncoding.Examples.RobinHeat.leftBoundaryRow1 :
  List QuantumBlockEncoding.StencilEntry
    def QuantumBlockEncoding.Examples.RobinHeat.leftBoundaryRow1 :
  List QuantumBlockEncoding.StencilEntry
    Second row after eliminating the left Robin ghost points.
Definition10.1.7
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “right boundary row nm 2”. Penultimate row after eliminating the right Robin ghost points.

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 and concrete Robin-boundary example artifacts.

Technical source note. Penultimate row after eliminating the right Robin ghost points.

Declaration kind. def.

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

Lean code for Definition10.1.7●1 definition
  • defdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    def QuantumBlockEncoding.Examples.RobinHeat.rightBoundaryRowNm2 :
  List QuantumBlockEncoding.StencilEntry
    def QuantumBlockEncoding.Examples.RobinHeat.rightBoundaryRowNm2 :
  List QuantumBlockEncoding.StencilEntry
    Penultimate row after eliminating the right Robin ghost points.
Definition10.1.8
uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “right boundary row nm 1”. Last row after eliminating the right Robin ghost points.

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 and concrete Robin-boundary example artifacts.

Technical source note. Last row after eliminating the right Robin ghost points.

Declaration kind. def.

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

Lean code for Definition10.1.8●1 definition
  • defdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    def QuantumBlockEncoding.Examples.RobinHeat.rightBoundaryRowNm1 :
  List QuantumBlockEncoding.StencilEntry
    def QuantumBlockEncoding.Examples.RobinHeat.rightBoundaryRowNm1 :
  List QuantumBlockEncoding.StencilEntry
    Last row after eliminating the right Robin ghost points.
Definition10.1.9
uses 0used by 0✓L∃∀N

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

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 and concrete Robin-boundary 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/Examples/RobinHeat.lean:70. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.1.9●1 definition
  • defdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    def QuantumBlockEncoding.Examples.RobinHeat.robinWindow (n : ℕ) :
  QuantumBlockEncoding.BulkWindow
    def QuantumBlockEncoding.Examples.RobinHeat.robinWindow
  (n : ℕ) :
  QuantumBlockEncoding.BulkWindow
Definition10.1.10
uses 0used by 0✓L∃∀N

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

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 and concrete Robin-boundary 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/Examples/RobinHeat.lean:74. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Definition10.1.10●1 definition
  • defdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    def QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters (n : ℕ) :
  QuantumBlockEncoding.GHL2025.OneTermRobinParameters
    def QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters
  (n : ℕ) :
  QuantumBlockEncoding.GHL2025.OneTermRobinParameters
Theorem10.1.11
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “fourth order stencil width”; 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 and concrete Robin-boundary 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/Examples/RobinHeat.lean:80. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.1.11●1 theorem
  • theoremdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    theorem QuantumBlockEncoding.Examples.RobinHeat.fourthOrderStencilWidth :
  QuantumBlockEncoding.Examples.RobinHeat.fourthOrderSecondDerivative.width =
    5
    theorem QuantumBlockEncoding.Examples.RobinHeat.fourthOrderStencilWidth :
  QuantumBlockEncoding.Examples.RobinHeat.fourthOrderSecondDerivative.width =
    5
Theorem10.1.12
uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “robin heat ancillas”; 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 and concrete Robin-boundary 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/Examples/RobinHeat.lean:83. A commit-pinned external link is added by the publication build when the source exists at the published ref.

Lean code for Theorem10.1.12●1 theorem
  • theoremdefined in QuantumBlockEncoding/Examples/RobinHeat.lean
    complete
    theorem QuantumBlockEncoding.Examples.RobinHeat.robinHeatAncillas (n : ℕ) :
  (QuantumBlockEncoding.GHL2025.oneTermRobinResource
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters
          n)).pureAncilla =
    2 * n
    theorem QuantumBlockEncoding.Examples.RobinHeat.robinHeatAncillas
  (n : ℕ) :
  (QuantumBlockEncoding.GHL2025.oneTermRobinResource
        (QuantumBlockEncoding.Examples.RobinHeat.oneTermParameters
          n)).pureAncilla =
    2 * n