10.3. QuantumBlockEncoding/GHLHamiltonian.lean🔗

64 explicit public declarations, in source order.

Theorem10.3.1

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “conj two”; the hypotheses and conclusion in the code panel fix its exact scope. Complex conjugation fixes the real scalar two.

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. Complex conjugation fixes the real scalar two.

Declaration kind. theorem.

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

Lean code for Theorem10.3.1●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.conj_two :
  (starRingEnd ℂ) 2 = 2

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.conj_two :
  (starRingEnd ℂ) 2 = 2

Complex conjugation fixes the real scalar two.

Definition10.3.2

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “c matrix”. Complex finite matrix with arbitrary finite basis type.

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. Complex finite matrix with arbitrary finite basis type.

Declaration kind. abbrev.

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

abbrevdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

abbrev QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix.{u_1, u_2}
  (ι : Type u_1) (κ : Type u_2) : Type (max u_1 u_2)

abbrev QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix.{u_1,
    u_2}
  (ι : Type u_1) (κ : Type u_2) :
  Type (max u_1 u_2)

Complex finite matrix with arbitrary finite basis type.

Definition10.3.3

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “add”. Entrywise addition, kept explicit so source formulas remain readable.

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. Entrywise addition, kept explicit so source formulas remain readable.

Declaration kind. def.

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

Lean code for Definition10.3.3●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.add.{u_1, u_2} {ι : Type u_1}
  {κ : Type u_2}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι κ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι κ

def QuantumBlockEncoding.GHL2025.Hamiltonian.add.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι κ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ι κ

Entrywise addition, kept explicit so source formulas remain readable.

Definition10.3.4

uses 0used by 0✓L∃∀N

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

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. Entrywise subtraction.

Declaration kind. def.

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

Lean code for Definition10.3.4●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.sub.{u_1, u_2} {ι : Type u_1}
  {κ : Type u_2}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι κ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι κ

def QuantumBlockEncoding.GHL2025.Hamiltonian.sub.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι κ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ι κ

Entrywise subtraction.

Definition10.3.5

uses 0used by 0✓L∃∀N

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

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. Scalar multiplication.

Declaration kind. def.

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

Lean code for Definition10.3.5●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.scale.{u_1, u_2} {ι : Type u_1}
  {κ : Type u_2} (c : ℂ)
  (A : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι κ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι κ

def QuantumBlockEncoding.GHL2025.Hamiltonian.scale.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2} (c : ℂ)
  (A :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι κ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ι κ

Scalar multiplication.

Definition10.3.6

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “adjoint”. The matrix adjoint written directly as conjugate transpose.

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 matrix adjoint written directly as conjugate transpose.

Declaration kind. def.

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

Lean code for Definition10.3.6●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint.{u_1} {ι : Type u_1}
  (A : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι

def QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint.{u_1}
  {ι : Type u_1}
  (A :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ι ι

The matrix adjoint written directly as conjugate transpose.

Definition10.3.7

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “is hermitian”. Source-level Hermitian predicate.

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. Source-level Hermitian predicate.

Declaration kind. def.

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

Lean code for Definition10.3.7●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian.{u_1}
  {ι : Type u_1}
  (A : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) : Prop

def QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian.{u_1}
  {ι : Type u_1}
  (A :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  Prop

Source-level Hermitian predicate.

Definition10.3.8

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “hermitian part”. The Hermitian part '(A + A†)/2'.

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 Hermitian part '(A + A†)/2'.

Declaration kind. def.

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

Lean code for Definition10.3.8●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.hermitianPart.{u_1}
  {ι : Type u_1}
  (A : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι

def QuantumBlockEncoding.GHL2025.Hamiltonian.hermitianPart.{u_1}
  {ι : Type u_1}
  (A :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ι ι

The Hermitian part `(A + A†)/2`.

Definition10.3.9

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “anti hermitian part”. The second Hermitian piece '(A - A†)/(2i)'.

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 second Hermitian piece '(A - A†)/(2i)'.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.antiHermitianPart.{u_1}
  {ι : Type u_1}
  (A : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι

def QuantumBlockEncoding.GHL2025.Hamiltonian.antiHermitianPart.{u_1}
  {ι : Type u_1}
  (A :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ι ι

The second Hermitian piece `(A - A†)/(2i)`.

Theorem10.3.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermitian decomposition”; the hypotheses and conclusion in the code panel fix its exact scope. The two canonical pieces reconstruct the original matrix.

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 two canonical pieces reconstruct the original matrix.

Declaration kind. theorem.

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

Lean code for Theorem10.3.10●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.hermitian_decomposition.{u_1}
  {ι : Type u_1}
  (A : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) (i j : ι) :
  A i j =
    QuantumBlockEncoding.GHL2025.Hamiltonian.hermitianPart A i j +
      Complex.I *
        QuantumBlockEncoding.GHL2025.Hamiltonian.antiHermitianPart A i j

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.hermitian_decomposition.{u_1}
  {ι : Type u_1}
  (A :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (i j : ι) :
  A i j =
    QuantumBlockEncoding.GHL2025.Hamiltonian.hermitianPart
        A i j +
      Complex.I *
        QuantumBlockEncoding.GHL2025.Hamiltonian.antiHermitianPart
          A i j

The two canonical pieces reconstruct the original matrix.

Theorem10.3.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermitian part is hermitian”; the hypotheses and conclusion in the code panel fix its exact scope. '(A + A†)/2' is Hermitian for every complex matrix 'A'.

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. '(A + A†)/2' is Hermitian for every complex matrix 'A'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.11●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.hermitianPart_isHermitian.{u_1}
  {ι : Type u_1}
  (A : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.hermitianPart A)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.hermitianPart_isHermitian.{u_1}
  {ι : Type u_1}
  (A :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.hermitianPart
      A)

`(A + A†)/2` is Hermitian for every complex matrix `A`.

Theorem10.3.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “anti hermitian part is hermitian”; the hypotheses and conclusion in the code panel fix its exact scope. '(A - A†)/(2i)' is Hermitian for every complex matrix 'A'.

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. '(A - A†)/(2i)' is Hermitian for every complex matrix 'A'.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.antiHermitianPart_isHermitian.{u_1}
  {ι : Type u_1}
  (A : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.antiHermitianPart A)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.antiHermitianPart_isHermitian.{u_1}
  {ι : Type u_1}
  (A :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.antiHermitianPart
      A)

`(A - A†)/(2i)` is Hermitian for every complex matrix `A`.

Definition10.3.13

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “sum terms”. Sum of the paper's one-term matrices 'A_k'.

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. Sum of the paper's one-term matrices 'A_k'.

Declaration kind. def.

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

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms.{u_1, u_2}
  {ι : Type u_2} {η : Type u_1} [Fintype η]
  (terms : η → QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι

def QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms.{u_1,
    u_2}
  {ι : Type u_2} {η : Type u_1}
  [Fintype η]
  (terms :
    η →
      QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
        ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ι ι

Sum of the paper's one-term matrices `A_k`.

Theorem10.3.14

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.3.14●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms_entry.{u_1, u_2}
  {ι : Type u_2} {η : Type u_1} [Fintype η]
  (terms : η → QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms terms i j =
    ∑ k, terms k i j

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms_entry.{u_1,
    u_2}
  {ι : Type u_2} {η : Type u_1}
  [Fintype η]
  (terms :
    η →
      QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
        ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms
      terms i j =
    ∑ k, terms k i j

Theorem10.3.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “adjoint sum terms”; the hypotheses and conclusion in the code panel fix its exact scope. Taking the adjoint commutes with the paper's finite sum of one-term matrices.

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. Taking the adjoint commutes with the paper's finite sum of one-term matrices.

Declaration kind. theorem.

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

Lean code for Theorem10.3.15●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint_sumTerms.{u_1, u_2}
  {ι : Type u_2} {η : Type u_1} [Fintype η]
  (terms : η → QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint
      (QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms terms) =
    QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms fun k =>
      QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint (terms k)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint_sumTerms.{u_1,
    u_2}
  {ι : Type u_2} {η : Type u_1}
  [Fintype η]
  (terms :
    η →
      QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
        ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint
      (QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms
        terms) =
    QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms
      fun k =>
      QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint
        (terms k)

Taking the adjoint commutes with the paper's finite sum of one-term matrices.

Definition10.3.16

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “homogenized s”. Homogenized matrix from the paper, on the direct-sum basis 'ι ⊕ ι': 'S = [[A,B],[0,0]]'.

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. Homogenized matrix from the paper, on the direct-sum basis 'ι ⊕ ι': 'S = [[A,B],[0,0]]'.

Declaration kind. def.

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

Lean code for Definition10.3.16●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.homogenizedS.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.homogenizedS.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

Homogenized matrix from the paper, on the direct-sum basis `ι ⊕ ι`:
`S = [[A,B],[0,0]]`.

Definition10.3.17

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “s 1”. 'S₁ = (S + S†)/2'.

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. 'S₁ = (S + S†)/2'.

Declaration kind. def.

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

Lean code for Definition10.3.17●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.S1.{u_1} {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.S1.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

`S₁ = (S + S†)/2`.

Definition10.3.18

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “s 2”. 'S₂ = (S - S†)/(2i)'.

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. 'S₂ = (S - S†)/(2i)'.

Declaration kind. def.

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

Lean code for Definition10.3.18●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.S2.{u_1} {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.S2.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

`S₂ = (S - S†)/(2i)`.

Theorem10.3.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “homogenized s eq s 1 add i s 2”; the hypotheses and conclusion in the code panel fix its exact scope. The homogenized matrix is exactly 'S₁ + i S₂'.

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 homogenized matrix is exactly 'S₁ + i S₂'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.19●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.homogenizedS_eq_S1_add_iS2.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (i j : ι ⊕ ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.homogenizedS A B i j =
    QuantumBlockEncoding.GHL2025.Hamiltonian.S1 A B i j +
      Complex.I * QuantumBlockEncoding.GHL2025.Hamiltonian.S2 A B i j

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.homogenizedS_eq_S1_add_iS2.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (i j : ι ⊕ ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.homogenizedS
      A B i j =
    QuantumBlockEncoding.GHL2025.Hamiltonian.S1
        A B i j +
      Complex.I *
        QuantumBlockEncoding.GHL2025.Hamiltonian.S2
          A B i j

The homogenized matrix is exactly `S₁ + i S₂`.

Theorem10.3.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “s 1 is hermitian”; the hypotheses and conclusion in the code panel fix its exact scope. The two Schrödingerisation pieces are Hermitian.

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 two Schrödingerisation pieces are Hermitian.

Declaration kind. theorem.

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

Lean code for Theorem10.3.20●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S1_isHermitian.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.S1 A B)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S1_isHermitian.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.S1
      A B)

The two Schrödingerisation pieces are Hermitian.

Theorem10.3.21

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.3.21●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S2_isHermitian.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.S2 A B)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S2_isHermitian.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.S2
      A B)

Theorem10.3.22

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “s 1 upper left”; the hypotheses and conclusion in the code panel fix its exact scope. Paper Eq.

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. Paper Eq. (18), upper-left block of 'S₁'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.22●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S1_upperLeft.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S1 A B (Sum.inl i)
      (Sum.inl j) =
    (A i j + (starRingEnd ℂ) (A j i)) / 2

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S1_upperLeft.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S1
      A B (Sum.inl i) (Sum.inl j) =
    (A i j + (starRingEnd ℂ) (A j i)) / 2

Paper Eq. (18), upper-left block of `S₁`.

Theorem10.3.23

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “s 1 upper right”; the hypotheses and conclusion in the code panel fix its exact scope. Paper Eq.

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. Paper Eq. (18), upper-right block of 'S₁'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.23●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S1_upperRight.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S1 A B (Sum.inl i)
      (Sum.inr j) =
    B i j / 2

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S1_upperRight.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S1
      A B (Sum.inl i) (Sum.inr j) =
    B i j / 2

Paper Eq. (18), upper-right block of `S₁`.

Theorem10.3.24

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “s 1 lower left of b hermitian”; the hypotheses and conclusion in the code panel fix its exact scope. Under the paper's Hermitian 'B', the lower-left block of 'S₁' is 'B/2'.

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. Under the paper's Hermitian 'B', the lower-left block of 'S₁' is 'B/2'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.24●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S1_lowerLeft_of_B_hermitian.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (hB : QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian B)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S1 A B (Sum.inr i)
      (Sum.inl j) =
    B i j / 2

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S1_lowerLeft_of_B_hermitian.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (hB :
    QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
      B)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S1
      A B (Sum.inr i) (Sum.inl j) =
    B i j / 2

Under the paper's Hermitian `B`, the lower-left block of `S₁` is `B/2`.

Theorem10.3.25

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “s 1 lower right”; 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/GHLHamiltonian.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.3.25●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S1_lowerRight.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S1 A B (Sum.inr i)
      (Sum.inr j) =
    0

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S1_lowerRight.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S1
      A B (Sum.inr i) (Sum.inr j) =
    0

Theorem10.3.26

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “s 2 upper left”; the hypotheses and conclusion in the code panel fix its exact scope. Paper Eq.

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. Paper Eq. (18), upper-left block of 'S₂'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.26●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S2_upperLeft.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S2 A B (Sum.inl i)
      (Sum.inl j) =
    (A i j - (starRingEnd ℂ) (A j i)) / (2 * Complex.I)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S2_upperLeft.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S2
      A B (Sum.inl i) (Sum.inl j) =
    (A i j - (starRingEnd ℂ) (A j i)) /
      (2 * Complex.I)

Paper Eq. (18), upper-left block of `S₂`.

Theorem10.3.27

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “s 2 upper right”; the hypotheses and conclusion in the code panel fix its exact scope. Paper Eq.

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. Paper Eq. (18), upper-right block of 'S₂'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.27●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S2_upperRight.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S2 A B (Sum.inl i)
      (Sum.inr j) =
    B i j / (2 * Complex.I)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S2_upperRight.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S2
      A B (Sum.inl i) (Sum.inr j) =
    B i j / (2 * Complex.I)

Paper Eq. (18), upper-right block of `S₂`.

Theorem10.3.28

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “s 2 lower left of b hermitian”; the hypotheses and conclusion in the code panel fix its exact scope. Under Hermitian 'B', the lower-left block is '-B/(2i)'.

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. Under Hermitian 'B', the lower-left block is '-B/(2i)'.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S2_lowerLeft_of_B_hermitian.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (hB : QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian B)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S2 A B (Sum.inr i)
      (Sum.inl j) =
    -B i j / (2 * Complex.I)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S2_lowerLeft_of_B_hermitian.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (hB :
    QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
      B)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S2
      A B (Sum.inr i) (Sum.inl j) =
    -B i j / (2 * Complex.I)

Under Hermitian `B`, the lower-left block is `-B/(2i)`.

Theorem10.3.29

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.3.29●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S2_lowerRight.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S2 A B (Sum.inr i)
      (Sum.inr j) =
    0

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.S2_lowerRight.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (i j : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.S2
      A B (Sum.inr i) (Sum.inr j) =
    0

Definition10.3.30

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “identity”. Matrix identity on an arbitrary finite basis.

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. Matrix identity on an arbitrary finite basis.

Declaration kind. def.

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

Lean code for Definition10.3.30●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.identity.{u_1} (ι : Type u_1)
  [DecidableEq ι] : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι

def QuantumBlockEncoding.GHL2025.Hamiltonian.identity.{u_1}
  (ι : Type u_1) [DecidableEq ι] :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ι ι

Matrix identity on an arbitrary finite basis.

Definition10.3.31

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “scaled controlled phase source”. The clean-block matrix contributed by 'N_A L₁(φ)' or 'N_A L₂(φ)' in Eq.

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 clean-block matrix contributed by 'N_A L₁(φ)' or 'N_A L₂(φ)' in Eq. (29). The upper block is already rescaled from 'A/N_A' to 'A'; the lower filler block is 'N_A e^{iφ} I'. We expose the filler because cancellation of these entries is a real source-level proof obligation in the next LCU.

Declaration kind. def.

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

Lean code for Definition10.3.31●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.scaledControlledPhaseSource.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (upper : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (normalizer phase : ℂ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.scaledControlledPhaseSource.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (upper :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (normalizer phase : ℂ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

The clean-block matrix contributed by `N_A L₁(φ)` or `N_A L₂(φ)` in Eq. (29).
The upper block is already rescaled from `A/N_A` to `A`; the lower filler block
is `N_A e^{iφ} I`.  We expose the filler because cancellation of these entries
is a real source-level proof obligation in the next LCU.

Definition10.3.32

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pauli x tensor”. 'X ⊗ B' in the paper's Eq.

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. 'X ⊗ B' in the paper's Eq. (30), written on the 'ι ⊕ ι' basis.

Declaration kind. def.

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

Lean code for Definition10.3.32●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.pauliXTensor.{u_1}
  {ι : Type u_1}
  (B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.pauliXTensor.{u_1}
  {ι : Type u_1}
  (B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

`X ⊗ B` in the paper's Eq. (30), written on the `ι ⊕ ι` basis.

Definition10.3.33

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “pauli y tensor”. 'Y ⊗ B' in the paper's Eq.

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. 'Y ⊗ B' in the paper's Eq. (30), written on the 'ι ⊕ ι' basis.

Declaration kind. def.

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

Lean code for Definition10.3.33●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.pauliYTensor.{u_1}
  {ι : Type u_1}
  (B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.pauliYTensor.{u_1}
  {ι : Type u_1}
  (B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

`Y ⊗ B` in the paper's Eq. (30), written on the `ι ⊕ ι` basis.

Definition10.3.34

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “eq 29 printed clean”. Literal clean-block algebra of the first line of the printed Eq.

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. Literal clean-block algebra of the first line of the printed Eq. (30): both filler phases are 'e^{±iπ} = -1'. The selected 'A,A†,B' entries are correct, but the lower-right filler blocks add instead of canceling.

Declaration kind. def.

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

Lean code for Definition10.3.34●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (normalizerA : ℂ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (normalizerA : ℂ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

Literal clean-block algebra of the first line of the printed Eq. (30): both
filler phases are `e^{±iπ} = -1`.  The selected `A,A†,B` entries are correct,
but the lower-right filler blocks add instead of canceling.

Definition10.3.35

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “eq 29 phase balanced clean”. Phase-balanced interpretation of the first line of Eq.

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. Phase-balanced interpretation of the first line of Eq. (30). Replacing one of the two equal 'π,-π' filler phases by phase '0' makes the irrelevant identity blocks cancel while preserving the desired 'A' and 'A†' clean blocks.

Declaration kind. def.

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

Lean code for Definition10.3.35●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (normalizerA : ℂ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (normalizerA : ℂ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

Phase-balanced interpretation of the first line of Eq. (30).  Replacing one of
the two equal `π,-π` filler phases by phase `0` makes the irrelevant identity
blocks cancel while preserving the desired `A` and `A†` clean blocks.

Theorem10.3.36

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eq 29 printed clean lower right”; the hypotheses and conclusion in the code panel fix its exact scope. The printed Eq.

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 printed Eq. (29) leaves the lower-right clean filler equal to '-N_A'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.36●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_lowerRight.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (normalizerA : ℂ) (i : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean A B
      normalizerA (Sum.inr i) (Sum.inr i) =
    -normalizerA

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_lowerRight.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (normalizerA : ℂ) (i : ι) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean
      A B normalizerA (Sum.inr i)
      (Sum.inr i) =
    -normalizerA

The printed Eq. (29) leaves the lower-right clean filler equal to `-N_A`.

Theorem10.3.37

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eq 29 printed clean ne s 1”; the hypotheses and conclusion in the code panel fix its exact scope. Therefore the literal printed phase choice cannot equal 'S₁' when 'N_A ≠ 0'.

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

Why it is in this chapter. Paper-facing backend models and concrete Robin-boundary example artifacts.

Technical source note. Therefore the literal printed phase choice cannot equal 'S₁' when 'N_A ≠ 0'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.37●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (normalizerA : ℂ) (i : ι) (hN : normalizerA ≠ 0) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean A B
      normalizerA ≠
    QuantumBlockEncoding.GHL2025.Hamiltonian.S1 A B

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean_ne_S1.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (normalizerA : ℂ) (i : ι)
  (hN : normalizerA ≠ 0) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PrintedClean
      A B normalizerA ≠
    QuantumBlockEncoding.GHL2025.Hamiltonian.S1
      A B

Therefore the literal printed phase choice cannot equal `S₁` when `N_A ≠ 0`.

Theorem10.3.38

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eq 29 phase balanced clean eq s 1”; the hypotheses and conclusion in the code panel fix its exact scope. The phase-balanced Eq.

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 phase-balanced Eq. (29) clean block is exactly the paper's 'S₁' whenever 'B' is Hermitian (in the PDE theorem 'B' is real diagonal).

Declaration kind. theorem.

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

Lean code for Theorem10.3.38●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (normalizerA : ℂ)
  (hB : QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian B) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean A B
      normalizerA =
    QuantumBlockEncoding.GHL2025.Hamiltonian.S1 A B

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean_eq_S1.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (normalizerA : ℂ)
  (hB :
    QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
      B) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean
      A B normalizerA =
    QuantumBlockEncoding.GHL2025.Hamiltonian.S1
      A B

The phase-balanced Eq. (29) clean block is exactly the paper's `S₁` whenever
`B` is Hermitian (in the PDE theorem `B` is real diagonal).

Definition10.3.39

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “eq 30 clean”. Literal clean-block algebra of the second line of Eq.

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. Literal clean-block algebra of the second line of Eq. (30).

Declaration kind. def.

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

Lean code for Definition10.3.39●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean.{u_1} {ι : Type u_1}
  [DecidableEq ι]
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (normalizerA : ℂ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (normalizerA : ℂ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

Literal clean-block algebra of the second line of Eq. (30).

Theorem10.3.40

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “eq 30 clean eq s 2”; the hypotheses and conclusion in the code panel fix its exact scope. The second line of Eq.

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 second line of Eq. (30) has the required filler cancellation and equals 'S₂'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.40●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean_eq_S2.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (normalizerA : ℂ)
  (hB : QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian B) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean A B normalizerA =
    QuantumBlockEncoding.GHL2025.Hamiltonian.S2 A B

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean_eq_S2.{u_1}
  {ι : Type u_1} [DecidableEq ι]
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (normalizerA : ℂ)
  (hB :
    QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
      B) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean
      A B normalizerA =
    QuantumBlockEncoding.GHL2025.Hamiltonian.S2
      A B

The second line of Eq. (30) has the required filler cancellation and equals `S₂`.

Theorem10.3.41

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one dim hamiltonian claim normalization closed”; the hypotheses and conclusion in the code panel fix its exact scope. Theorem 4's source normalization is registered exactly.

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. Theorem 4's source normalization is registered exactly.

Declaration kind. theorem.

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

Lean code for Theorem10.3.41●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_normalization_closed :
  QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.normalization =
    "O(kappa * ||H||_max)"

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_normalization_closed :
  QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.normalization =
    "O(kappa * ||H||_max)"

Theorem 4's source normalization is registered exactly.

Theorem10.3.42

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one dim hamiltonian claim layout closed”; the hypotheses and conclusion in the code panel fix its exact scope. Theorem 4's source signal-qubit expression is registered exactly.

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. Theorem 4's source signal-qubit expression is registered exactly.

Declaration kind. theorem.

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

Lean code for Theorem10.3.42●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_layout_closed :
  QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.layout =
    "ceil(log2 n_xi)+ceil(log2 n)+ceil(log2 G)+ceil(log2 kappa)+ceil(log2 eta)+7 signal qubits"

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_layout_closed :
  QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.layout =
    "ceil(log2 n_xi)+ceil(log2 n)+ceil(log2 G)+ceil(log2 kappa)+ceil(log2 eta)+7 signal qubits"

Theorem 4's source signal-qubit expression is registered exactly.

Theorem10.3.43

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one dim hamiltonian resource pure ancilla closed”; the hypotheses and conclusion in the code panel fix its exact scope. Theorem 4's source pure-ancilla expression is exactly '2n+2'.

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. Theorem 4's source pure-ancilla expression is exactly '2n+2'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.43●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianResource_pureAncilla_closed :
  QuantumBlockEncoding.GHL2025.oneDimHamiltonianResourceExpr.pureAncilla =
    2 * QuantumBlockEncoding.CostExpr.atom "n" + 2

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianResource_pureAncilla_closed :
  QuantumBlockEncoding.GHL2025.oneDimHamiltonianResourceExpr.pureAncilla =
    2 *
        QuantumBlockEncoding.CostExpr.atom
          "n" +
      2

Theorem 4's source pure-ancilla expression is exactly `2n+2`.

Definition10.3.44

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “tensor”. Kronecker product in explicit product-index form.

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. Kronecker product in explicit product-index form.

Declaration kind. def.

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

Lean code for Definition10.3.44●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.tensor.{u_1, u_2}
  {ι : Type u_1} {κ : Type u_2}
  (A : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix κ κ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι × κ) (ι × κ)

def QuantumBlockEncoding.GHL2025.Hamiltonian.tensor.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2}
  (A :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      κ κ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι × κ) (ι × κ)

Kronecker product in explicit product-index form.

Definition10.3.45

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “one dim hamiltonian”. The paper's one-dimensional Hamiltonian 'H = S₁⊗x_ξ + S₂⊗I_ξ'.

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 paper's one-dimensional Hamiltonian 'H = S₁⊗x_ξ + S₂⊗I_ξ'.

Declaration kind. def.

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

Lean code for Definition10.3.45●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonian.{u_1, u_2}
  {ξ : Type u_1} {ι : Type u_2} [DecidableEq ξ]
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (xXi : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ξ ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ((ι ⊕ ι) × ξ)
    ((ι ⊕ ι) × ξ)

def QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonian.{u_1,
    u_2}
  {ξ : Type u_1} {ι : Type u_2}
  [DecidableEq ξ]
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (xXi :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ξ ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ((ι ⊕ ι) × ξ) ((ι ⊕ ι) × ξ)

The paper's one-dimensional Hamiltonian `H = S₁⊗x_ξ + S₂⊗I_ξ`.

Theorem10.3.46

uses 0used by 0✓L∃∀N

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

Lean code for Theorem10.3.46●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonian_entry.{u_1,
    u_2}
  {ξ : Type u_1} {ι : Type u_2} [DecidableEq ξ]
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (xXi : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ξ ξ)
  (row col : (ι ⊕ ι) × ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonian A B xXi row
      col =
    QuantumBlockEncoding.GHL2025.Hamiltonian.S1 A B row.1 col.1 *
        xXi row.2 col.2 +
      QuantumBlockEncoding.GHL2025.Hamiltonian.S2 A B row.1 col.1 *
        if row.2 = col.2 then 1 else 0

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonian_entry.{u_1,
    u_2}
  {ξ : Type u_1} {ι : Type u_2}
  [DecidableEq ξ]
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (xXi :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ξ ξ)
  (row col : (ι ⊕ ι) × ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonian
      A B xXi row col =
    QuantumBlockEncoding.GHL2025.Hamiltonian.S1
          A B row.1 col.1 *
        xXi row.2 col.2 +
      QuantumBlockEncoding.GHL2025.Hamiltonian.S2
          A B row.1 col.1 *
        if row.2 = col.2 then 1 else 0

Theorem10.3.47

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “identity is hermitian”; the hypotheses and conclusion in the code panel fix its exact scope. The identity matrix is Hermitian.

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 identity matrix is Hermitian.

Declaration kind. theorem.

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

Lean code for Theorem10.3.47●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.identity_isHermitian.{u_1}
  {ι : Type u_1} [DecidableEq ι] :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.identity ι)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.identity_isHermitian.{u_1}
  {ι : Type u_1} [DecidableEq ι] :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.identity
      ι)

The identity matrix is Hermitian.

Theorem10.3.48

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “tensor is hermitian”; the hypotheses and conclusion in the code panel fix its exact scope. Tensor products of Hermitian matrices are Hermitian.

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. Tensor products of Hermitian matrices are Hermitian.

Declaration kind. theorem.

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

Lean code for Theorem10.3.48●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.tensor_isHermitian.{u_1, u_2}
  {ι : Type u_1} {κ : Type u_2}
  (A : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix κ κ)
  (hA : QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian A)
  (hB : QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian B) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.tensor A B)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.tensor_isHermitian.{u_1,
    u_2}
  {ι : Type u_1} {κ : Type u_2}
  (A :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      κ κ)
  (hA :
    QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
      A)
  (hB :
    QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
      B) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.tensor
      A B)

Tensor products of Hermitian matrices are Hermitian.

Theorem10.3.49

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “add is hermitian”; the hypotheses and conclusion in the code panel fix its exact scope. Sums of Hermitian matrices are Hermitian.

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. Sums of Hermitian matrices are Hermitian.

Declaration kind. theorem.

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

Lean code for Theorem10.3.49●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.add_isHermitian.{u_1}
  {ι : Type u_1}
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (hA : QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian A)
  (hB : QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian B) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.add A B)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.add_isHermitian.{u_1}
  {ι : Type u_1}
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (hA :
    QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
      A)
  (hB :
    QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
      B) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.add
      A B)

Sums of Hermitian matrices are Hermitian.

Theorem10.3.50

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one dim hamiltonian is hermitian”; the hypotheses and conclusion in the code panel fix its exact scope. The paper's 'H' is Hermitian whenever the coordinate operator is.

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 paper's 'H' is Hermitian whenever the coordinate operator is.

Declaration kind. theorem.

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

Lean code for Theorem10.3.50●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonian_isHermitian.{u_1,
    u_2}
  {ξ : Type u_1} {ι : Type u_2} [DecidableEq ξ]
  (A B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι)
  (xXi : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ξ ξ)
  (hx : QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian xXi) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonian A B xXi)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonian_isHermitian.{u_1,
    u_2}
  {ξ : Type u_1} {ι : Type u_2}
  [DecidableEq ξ]
  (A B :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ι ι)
  (xXi :
    QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
      ξ ξ)
  (hx :
    QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
      xXi) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    (QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonian
      A B xXi)

The paper's `H` is Hermitian whenever the coordinate operator is.

Definition10.3.51

uses 0used by 0✓L∃∀N

Plain-English reading. This record groups the data and proof fields needed for “one dim composition certificate”. A proposition-valued field is a requirement until a constructor supplies it. Proof-carrying source bundle for Theorem 4.

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

Technical source note. Proof-carrying source bundle for Theorem 4. It records the paper's exact composition data: one-term matrices, the inhomogeneous block 'B', and the Schrödingerisation coordinate 'x_ξ'.

Declaration kind. structure.

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

Lean code for Definition10.3.51●1 definition

structure(5 fields)defined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

structure QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.{u_1,
    u_2, u_3}
  (η : Type u_1) (ι : Type u_2) (ξ : Type u_3) [Fintype η]
  [DecidableEq ξ] : Type (max (max u_1 u_2) u_3)

structure QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.{u_1,
    u_2, u_3}
  (η : Type u_1) (ι : Type u_2)
  (ξ : Type u_3) [Fintype η]
  [DecidableEq ξ] :
  Type (max (max u_1 u_2) u_3)

Proof-carrying source bundle for Theorem 4. It records the paper's exact
composition data: one-term matrices, the inhomogeneous block `B`, and
the Schrödingerisation coordinate `x_ξ`.

Fields

terms : η → QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι

B : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι

xXi : QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ξ ξ

B_hermitian : QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian self.B

xXi_hermitian : QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian self.xXi

Definition10.3.52

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “a”. 'A = Σ_k A_k', exactly as in Theorem 4.

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. 'A = Σ_k A_k', exactly as in Theorem 4.

Declaration kind. def.

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

Lean code for Definition10.3.52●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.A.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2} {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.A.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2}
  {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ι ι

`A = Σ_k A_k`, exactly as in Theorem 4.

Definition10.3.53

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “adagger”. 'A†', exposed as a named stage because Theorem 4 combines both 'A' and 'A†'.

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. 'A†', exposed as a named stage because Theorem 4 combines both 'A' and 'A†'.

Declaration kind. def.

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

Lean code for Definition10.3.53●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.Adagger.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2} {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ι ι

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.Adagger.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2}
  {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ι ι

`A†`, exposed as a named stage because Theorem 4 combines both `A` and `A†`.

Theorem10.3.54

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “adagger eq sum term adjoints”; the hypotheses and conclusion in the code panel fix its exact scope. The adjoint assembled from the one-term adjoints equals the adjoint of 'A'.

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 adjoint assembled from the one-term adjoints equals the adjoint of 'A'.

Declaration kind. theorem.

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

Lean code for Theorem10.3.54●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.Adagger_eq_sum_term_adjoints.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2} {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  cert.Adagger =
    QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms fun k =>
      QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint (cert.terms k)

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.Adagger_eq_sum_term_adjoints.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2}
  {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  cert.Adagger =
    QuantumBlockEncoding.GHL2025.Hamiltonian.sumTerms
      fun k =>
      QuantumBlockEncoding.GHL2025.Hamiltonian.adjoint
        (cert.terms k)

The adjoint assembled from the one-term adjoints equals the adjoint of `A`.

Definition10.3.55

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “s”. Homogenized source matrix 'S = [[A,B],[0,0]]'.

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. Homogenized source matrix 'S = [[A,B],[0,0]]'.

Declaration kind. def.

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

Lean code for Definition10.3.55●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.S.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2} {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.S.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2}
  {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

Homogenized source matrix `S = [[A,B],[0,0]]`.

Definition10.3.56

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “first”. First Hermitian source block.

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 Hermitian source block.

Declaration kind. def.

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

Lean code for Definition10.3.56●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.first.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2} {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.first.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2}
  {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

First Hermitian source block.

Definition10.3.57

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “second”. Second Hermitian source block.

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 Hermitian source block.

Declaration kind. def.

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

Lean code for Definition10.3.57●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.second.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2} {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix (ι ⊕ ι) (ι ⊕ ι)

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.second.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2}
  {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    (ι ⊕ ι) (ι ⊕ ι)

Second Hermitian source block.

Definition10.3.58

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “h”. Final Schrödingerised Hamiltonian.

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. Final Schrödingerised Hamiltonian.

Declaration kind. def.

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

Lean code for Definition10.3.58●1 definition

defdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2} {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix ((ι ⊕ ι) × ξ)
    ((ι ⊕ ι) × ξ)

def QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2}
  {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.CMatrix
    ((ι ⊕ ι) × ξ) ((ι ⊕ ι) × ξ)

Final Schrödingerised Hamiltonian.

Theorem10.3.59

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “s decomposition”; the hypotheses and conclusion in the code panel fix its exact scope. The certificate reconstructs 'S' from the two Hermitian pieces.

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 certificate reconstructs 'S' from the two Hermitian pieces.

Declaration kind. theorem.

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

Lean code for Theorem10.3.59●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.S_decomposition.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2} {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ)
  (i j : ι ⊕ ι) :
  cert.S i j = cert.first i j + Complex.I * cert.second i j

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.S_decomposition.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2}
  {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ)
  (i j : ι ⊕ ι) :
  cert.S i j =
    cert.first i j +
      Complex.I * cert.second i j

The certificate reconstructs `S` from the two Hermitian pieces.

Theorem10.3.60

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “h is hermitian”; the hypotheses and conclusion in the code panel fix its exact scope. The final source-level Hamiltonian is Hermitian.

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 final source-level Hamiltonian is Hermitian.

Declaration kind. theorem.

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

Lean code for Theorem10.3.60●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H_isHermitian.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2} {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian cert.H

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H_isHermitian.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2}
  {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.IsHermitian
    cert.H

The final source-level Hamiltonian is Hermitian.

Theorem10.3.61

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “h eq s 1 tensor x xi add s 2 tensor i”; the hypotheses and conclusion in the code panel fix its exact scope. Theorem 4 target formula is definitional in the proof-carrying bundle.

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. Theorem 4 target formula is definitional in the proof-carrying bundle.

Declaration kind. theorem.

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

Lean code for Theorem10.3.61●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H_eq_S1_tensor_xXi_add_S2_tensor_I.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2} {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  cert.H =
    QuantumBlockEncoding.GHL2025.Hamiltonian.add
      (QuantumBlockEncoding.GHL2025.Hamiltonian.tensor cert.first
        cert.xXi)
      (QuantumBlockEncoding.GHL2025.Hamiltonian.tensor cert.second
        (QuantumBlockEncoding.GHL2025.Hamiltonian.identity ξ))

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate.H_eq_S1_tensor_xXi_add_S2_tensor_I.{u_1,
    u_2, u_3}
  {η : Type u_1} {ι : Type u_2}
  {ξ : Type u_3} [Fintype η]
  [DecidableEq ξ]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ) :
  cert.H =
    QuantumBlockEncoding.GHL2025.Hamiltonian.add
      (QuantumBlockEncoding.GHL2025.Hamiltonian.tensor
        cert.first cert.xXi)
      (QuantumBlockEncoding.GHL2025.Hamiltonian.tensor
        cert.second
        (QuantumBlockEncoding.GHL2025.Hamiltonian.identity
          ξ))

Theorem 4 target formula is definitional in the proof-carrying bundle.

Theorem10.3.62

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one dim hamiltonian claim target closed”; the hypotheses and conclusion in the code panel fix its exact scope. The paper registry's 1D target is exactly the composition formalized here.

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 paper registry's 1D target is exactly the composition formalized here.

Declaration kind. theorem.

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

Lean code for Theorem10.3.62●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_target_closed :
  QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.target =
    "H = S1 tensor x_xi + S2 tensor I_xi"

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_target_closed :
  QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.target =
    "H = S1 tensor x_xi + S2 tensor I_xi"

The paper registry's 1D target is exactly the composition formalized here.

Theorem10.3.63

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “one dim hamiltonian claim resource closed”; the hypotheses and conclusion in the code panel fix its exact scope. Theorem 4's resource expression is the registered source expression.

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. Theorem 4's resource expression is the registered source expression.

Declaration kind. theorem.

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

Lean code for Theorem10.3.63●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_resource_closed :
  QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.resource =
    QuantumBlockEncoding.GHL2025.oneDimHamiltonianResourceExpr

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.oneDimHamiltonianClaim_resource_closed :
  QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.resource =
    QuantumBlockEncoding.GHL2025.oneDimHamiltonianResourceExpr

Theorem 4's resource expression is the registered source expression.

Theorem10.3.64

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “theorem 4 source lcu route closed”; the hypotheses and conclusion in the code panel fix its exact scope. Single proof root for the paper-level Theorem 4 composition.

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. Single proof root for the paper-level Theorem 4 composition. This closes the source clean-block algebra of Eqs. (29)-(30), the final 'H' formula, and the normalization/layout/resource records. Primitive arbitrary-width realization of every Theorem-3 input oracle remains a separate compiler layer.

Declaration kind. theorem.

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

Lean code for Theorem10.3.64●1 theorem

theoremdefined in QuantumBlockEncoding/GHLHamiltonian.lean

complete

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed.{u_1,
    u_2, u_3}
  {ι : Type u_2} {ξ : Type u_3} [DecidableEq ι] [DecidableEq ξ]
  {η : Type u_1} [Fintype η]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ)
  (normalizerA : ℂ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean cert.A
        cert.B normalizerA =
      cert.first ∧
    QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean cert.A cert.B
          normalizerA =
        cert.second ∧
      cert.H =
          QuantumBlockEncoding.GHL2025.Hamiltonian.add
            (QuantumBlockEncoding.GHL2025.Hamiltonian.tensor cert.first
              cert.xXi)
            (QuantumBlockEncoding.GHL2025.Hamiltonian.tensor cert.second
              (QuantumBlockEncoding.GHL2025.Hamiltonian.identity ξ)) ∧
        QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.normalization =
            "O(kappa * ||H||_max)" ∧
          QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.resource =
            QuantumBlockEncoding.GHL2025.oneDimHamiltonianResourceExpr

theorem QuantumBlockEncoding.GHL2025.Hamiltonian.theorem4_source_lcu_route_closed.{u_1,
    u_2, u_3}
  {ι : Type u_2} {ξ : Type u_3}
  [DecidableEq ι] [DecidableEq ξ]
  {η : Type u_1} [Fintype η]
  (cert :
    QuantumBlockEncoding.GHL2025.Hamiltonian.OneDimCompositionCertificate
      η ι ξ)
  (normalizerA : ℂ) :
  QuantumBlockEncoding.GHL2025.Hamiltonian.eq29PhaseBalancedClean
        cert.A cert.B normalizerA =
      cert.first ∧
    QuantumBlockEncoding.GHL2025.Hamiltonian.eq30Clean
          cert.A cert.B normalizerA =
        cert.second ∧
      cert.H =
          QuantumBlockEncoding.GHL2025.Hamiltonian.add
            (QuantumBlockEncoding.GHL2025.Hamiltonian.tensor
              cert.first cert.xXi)
            (QuantumBlockEncoding.GHL2025.Hamiltonian.tensor
              cert.second
              (QuantumBlockEncoding.GHL2025.Hamiltonian.identity
                ξ)) ∧
        QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.normalization =
            "O(kappa * ||H||_max)" ∧
          QuantumBlockEncoding.GHL2025.oneDimHamiltonianClaim.resource =
            QuantumBlockEncoding.GHL2025.oneDimHamiltonianResourceExpr

Single proof root for the paper-level Theorem 4 composition.  This closes the
source clean-block algebra of Eqs. (29)-(30), the final `H` formula, and the
normalization/layout/resource records.  Primitive arbitrary-width realization
of every Theorem-3 input oracle remains a separate compiler layer.