QuantumBlockEncoding/StoredHermiteRawSource.lean

This record groups the data and proof fields needed for “stage run”. A proposition-valued field is a requirement until a constructor supplies it.

structure StageRun (α : Type) extends SourceRun α where
  integerAdditions : ℕ

commit-pinned source · Verso Blueprint panel

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

noncomputable def stage {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
    (t : Fin (n+1)) : StageRun (StoredCore (2*k+6) (2*k+6)) :=
  let input := StoredHermiteStageInput.input cache t
  let fields := StoredHermiteStageFields.two input.run.value t.val
  let core := StoredHermiteKernelTable.assemble fields.run.value
  { run := ⟨core.value, input.run.cost + fields.run.cost + core.cost⟩
    exponentialCalls := fields.exponentialCalls
    integerAdditions := input.integerAdditions }

commit-pinned source · Verso Blueprint panel

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

theorem stage_source (k n : ℕ) (L : ℝ) (hL : 0 < L) (t : Fin (n+1))
    (a : Fin (2*k+6)) (out : Fin 2 × Fin (2*k+6)) :
    denoteCore (stage (StoredHermiteSourceCache.compile k n L).run.value t).run.value a out =
      HermiteExplicitBond.kernel k n L t.val out.1 a out.2 := by

commit-pinned source · Verso Blueprint panel

This definition gives the library's named construction or computation for “collect stages”. Materialize the stage records once, then project cores and their ledgers.

def collectStages {m : ℕ} (f : Fin m → StageRun α) : StageRun (Vector α m) :=
  let entries : Vector (StageRun α) m := Vector.ofFn f
  let projected := collect fun i => do
    let entry ← read entries i
    pure entry.run.value
  { run := ⟨projected.value,
      (fun op => ∑ i : Fin m, entries[i.val].run.cost op) +
        m • tick .write + projected.cost⟩
    exponentialCalls := ∑ i : Fin m, entries[i.val].exponentialCalls
    integerAdditions := ∑ i : Fin m, entries[i.val].integerAdditions }

commit-pinned source · Verso Blueprint panel

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

theorem collectStages_value {m : ℕ} (f : Fin m → StageRun α) (i : Fin m) :
    (collectStages f).run.value[i.val] = (f i).run.value := by

commit-pinned source · Verso Blueprint panel

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

noncomputable def tables {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n) :
    StageRun (Vector (StoredCore (2*k+6) (2*k+6)) (n+1)) := collectStages (stage cache)

commit-pinned source · Verso Blueprint panel

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

theorem tables_window (k n : ℕ) (L : ℝ) (hL : 0 < L) :
    StoredMatrixProductChain.Window
      (tables (StoredHermiteSourceCache.compile k n L).run.value).run.value
      (HermiteExplicitBond.kernel k n L) 0 := by

commit-pinned source · Verso Blueprint panel

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

def boundaryInputs {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n) : Run (ℕ × ℕ) := do
  let tails ← charge .read cache.tails
  let cut ← charge .read tails.cutoff
  let spans ← charge .read cache.spans
  let midpoint ← read spans (Fin.last n)
  pure (cut, midpoint)

commit-pinned source · Verso Blueprint panel

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

def boundaries {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n) :
    Run (Vector ℝ (2*k+6) × Vector ℝ (2*k+6)) := do
  let params ← boundaryInputs cache
  let left ← StoredHermiteBoundaries.initial k params.1 params.2
  let right ← StoredHermiteBoundaries.terminal k
  pure (left, right)

commit-pinned source · Verso Blueprint panel

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

theorem boundaries_initial (k n : ℕ) (L : ℝ) (hL : 0 < L) (i : Fin (2*k+6)) :
    (boundaries (StoredHermiteSourceCache.compile k n L).run.value).value.1[i.val] =
      HermiteExplicitBond.initial k n L i := by

commit-pinned source · Verso Blueprint panel

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

theorem boundaries_terminal (k n : ℕ) (L : ℝ) (i : Fin (2*k+6)) :
    (boundaries (StoredHermiteSourceCache.compile k n L).run.value).value.2[i.val] =
      HermiteExplicitBond.terminal k i :=
  StoredHermiteBoundaries.terminal_value k i

commit-pinned source · Verso Blueprint panel

This record groups the data and proof fields needed for “raw run”. A proposition-valued field is a requirement until a constructor supplies it.

structure RawRun (α : Type) extends StoredHermiteSourceCache.CacheRun α where
  integerAdditions : ℕ

commit-pinned source · Verso Blueprint panel

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

noncomputable def raw (k n : ℕ) (L : ℝ) : RawRun (StoredChain (n+1) 1 1) :=
  let cache := StoredHermiteSourceCache.compile k n L
  let cores := tables cache.run.value
  let ends := boundaries cache.run.value
  let chain := StoredMatrixProductChain.ofTable cores.run.value ends.value.1 ends.value.2
  { run := ⟨chain.value, cache.run.cost + cores.run.cost + ends.cost + chain.cost⟩
    exponentialCalls := cache.exponentialCalls + cores.exponentialCalls
    quotientCalls := cache.quotientCalls
    remainderCalls := cache.remainderCalls
    integerDoublings := cache.integerDoublings
    integerAdditions := cores.integerAdditions }

commit-pinned source · Verso Blueprint panel

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

theorem raw_value (k n : ℕ) (L : ℝ) (hL : 0 < L) :
    denoteChain (raw k n L).run.value = HermiteExplicitBond.rawSourceChain k n L := by

commit-pinned source · Verso Blueprint panel

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

theorem raw_contract (k n : ℕ) (L : ℝ) (hL : 0 < L)
    (x : TensorTrainCanonical.Word (n+1)) :
    TensorTrainCanonical.contract (denoteChain (raw k n L).run.value) x 0 0 =
      HermiteStatePreparation.sampledAmplitude k (n+1) L (TensorTrainWord.sampleEquiv (n+1) x) := by

commit-pinned source · Verso Blueprint panel