This record groups the data and proof fields needed for “indexed run”. A proposition-valued field is a requirement until a constructor supplies it.
structure IndexedRun (α : Type) where
run : Run α
quotientCalls : ℕ
remainderCalls : ℕ
/-- Read exactly `width` low binary digits using quotient/remainder, then
Horner arithmetic. The legal-input theorem requires the integer to fit. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “binary real”. Read exactly 'width' low binary digits using quotient/remainder, then Horner arithmetic.
noncomputable def binaryReal : (width j : ℕ) → IndexedRun ℝ
| 0, _ => ⟨pure 0, 0, 0⟩
| width + 1, j =>
let quotient := j / 2
let remainder := j % 2
let previous := binaryReal width quotient
let bit : Run ℝ := charge .compare (if remainder = 0 then 0 else 1)
let result : Run ℝ := do
let twice ← StoredGivens.mul previous.run.value 2
StoredGivens.add twice bit.value
⟨⟨result.value, previous.run.cost + bit.cost + result.cost⟩,
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “binary real value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem binaryReal_value (width j : ℕ) (h : j < 2 ^ width) :
(binaryReal width j).run.value = (j : ℝ) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “binary real cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem binaryReal_cost (width j : ℕ) (op : Op) :
(binaryReal width j).run.cost op =
2 * width * tick .field op + width * tick .compare op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “binary real quotients”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem binaryReal_quotients (width j : ℕ) :
(binaryReal width j).quotientCalls = width := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “binary real remainders”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem binaryReal_remainders (width j : ℕ) :
(binaryReal width j).remainderCalls = width := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “coordinate”. Coordinate supplier from explicit real origin/step and a binary index.
noncomputable def coordinate (width j : ℕ) (origin step : ℝ) : IndexedRun ℝ :=
let index := binaryReal width j
let result : Run ℝ := do
let offset ← StoredGivens.mul step index.run.value
StoredGivens.add origin offset
⟨⟨result.value, index.run.cost + result.cost⟩,
index.quotientCalls, index.remainderCalls⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “coordinate value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem coordinate_value (width j : ℕ) (origin step : ℝ) (h : j < 2 ^ width) :
(coordinate width j origin step).run.value = affinePoint origin step j := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “coordinate cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem coordinate_cost (width j : ℕ) (origin step : ℝ) (op : Op) :
(coordinate width j origin step).run.cost op =
(2 * width + 2) * tick .field op + width * tick .compare op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “coordinate quotients”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem coordinate_quotients (width j : ℕ) (origin step : ℝ) :
(coordinate width j origin step).quotientCalls = width := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “coordinate remainders”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem coordinate_remainders (width j : ℕ) (origin step : ℝ) :
(coordinate width j origin step).remainderCalls = width := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “collect indexed”. One materialized indexed pass, followed by value projection.
def collectIndexed {m : ℕ} (f : Fin m → IndexedRun α) : IndexedRun (Vector α m) :=
let entries : Vector (IndexedRun α) m := Vector.ofFn f
⟨⟨entries.map (fun e => e.run.value),
(fun op => ∑ i : Fin m, entries[i.val].run.cost op) +
m • (2 • tick .read + 2 • tick .write)⟩,
∑ i : Fin m, entries[i.val].quotientCalls,
∑ i : Fin m, entries[i.val].remainderCalls⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “collect indexed value”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem collectIndexed_value {m : ℕ} (f : Fin m → IndexedRun α) (i : Fin m) :
(collectIndexed f).run.value[i.val] = (f i).run.value := by simp [collectIndexed]
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “collect indexed cost”; the hypotheses and conclusion in the code panel fix its exact scope.
@[simp] theorem collectIndexed_cost {m : ℕ} (f : Fin m → IndexedRun α) (op : Op) :
(collectIndexed f).run.cost op = (∑ i : Fin m, (f i).run.cost op) +
m * (2 * tick .read op + 2 * tick .write op) := by simp [collectIndexed]; ring
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “point”. A proposition-valued field is a requirement until a constructor supplies it.
structure Point where
first : ℕ
lower : ℝ
/-- The schedule uses one separately counted integer quotient. Powers and
integer address multiplication remain outside the two selected index counters.
The real coordinate itself is built by charged binary arithmetic. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “parent”. The schedule uses one separately counted integer quotient.
noncomputable def parent (n cut r : ℕ) (origin step : ℝ) : IndexedRun Point :=
let scale := 2 ^ (r + 1)
let block := cut / scale
let first := scale * block
let result := coordinate (n + 1) first origin step
⟨⟨⟨first, result.run.value⟩, result.run.cost⟩,
result.quotientCalls + 1, result.remainderCalls⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “parent first”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem parent_first (n cut r : ℕ) (origin step : ℝ) :
(parent n cut r origin step).run.value.first = boundarySchedule cut (r + 1) := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “parent lower”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem parent_lower (n cut r : ℕ) (origin step : ℝ) (hc : cut ≤ 2 ^ n) :
(parent n cut r origin step).run.value.lower =
affinePoint origin step (boundarySchedule cut (r + 1)) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “parent cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem parent_cost (n cut r : ℕ) (origin step : ℝ) (op : Op) :
(parent n cut r origin step).run.cost op =
(2 * n + 4) * tick .field op + (n + 1) * tick .compare op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “parent quotients”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem parent_quotients (n cut r : ℕ) (origin step : ℝ) :
(parent n cut r origin step).quotientCalls = n + 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “parent remainders”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem parent_remainders (n cut r : ℕ) (origin step : ℝ) :
(parent n cut r origin step).remainderCalls = n + 1 := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “parents”. Chronological parent rows: index 't' corresponds to residual width 'n-t'.
noncomputable def parents (n cut : ℕ) (origin step : ℝ) :
IndexedRun (Vector Point (n + 1)) :=
collectIndexed fun t => parent n cut (n - t.val) origin step
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “parents first”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem parents_first (n cut : ℕ) (origin step : ℝ) (t : Fin (n + 1)) :
(parents n cut origin step).run.value[t.val].first =
boundarySchedule cut (n - t.val + 1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “parents lower”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem parents_lower (n cut : ℕ) (origin step : ℝ) (hc : cut ≤ 2 ^ n)
(t : Fin (n + 1)) :
(parents n cut origin step).run.value[t.val].lower =
affinePoint origin step (boundarySchedule cut (n - t.val + 1)) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “parents cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem parents_cost (n cut : ℕ) (origin step : ℝ) (op : Op) :
(parents n cut origin step).run.cost op =
(n + 1) * ((2 * n + 4) * tick .field op + (n + 1) * tick .compare op +
2 * tick .read op + 2 * tick .write op) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “parents quotients”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem parents_quotients (n cut : ℕ) (origin step : ℝ) :
(parents n cut origin step).quotientCalls = (n + 1) * (n + 2) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “parents remainders”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem parents_remainders (n cut : ℕ) (origin step : ℝ) :
(parents n cut origin step).remainderCalls = (n + 1) ^ 2 := by
commit-pinned source · Verso Blueprint panel