QuantumBlockEncoding/HermiteFiniteChain.lean

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

noncomputable def bondEquiv (k : Nat) : Fin (2 * k + 6) ≃ HermiteFiniteBond k :=
  (Fintype.equivFinOfCardEq (hermiteFiniteBond_card k)).symm

commit-pinned source · Verso Blueprint panel

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

noncomputable def kernel (k n : Nat) (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 “terminal”.

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

commit-pinned source · Verso Blueprint panel

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

noncomputable def initial (k n : Nat) (L : ℝ) : Fin (2 * k + 6) → ℝ :=
  fun a => hermiteInitial k n L (bondEquiv k a) / HermiteStatePreparation.sampleNorm k (n + 1) L

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 : Nat) (L : ℝ) (m start : Nat) (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 “source chain”. Actual local cores, with normalization absorbed into the initial row.

noncomputable def sourceChain (k n : Nat) (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 “source chain contract”; the hypotheses and conclusion in the code panel fix its exact scope.

theorem sourceChain_contract (k n : Nat) (L : ℝ) (hL : 0 < L)
    (x : Word (n + 1)) :
    contract (sourceChain k n L) x 0 0 =
      HermiteStatePreparation.sampledAmplitude k (n + 1) L (sampleEquiv (n + 1) x) /
        HermiteStatePreparation.sampleNorm k (n + 1) L := by

commit-pinned source · Verso Blueprint panel

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

theorem sourceChain_maxBond (k n : Nat) (L : ℝ) : maxBond (sourceChain k n L) ≤ 2 * k + 6 := by

commit-pinned source · Verso Blueprint panel

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

theorem sourceChain_storage (k n : Nat) (L : ℝ) :
    MatrixProductChain.storedScalars (sourceChain k n L) ≤ 2 * (n + 1) * (2 * k + 6) ^ 2 :=
  MatrixProductChain.storedScalars_le _ _ (sourceChain_maxBond k n L)

commit-pinned source · Verso Blueprint panel

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

theorem sourceChain_normalized (k n : Nat) (L : ℝ) (hL : 0 < L) :
    (∑ x : Word (n + 1), (contract (sourceChain k n L) x 0 0) ^ 2) = 1 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “bond qubits”. Actual binary bond register; its size depends on smoothing order, not the number of data qubits.

def bondQubits (k : Nat) : Nat := Nat.clog 2 (2 * k + 6)

commit-pinned source · Verso Blueprint panel

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

theorem bond_fits (k : Nat) : 2 * k + 6 ≤ 2 ^ bondQubits k :=
  Nat.le_pow_clog (by decide) _

commit-pinned source · Verso Blueprint panel

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

theorem padded_bond_le_twice (k : Nat) : 2 ^ bondQubits k ≤ 2 * (2 * k + 6) := by

commit-pinned source · Verso Blueprint panel

Lean checks the proposition indexed as “cubic stage budget”; the hypotheses and conclusion in the code panel fix its exact scope. Algebraic substitution used after the actual stage compiler is supplied.

theorem cubic_stage_budget (k n : Nat) :
    6 * (n + 1) * (2 ^ bondQubits k) ^ 3 ≤ 48 * (n + 1) * (2 * k + 6) ^ 3 := by

commit-pinned source · Verso Blueprint panel