This definition gives the library's named construction or computation for “initial literal”.
def initialLiteral {k : ℕ} (left middle : Bool) : HermiteFiniteBond k → ℝ
| .inl none => if left then 1 else 0
| .inl (some _) => 0
| .inr (.inl none) => if middle then 1 else 0
| .inr (.inl (some _)) => 0
| .inr (.inr _) => 1
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “terminal literal”.
def terminalLiteral {k : ℕ} : HermiteFiniteBond k → ℝ
| .inl none => 0
| .inl (some _) => 1
| .inr (.inl none) => 0
| .inr (.inl (some j)) => if j.val = 0 then 1 else 0
| .inr (.inr _) => 1
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “initial”.
def initial (k cut midpoint : ℕ) : Run (Vector ℝ (2*k+6)) := do
let left ← charge .compare (decide (cut ≠ 0))
let middle ← charge .compare (decide (cut ≠ midpoint))
collect fun i =>
⟨initialLiteral left middle (HermiteExplicitBond.bondEquiv k i),
12 • tick .compare⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “terminal”.
def terminal (k : ℕ) : Run (Vector ℝ (2*k+6)) :=
collect fun i =>
⟨terminalLiteral (HermiteExplicitBond.bondEquiv k i), 12 • tick .compare⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “initial get”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem initial_get (k cut midpoint : ℕ) (i : Fin (2*k+6)) :
(initial k cut midpoint).value[i.val] =
initialLiteral (decide (cut ≠ 0)) (decide (cut ≠ midpoint))
(HermiteExplicitBond.bondEquiv k i) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “terminal get”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem terminal_get (k : ℕ) (i : Fin (2*k+6)) :
(terminal k).value[i.val] = terminalLiteral (HermiteExplicitBond.bondEquiv k i) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “initial value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem initial_value (k n : ℕ) (L : ℝ) (cut : ℕ)
(hcut : cut = cutIndex n L) (i : Fin (2*k+6)) :
(initial k cut (2^n)).value[i.val] = HermiteExplicitBond.initial k n L i := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “terminal value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem terminal_value (k : ℕ) (i : Fin (2*k+6)) :
(terminal k).value[i.val] = HermiteExplicitBond.terminal k i := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “initial cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem initial_cost (k cut midpoint : ℕ) (op : Op) :
(initial k cut midpoint).cost op = 2*tick .compare op +
(2*k+6)*(12*tick .compare op+2*tick .read op+2*tick .write op) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “terminal cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem terminal_cost (k : ℕ) (op : Op) :
(terminal k).cost op =
(2*k+6)*(12*tick .compare op+2*tick .read op+2*tick .write op) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “initial total cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem initial_total_cost (k cut midpoint : ℕ) :
StoredRectangularGivens.total (initial k cut midpoint).cost = 16*(2*k+6)+2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “terminal total cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem terminal_total_cost (k : ℕ) :
StoredRectangularGivens.total (terminal k).cost = 16*(2*k+6) := by
commit-pinned source · Verso Blueprint panel