QuantumBlockEncoding/HermiteCutRank.lean

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

def FactorsThrough [Fintype ι] (F : Matrix α β ℝ) : Prop :=
  ∃ A : Matrix α ι ℝ, ∃ B : Matrix ι β ℝ, F = A * B

commit-pinned source · Verso Blueprint panel

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

theorem FactorsThrough.rank_le [Fintype β] [Fintype ι]
    {F : Matrix α β ℝ} (h : FactorsThrough (ι := ι) F) :
    F.rank ≤ Fintype.card ι := by

commit-pinned source · Verso Blueprint panel

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.

theorem polynomial_add_factorization (p : ℝ[X]) (d : ℕ)
    (hd : p.natDegree ≤ d) (u : α → ℝ) (v : β → ℝ) :
    FactorsThrough (ι := Fin (d + 1)) (fun x y => p.eval (u x + v y)) := by

commit-pinned source · Verso Blueprint panel

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

theorem polynomial_add_rank_le [Fintype β] (p : ℝ[X]) (d : ℕ)
    (hd : p.natDegree ≤ d) (u : α → ℝ) (v : β → ℝ) :
    Matrix.rank (fun x y => p.eval (u x + v y) : Matrix α β ℝ) ≤ d + 1 := by

commit-pinned source · Verso Blueprint panel

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.

theorem hermite_polynomial_add_rank_le [Fintype β] (k : ℕ)
    (u : α → ℝ) (v : β → ℝ) :
    Matrix.rank (fun x y => (HermitePolynomial.sourceInterpolant k).eval (u x + v y) :
      Matrix α β ℝ) ≤ 2 * k + 2 := by

commit-pinned source · Verso Blueprint panel

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

theorem product_factorization (u : α → ℝ) (v : β → ℝ) :
    FactorsThrough (ι := Unit) (fun x y => u x * v y) := by

commit-pinned source · Verso Blueprint panel

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

theorem exponential_add_factorization (u : α → ℝ) (v : β → ℝ) :
    FactorsThrough (ι := Unit) (fun x y => Real.exp (u x + v y)) := by

commit-pinned source · Verso Blueprint panel

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.

theorem FactorsThrough.add [Fintype ι] [Fintype κ]
    {F G : Matrix α β ℝ} (hf : FactorsThrough (ι := ι) F)
    (hg : FactorsThrough (ι := κ) G) :
    FactorsThrough (ι := Sum ι κ) (F + G) := by

commit-pinned source · Verso Blueprint panel

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

theorem FactorsThrough.neg [Fintype ι]
    {F : Matrix α β ℝ} (hf : FactorsThrough (ι := ι) F) :
    FactorsThrough (ι := ι) (-F) := by

commit-pinned source · Verso Blueprint panel

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.

theorem FactorsThrough.pointwise_mul [Fintype ι] [Fintype κ]
    {F G : Matrix α β ℝ} (hf : FactorsThrough (ι := ι) F)
    (hg : FactorsThrough (ι := κ) G) :
    FactorsThrough (ι := ι × κ) (fun x y => F x y * G x y) := by

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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.

theorem threshold_factorization (M T : ℕ) (u : α → ℕ) (v : β → ℕ)
    (hv : ∀ y, v y < M) :
    FactorsThrough (ι := Fin 2)
      (fun x y => if M * u x + v y < T then (1 : ℝ) else 0) := by

commit-pinned source · Verso Blueprint panel

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.

theorem threshold_complement_factorization (M T : ℕ) (u : α → ℕ) (v : β → ℕ)
    (hv : ∀ y, v y < M) :
    FactorsThrough (ι := Fin 2)
      (fun x y => 1 - if M * u x + v y < T then (1 : ℝ) else 0) := by

commit-pinned source · Verso Blueprint panel

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.

theorem affine_lt_cut (a h t : ℝ) (hh : 0 < h) (j : ℕ) :
    a + h * (j : ℝ) < t ↔ j < Nat.ceil ((t - a) / h) := by

commit-pinned source · Verso Blueprint panel

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.

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

commit-pinned source · Verso Blueprint panel

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

abbrev HermiteBond (k : ℕ) :=
  Sum (Sum (Fin 2 × Unit) ((Sum (Fin 2) (Fin 2)) × Fin (2 * k + 2)))
    (Fin 2 × Unit)

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

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.

theorem hermite_affine_factorization (k M : ℕ) (a h : ℝ) (hh : 0 < h)
    (u : α → ℕ) (v : β → ℕ) (hv : ∀ y, v y < M) :
    FactorsThrough (ι := HermiteBond k)
      (fun x y => HermitePolynomial.smoothInitial k
        (a + h * ((M * u x + v y : ℕ) : ℝ))) := by

commit-pinned source · Verso Blueprint panel

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

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

commit-pinned source · Verso Blueprint panel

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.

theorem FactorsThrough.scale [Fintype ι] {F : Matrix α β ℝ}
    (hf : FactorsThrough (ι := ι) F) (c : ℝ) :
    FactorsThrough (ι := ι) (fun x y => c * F x y) := by

commit-pinned source · Verso Blueprint panel