10.8. QuantumBlockEncoding/HermiteCutRank.lean🔗

20 explicit public declarations, in source order.

Definition10.8.1

uses 0used by 0✓L∃∀N

Plain-English reading. This definition gives the library's named construction or computation for “factors through”. Explicit finite-width separation, retaining both factors as witnesses.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. Explicit finite-width separation, retaining both factors as witnesses.

Declaration kind. def.

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

Lean code for Definition10.8.1●1 definition

defdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

def QuantumBlockEncoding.HermiteCutRank.FactorsThrough.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype ι]
  (F : Matrix α β ℝ) : Prop

def QuantumBlockEncoding.HermiteCutRank.FactorsThrough.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {ι : Type u_3} [Fintype ι]
  (F : Matrix α β ℝ) : Prop

Explicit finite-width separation, retaining both factors as witnesses.

Theorem10.8.2

uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.8.2●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.FactorsThrough.rank_le.{u_1, u_2,
    u_3}
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype β] [Fintype ι]
  {F : Matrix α β ℝ}
  (h : QuantumBlockEncoding.HermiteCutRank.FactorsThrough F) :
  F.rank ≤ Fintype.card ι

theorem QuantumBlockEncoding.HermiteCutRank.FactorsThrough.rank_le.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {ι : Type u_3} [Fintype β] [Fintype ι]
  {F : Matrix α β ℝ}
  (h :
    QuantumBlockEncoding.HermiteCutRank.FactorsThrough
      F) :
  F.rank ≤ Fintype.card ι

Theorem10.8.3

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “polynomial add factorization”; the hypotheses and conclusion in the code panel fix its exact scope. Taylor coefficients give a degree-sized factorization at any additive cut.

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

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

Technical source note. Taylor coefficients give a degree-sized factorization at any additive cut.

Declaration kind. theorem.

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

Lean code for Theorem10.8.3●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.polynomial_add_factorization.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} (p : Polynomial ℝ) (d : ℕ)
  (hd : p.natDegree ≤ d) (u : α → ℝ) (v : β → ℝ) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough fun x y =>
    Polynomial.eval (u x + v y) p

theorem QuantumBlockEncoding.HermiteCutRank.polynomial_add_factorization.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  (p : Polynomial ℝ) (d : ℕ)
  (hd : p.natDegree ≤ d) (u : α → ℝ)
  (v : β → ℝ) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    fun x y =>
    Polynomial.eval (u x + v y) p

Taylor coefficients give a degree-sized factorization at any additive cut.

Theorem10.8.4

uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.8.4●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.polynomial_add_rank_le.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} [Fintype β] (p : Polynomial ℝ) (d : ℕ)
  (hd : p.natDegree ≤ d) (u : α → ℝ) (v : β → ℝ) :
  (Matrix.rank fun x y => Polynomial.eval (u x + v y) p) ≤ d + 1

theorem QuantumBlockEncoding.HermiteCutRank.polynomial_add_rank_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype β] (p : Polynomial ℝ) (d : ℕ)
  (hd : p.natDegree ≤ d) (u : α → ℝ)
  (v : β → ℝ) :
  (Matrix.rank fun x y =>
      Polynomial.eval (u x + v y) p) ≤
    d + 1

Theorem10.8.5

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite polynomial add rank le”; the hypotheses and conclusion in the code panel fix its exact scope. Instantiates the existing Hermite degree theorem, rather than reproving it.

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

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

Technical source note. Instantiates the existing Hermite degree theorem, rather than reproving it.

Declaration kind. theorem.

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

Lean code for Theorem10.8.5●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.hermite_polynomial_add_rank_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} [Fintype β] (k : ℕ) (u : α → ℝ)
  (v : β → ℝ) :
  (Matrix.rank fun x y =>
      Polynomial.eval (u x + v y)
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)) ≤
    2 * k + 2

theorem QuantumBlockEncoding.HermiteCutRank.hermite_polynomial_add_rank_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype β] (k : ℕ) (u : α → ℝ)
  (v : β → ℝ) :
  (Matrix.rank fun x y =>
      Polynomial.eval (u x + v y)
        (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
          k)) ≤
    2 * k + 2

Instantiates the existing Hermite degree theorem, rather than reproving it.

Theorem10.8.6

uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.8.6●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.product_factorization.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} (u : α → ℝ) (v : β → ℝ) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough fun x y =>
    u x * v y

theorem QuantumBlockEncoding.HermiteCutRank.product_factorization.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  (u : α → ℝ) (v : β → ℝ) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    fun x y => u x * v y

Theorem10.8.7

uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.8.7●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.exponential_add_factorization.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} (u : α → ℝ) (v : β → ℝ) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough fun x y =>
    Real.exp (u x + v y)

theorem QuantumBlockEncoding.HermiteCutRank.exponential_add_factorization.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  (u : α → ℝ) (v : β → ℝ) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    fun x y => Real.exp (u x + v y)

Theorem10.8.8

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “add”; the hypotheses and conclusion in the code panel fix its exact scope. A sum preserves an explicit direct-sum factorization.

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

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

Technical source note. A sum preserves an explicit direct-sum factorization.

Declaration kind. theorem.

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

Lean code for Theorem10.8.8●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.FactorsThrough.add.{u_1, u_2, u_3,
    u_4}
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} {κ : Type u_4}
  [Fintype ι] [Fintype κ] {F G : Matrix α β ℝ}
  (hf : QuantumBlockEncoding.HermiteCutRank.FactorsThrough F)
  (hg : QuantumBlockEncoding.HermiteCutRank.FactorsThrough G) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough (F + G)

theorem QuantumBlockEncoding.HermiteCutRank.FactorsThrough.add.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2}
  {ι : Type u_3} {κ : Type u_4}
  [Fintype ι] [Fintype κ]
  {F G : Matrix α β ℝ}
  (hf :
    QuantumBlockEncoding.HermiteCutRank.FactorsThrough
      F)
  (hg :
    QuantumBlockEncoding.HermiteCutRank.FactorsThrough
      G) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    (F + G)

A sum preserves an explicit direct-sum factorization.

Theorem10.8.9

uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.8.9●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.FactorsThrough.neg.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype ι]
  {F : Matrix α β ℝ}
  (hf : QuantumBlockEncoding.HermiteCutRank.FactorsThrough F) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough (-F)

theorem QuantumBlockEncoding.HermiteCutRank.FactorsThrough.neg.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {ι : Type u_3} [Fintype ι]
  {F : Matrix α β ℝ}
  (hf :
    QuantumBlockEncoding.HermiteCutRank.FactorsThrough
      F) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    (-F)

Theorem10.8.10

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “pointwise mul”; the hypotheses and conclusion in the code panel fix its exact scope. Entrywise multiplication multiplies widths, without constructing a dense 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, source-specific Hermite constructions, and concrete State Preparation / Robin example artifacts.

Technical source note. Entrywise multiplication multiplies widths, without constructing a dense matrix.

Declaration kind. theorem.

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

Lean code for Theorem10.8.10●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.FactorsThrough.pointwise_mul.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} {κ : Type u_4}
  [Fintype ι] [Fintype κ] {F G : Matrix α β ℝ}
  (hf : QuantumBlockEncoding.HermiteCutRank.FactorsThrough F)
  (hg : QuantumBlockEncoding.HermiteCutRank.FactorsThrough G) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough fun x y =>
    F x y * G x y

theorem QuantumBlockEncoding.HermiteCutRank.FactorsThrough.pointwise_mul.{u_1,
    u_2, u_3, u_4}
  {α : Type u_1} {β : Type u_2}
  {ι : Type u_3} {κ : Type u_4}
  [Fintype ι] [Fintype κ]
  {F G : Matrix α β ℝ}
  (hf :
    QuantumBlockEncoding.HermiteCutRank.FactorsThrough
      F)
  (hg :
    QuantumBlockEncoding.HermiteCutRank.FactorsThrough
      G) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    fun x y => F x y * G x y

Entrywise multiplication multiplies widths, without constructing a dense matrix.

Theorem10.8.11

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “block index lt iff”; the hypotheses and conclusion in the code panel fix its exact scope. The comparison of a concatenated prefix/suffix has only one boundary row.

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

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

Technical source note. The comparison of a concatenated prefix/suffix has only one boundary row.

Declaration kind. theorem.

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

Lean code for Theorem10.8.11●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.blockIndex_lt_iff (M x y T : ℕ)
  (hy : y < M) : M * x + y < T ↔ x < T / M ∨ x = T / M ∧ y < T % M

theorem QuantumBlockEncoding.HermiteCutRank.blockIndex_lt_iff
  (M x y T : ℕ) (hy : y < M) :
  M * x + y < T ↔
    x < T / M ∨ x = T / M ∧ y < T % M

The comparison of a concatenated prefix/suffix has only one boundary row.

Theorem10.8.12

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “threshold factorization”; the hypotheses and conclusion in the code panel fix its exact scope. An arbitrary threshold has a two-state separation across a binary cut.

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

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

Technical source note. An arbitrary threshold has a two-state separation across a binary cut.

Declaration kind. theorem.

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

Lean code for Theorem10.8.12●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.threshold_factorization.{u_1, u_2}
  {α : Type u_1} {β : Type u_2} (M T : ℕ) (u : α → ℕ) (v : β → ℕ)
  (hv : ∀ (y : β), v y < M) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough fun x y =>
    if M * u x + v y < T then 1 else 0

theorem QuantumBlockEncoding.HermiteCutRank.threshold_factorization.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} (M T : ℕ)
  (u : α → ℕ) (v : β → ℕ)
  (hv : ∀ (y : β), v y < M) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    fun x y =>
    if M * u x + v y < T then 1 else 0

An arbitrary threshold has a two-state separation across a binary cut.

Theorem10.8.13

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “threshold complement factorization”; the hypotheses and conclusion in the code panel fix its exact scope. Complementing a threshold still needs two states, not a dense complement.

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

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

Technical source note. Complementing a threshold still needs two states, not a dense complement.

Declaration kind. theorem.

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

Lean code for Theorem10.8.13●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.threshold_complement_factorization.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} (M T : ℕ) (u : α → ℕ) (v : β → ℕ)
  (hv : ∀ (y : β), v y < M) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough fun x y =>
    1 - if M * u x + v y < T then 1 else 0

theorem QuantumBlockEncoding.HermiteCutRank.threshold_complement_factorization.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} (M T : ℕ)
  (u : α → ℕ) (v : β → ℕ)
  (hv : ∀ (y : β), v y < M) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    fun x y =>
    1 - if M * u x + v y < T then 1 else 0

Complementing a threshold still needs two states, not a dense complement.

Theorem10.8.14

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “affine lt cut”; the hypotheses and conclusion in the code panel fix its exact scope. Relates the exact real grid to an integer cut; no bit-complexity claim.

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

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

Technical source note. Relates the exact real grid to an integer cut; no bit-complexity claim.

Declaration kind. theorem.

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

Lean code for Theorem10.8.14●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.affine_lt_cut (a h t : ℝ)
  (hh : 0 < h) (j : ℕ) : a + h * ↑j < t ↔ j < ⌈(t - a) / h⌉₊

theorem QuantumBlockEncoding.HermiteCutRank.affine_lt_cut
  (a h t : ℝ) (hh : 0 < h) (j : ℕ) :
  a + h * ↑j < t ↔ j < ⌈(t - a) / h⌉₊

Relates the exact real grid to an integer cut; no bit-complexity claim.

Theorem10.8.15

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “smooth initial strict”; the hypotheses and conclusion in the code panel fix its exact scope. Endpoint continuity permits the zero sample to use the right exponential.

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

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

Technical source note. Endpoint continuity permits the zero sample to use the right exponential.

Declaration kind. theorem.

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

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.smoothInitial_strict (k : ℕ)
  (p : ℝ) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial k p =
    if p < -1 then Real.exp p
    else
      if p < 0 then
        Polynomial.eval p
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant k)
      else Real.exp (-p)

theorem QuantumBlockEncoding.HermiteCutRank.smoothInitial_strict
  (k : ℕ) (p : ℝ) :
  QuantumBlockEncoding.HermitePolynomial.smoothInitial
      k p =
    if p < -1 then Real.exp p
    else
      if p < 0 then
        Polynomial.eval p
          (QuantumBlockEncoding.HermitePolynomial.sourceInterpolant
            k)
      else Real.exp (-p)

Endpoint continuity permits the zero sample to use the right exponential.

Definition10.8.16

uses 0used by 0✓L∃∀N

Plain-English reading. This abbreviation gives a shorter name to the type or expression used for “hermite bond”. Explicit index type of the three separated pieces.

Formal status. Compiled declaration in the default ASPBE import surface; its kind and displayed Lean type determine how it may be used.

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

Technical source note. Explicit index type of the three separated pieces.

Declaration kind. abbrev.

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

Lean code for Definition10.8.16●1 definition

abbrevdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

abbrev QuantumBlockEncoding.HermiteCutRank.HermiteBond (k : ℕ) : Type

abbrev QuantumBlockEncoding.HermiteCutRank.HermiteBond
  (k : ℕ) : Type

Explicit index type of the three separated pieces.

Theorem10.8.17

uses 0used by 0✓L∃∀N

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

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.8.17●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.hermiteBond_card (k : ℕ) :
  Fintype.card (QuantumBlockEncoding.HermiteCutRank.HermiteBond k) =
    8 * k + 12

theorem QuantumBlockEncoding.HermiteCutRank.hermiteBond_card
  (k : ℕ) :
  Fintype.card
      (QuantumBlockEncoding.HermiteCutRank.HermiteBond
        k) =
    8 * k + 12

Theorem10.8.18

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite affine factorization”; the hypotheses and conclusion in the code panel fix its exact scope. The literal Hermite samples, including both junctions, admit a bounded cut factorization.

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

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

Technical source note. The literal Hermite samples, including both junctions, admit a bounded cut factorization.

Declaration kind. theorem.

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

Lean code for Theorem10.8.18●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.hermite_affine_factorization.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} (k M : ℕ) (a h : ℝ) (hh : 0 < h)
  (u : α → ℕ) (v : β → ℕ) (hv : ∀ (y : β), v y < M) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough fun x y =>
    QuantumBlockEncoding.HermitePolynomial.smoothInitial k
      (a + h * ↑(M * u x + v y))

theorem QuantumBlockEncoding.HermiteCutRank.hermite_affine_factorization.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} (k M : ℕ)
  (a h : ℝ) (hh : 0 < h) (u : α → ℕ)
  (v : β → ℕ) (hv : ∀ (y : β), v y < M) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    fun x y =>
    QuantumBlockEncoding.HermitePolynomial.smoothInitial
      k (a + h * ↑(M * u x + v y))

The literal Hermite samples, including both junctions, admit a bounded cut factorization.

Theorem10.8.19

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “hermite affine cut rank le”; the hypotheses and conclusion in the code panel fix its exact scope.

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

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

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

Declaration kind. theorem.

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

Lean code for Theorem10.8.19●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.hermite_affine_cut_rank_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2} [Fintype β] (k M : ℕ) (a h : ℝ)
  (hh : 0 < h) (u : α → ℕ) (v : β → ℕ) (hv : ∀ (y : β), v y < M) :
  (Matrix.rank fun x y =>
      QuantumBlockEncoding.HermitePolynomial.smoothInitial k
        (a + h * ↑(M * u x + v y))) ≤
    8 * k + 12

theorem QuantumBlockEncoding.HermiteCutRank.hermite_affine_cut_rank_le.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  [Fintype β] (k M : ℕ) (a h : ℝ)
  (hh : 0 < h) (u : α → ℕ) (v : β → ℕ)
  (hv : ∀ (y : β), v y < M) :
  (Matrix.rank fun x y =>
      QuantumBlockEncoding.HermitePolynomial.smoothInitial
        k (a + h * ↑(M * u x + v y))) ≤
    8 * k + 12

Theorem10.8.20

uses 0used by 0✓L∃∀N

Plain-English reading. Lean checks the proposition indexed as “scale”; the hypotheses and conclusion in the code panel fix its exact scope. A constant normalization can be absorbed into the left factor.

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

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

Technical source note. A constant normalization can be absorbed into the left factor.

Declaration kind. theorem.

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

Lean code for Theorem10.8.20●1 theorem

theoremdefined in QuantumBlockEncoding/HermiteCutRank.lean

complete

theorem QuantumBlockEncoding.HermiteCutRank.FactorsThrough.scale.{u_1, u_2, u_3}
  {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype ι]
  {F : Matrix α β ℝ}
  (hf : QuantumBlockEncoding.HermiteCutRank.FactorsThrough F) (c : ℝ) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough fun x y =>
    c * F x y

theorem QuantumBlockEncoding.HermiteCutRank.FactorsThrough.scale.{u_1,
    u_2, u_3}
  {α : Type u_1} {β : Type u_2}
  {ι : Type u_3} [Fintype ι]
  {F : Matrix α β ℝ}
  (hf :
    QuantumBlockEncoding.HermiteCutRank.FactorsThrough
      F)
  (c : ℝ) :
  QuantumBlockEncoding.HermiteCutRank.FactorsThrough
    fun x y => c * F x y

A constant normalization can be absorbed into the left factor.