This definition gives the library's named construction or computation for “cut sample index”. Concatenate a most-significant prefix and a least-significant suffix.
def cutSampleIndex (pWidth sWidth : ℕ) (x : Fin (gridSize pWidth))
(y : Fin (gridSize sWidth)) : Fin (gridSize (pWidth + sWidth)) :=
⟨gridSize sWidth * x.val + y.val, by
have hx := x.isLt
have hy := y.isLt
have hm : 0 < gridSize sWidth := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sampled cut factorization”; the hypotheses and conclusion in the code panel fix its exact scope. The rank certificate applies to the actual frozen sample API at every cut, including empty prefix/suffix cuts.
theorem sampled_cut_factorization (k pWidth sWidth : ℕ) (L : ℝ) (hL : 0 < L) :
FactorsThrough (ι := HermiteBond k)
(fun x y => HermiteStatePreparation.sampledAmplitude k (pWidth + sWidth) L
(cutSampleIndex pWidth sWidth x y)) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “sampled cut rank le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem sampled_cut_rank_le (k pWidth sWidth : ℕ) (L : ℝ) (hL : 0 < L) :
_root_.Matrix.rank (fun x y =>
HermiteStatePreparation.sampledAmplitude k (pWidth + sWidth) L
(cutSampleIndex pWidth sWidth x y)) ≤ 8 * k + 12 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “normalized cut factorization”; the hypotheses and conclusion in the code panel fix its exact scope. The real amplitudes underlying the public complex state retain the same factor width after exact normalization.
theorem normalized_cut_factorization (k pWidth sWidth : ℕ) (L : ℝ) (hL : 0 < L) :
FactorsThrough (ι := HermiteBond k)
(fun x y =>
HermiteStatePreparation.sampledAmplitude k (pWidth + sWidth) L
(cutSampleIndex pWidth sWidth x y) /
HermiteStatePreparation.sampleNorm k (pWidth + sWidth) L) := by
commit-pinned source · Verso Blueprint panel