QuantumBlockEncoding/HermiteExplicitBond.lean

This definition gives the library's named construction or computation for “scalar equiv”.

def scalarEquiv : Fin 2 ≃ ScalarBond :=
  (finSuccEquiv 1).trans (Equiv.optionCongr finOneEquiv)

/-- Layout: two left-tail states, middle boundary then `2*k+2` Bernstein
states, and finally the right-tail state. All maps are executable. -/

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “bond equiv”. Layout: two left-tail states, middle boundary then '2*k+2' Bernstein states, and finally the right-tail state.

def bondEquiv (k : ℕ) : Fin (2 * k + 6) ≃ HermiteFiniteBond k :=
  (finCongr (show 2 * k + 6 = 2 + ((2 * k + 1 + 1 + 1) + 1) by omega)).trans
    (finSumFinEquiv.symm.trans (Equiv.sumCongr scalarEquiv
      (finSumFinEquiv.symm.trans
        (Equiv.sumCongr (finSuccEquiv (2 * k + 1 + 1)) finOneEquiv))))

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “kernel”.

noncomputable def kernel (k n : ℕ) (L : ℝ) : MatrixProductChain.Kernel (2 * k + 6) :=
  fun t bit a b => hermiteKernel k n L (n - t) (decide (bit = 1))
    (bondEquiv k a) (bondEquiv k b)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “initial”.

noncomputable def initial (k n : ℕ) (L : ℝ) : Fin (2 * k + 6) → ℝ :=
  fun a => hermiteInitial k n L (bondEquiv k a)

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “terminal”.

noncomputable def terminal (k : ℕ) : Fin (2 * k + 6) → ℝ :=
  fun a => hermiteTerminal k (bondEquiv k a)

commit-pinned source · Verso Blueprint panel

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

theorem kernel_readout (k n : ℕ) (L : ℝ) (m start : ℕ)
    (h : start + m = n + 1) (x : Word m) (a : Fin (2 * k + 6)) :
    MatrixProductChain.readout (kernel k n L) (terminal k) start x a =
      kernelContract (hermiteKernel k n L) (hermiteTerminal k) (toBits x)
        (bondEquiv k a) := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “raw source chain”.

noncomputable def rawSourceChain (k n : ℕ) (L : ℝ) : Chain (n + 1) 1 1 :=
  MatrixProductChain.ofKernel (kernel k n L) (initial k n L) (terminal k) 0 n

commit-pinned source · Verso Blueprint panel

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

theorem rawSourceChain_contract (k n : ℕ) (L : ℝ) (hL : 0 < L)
    (x : Word (n + 1)) :
    contract (rawSourceChain k n L) x 0 0 =
      HermiteStatePreparation.sampledAmplitude k (n + 1) L
        (sampleEquiv (n + 1) x) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “same literal source”; the hypotheses and conclusion in the code panel fix its exact scope. Equality of the observable source, not an unproved equality of layouts.

theorem same_literal_source (k n : ℕ) (L : ℝ) (hL : 0 < L)
    (x : Word (n + 1)) :
    contract (rawSourceChain k n L) x 0 0 =
      contract (HermiteFiniteNorm.rawSourceChain k n L) x 0 0 := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “raw source chain max bond”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem rawSourceChain_maxBond (k n : ℕ) (L : ℝ) :
    maxBond (rawSourceChain k n L) ≤ 2 * k + 6 := by

commit-pinned source · Verso Blueprint panel

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

theorem rawSourceChain_norm (k n : ℕ) (L : ℝ) (hL : 0 < L) :
    TensorTrainNormEnvironment.norm (rawSourceChain k n L) =
      HermiteStatePreparation.sampleNorm k (n + 1) L :=
  TensorTrainNormEnvironment.norm_eq_of_contract (rawSourceChain k n L)
    (sampleEquiv (n + 1)) (HermiteStatePreparation.sampledAmplitude k (n + 1) L)
    (rawSourceChain_contract k n L hL)

commit-pinned source · Verso Blueprint panel