This definition gives the library's named construction or computation for “cell”.
noncomputable def cell {n : ℕ} (xs : Vector ℝ n) (u t : ℝ) (i : Fin n) : Run ℝ := do
let _ ← charge .compare ()
if h : i.val + 1 < n then do
let x ← StoredGivens.read xs i
let y ← StoredGivens.read xs ⟨i.val + 1, h⟩
let ux ← StoredGivens.mul u x
let ty ← StoredGivens.mul t y
add ux ty
else pure 0
/-- Truncated row; the last entry is zero and is never read by a valid cone. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “step”. Truncated row; the last entry is zero and is never read by a valid cone.
noncomputable def step {n : ℕ} (xs : Vector ℝ n) (t : ℝ) : Run (Vector ℝ n) := do
let u ← sub 1 t
collect (cell xs u t)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “step value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem step_value {n : ℕ} (xs : Vector ℝ n) (t : ℝ)
(i : Fin n) (hi : i.val + 1 < n) :
(step xs t).value[i.val] =
(1 - t) * xs[i.val] + t * xs[i.val + 1] := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “rows”. Every scalar entry of the previous row is cached, not a nested callback.
noncomputable def rows {n : ℕ} (xs : Vector ℝ n) (t : ℝ) : ℕ → Run (Vector ℝ n)
| 0 => pure xs
| k + 1 => do
let previous ← rows xs t k
step previous t
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “casteljau succ”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem casteljau_succ (k : ℕ) (c : ℕ → ℝ) (t : ℝ) (i : ℕ) :
casteljau (k + 1) c t i =
(1 - t) * casteljau k c t i + t * casteljau k c t (i + 1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “rows value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem rows_value {n : ℕ} (xs : Vector ℝ n) (c : ℕ → ℝ)
(hx : ∀ i : Fin n, xs[i.val] = c i.val) (t : ℝ) (k : ℕ)
(i : Fin n) (hi : i.val + k < n) :
(rows xs t k).value[i.val] = casteljau k c t i.val := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “row budget”.
def rowBudget (n : ℕ) : Cost := fun op =>
tick .field op + n * (3 * tick .field op + tick .compare op +
4 * tick .read op + 2 * tick .write op)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “step cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem step_cost_le {n : ℕ} (xs : Vector ℝ n) (t : ℝ) (op : Op) :
(step xs t).cost op ≤ rowBudget n op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “rows cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem rows_cost_le {n : ℕ} (xs : Vector ℝ n) (t : ℝ) (k : ℕ) (op : Op) :
(rows xs t k).cost op ≤ k * rowBudget n op := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “left”.
noncomputable def left {d : ℕ} (xs : Vector ℝ (d + 1)) (u : ℝ) :
Run (Vector ℝ (d + 1)) :=
collect fun i => do
let row ← rows xs u i.val
read row ⟨0, by omega⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “right”.
noncomputable def right {d : ℕ} (xs : Vector ℝ (d + 1)) (u : ℝ) :
Run (Vector ℝ (d + 1)) :=
collect fun i => do
let row ← rows xs u (d - i.val)
read row i
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “left value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem left_value {d : ℕ} (xs : Vector ℝ (d + 1)) (c : ℕ → ℝ)
(hx : ∀ i : Fin (d + 1), xs[i.val] = c i.val) (u : ℝ) (i : Fin (d + 1)) :
(left xs u).value[i.val] = leftRestriction u c i.val := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “right value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem right_value {d : ℕ} (xs : Vector ℝ (d + 1)) (c : ℕ → ℝ)
(hx : ∀ i : Fin (d + 1), xs[i.val] = c i.val) (u : ℝ) (i : Fin (d + 1)) :
(right xs u).value[i.val] = rightRestriction d u c i.val := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “edge budget”.
def edgeBudget (d : ℕ) : Cost := fun op =>
(d + 1) * (d * rowBudget (d + 1) op + 3 * tick .read op + 2 * tick .write op)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “left cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem left_cost_le {d : ℕ} (xs : Vector ℝ (d + 1)) (u : ℝ) (op : Op) :
(left xs u).cost op ≤ edgeBudget d op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “right cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem right_cost_le {d : ℕ} (xs : Vector ℝ (d + 1)) (u : ℝ) (op : Op) :
(right xs u).cost op ≤ edgeBudget d op := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “restrict”. The actual two-edge producer, with three charged parameter operations.
noncomputable def restrict {d : ℕ} (xs : Vector ℝ (d + 1)) (u v : ℝ) :
Run (Vector ℝ (d + 1)) := do
let first ← right xs u
let delta ← sub v u
let complement ← sub 1 u
let parameter ← div delta complement
left first parameter
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “restrict value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem restrict_value {d : ℕ} (xs : Vector ℝ (d + 1)) (c : ℕ → ℝ)
(hx : ∀ i : Fin (d + 1), xs[i.val] = c i.val)
(u v : ℝ) (i : Fin (d + 1)) :
(restrict xs u v).value[i.val] = restrictCoefficients d u v c i.val := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “restrict cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem restrict_cost_le {d : ℕ} (xs : Vector ℝ (d + 1)) (u v : ℝ) (op : Op) :
(restrict xs u v).cost op ≤ 2 * edgeBudget d op + 3 * tick .field op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “restrict total cost le”; the hypotheses and conclusion in the code panel fix its exact scope. All eight counted operation classes; source coefficient generation is separate.
theorem restrict_total_cost_le {d : ℕ} (xs : Vector ℝ (d + 1)) (u v : ℝ) :
StoredRectangularGivens.total (restrict xs u v).cost ≤
20 * d ^ 3 + 42 * d ^ 2 + 32 * d + 13 := by
commit-pinned source · Verso Blueprint panel