This record groups the data and proof fields needed for “loaded”. A proposition-valued field is a requirement until a constructor supplies it.
structure Loaded (k : ℕ) where
source : Vector ℝ (2*k+1+1)
shared : StoredHermiteSharedTables.Tables (2*k+1)
level : StoredHermiteGeometry.TailLevel
parent : StoredBinaryCoordinates.Point
span : ℕ
midpoint : ℕ
cutoff : ℕ
grid : ℝ
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “view”.
def view {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
(t : Fin (n+1)) : Loaded k :=
⟨cache.source, cache.shared, (StoredHermiteGeometry.atStage cache.tails t).value,
cache.parents[t.val], cache.spans[n-t.val], cache.spans[n],
cache.tails.cutoff, cache.tails.grid⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “load”.
def load {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
(t : Fin (n+1)) : Run (Loaded k) := do
let source ← charge .read cache.source
let shared ← charge .read cache.shared
let tails ← charge .read cache.tails
let level ← StoredHermiteGeometry.atStage tails t
let parents ← charge .read cache.parents
let parent ← read parents t
let spans ← charge .read cache.spans
let span ← read spans ⟨n-t.val, by omega⟩
let midpoint ← read spans (Fin.last n)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “load value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem load_value {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
(t : Fin (n+1)) : (load cache t).value = view cache t := rfl
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “load cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem load_cost {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
(t : Fin (n+1)) (op : Op) : (load cache t).cost op = 11 * tick .read op := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “store”.
def store {k : ℕ} (x : Loaded k) (children : Vector StoredHermiteChildGeometry.Child 2) :
Run (StoredHermiteStageFields.Cache k) :=
⟨⟨x.source, x.shared, x.level, children, x.grid⟩, 5 • tick .write⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “input”.
noncomputable def input {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
(t : Fin (n+1)) : StoredHermiteChildGeometry.ChildRun (StoredHermiteStageFields.Cache k) :=
let x := load cache t
let children := StoredHermiteChildGeometry.children x.value.parent x.value.level
x.value.span x.value.cutoff x.value.midpoint
let result := store x.value children.run.value
⟨⟨result.value, x.cost + children.run.cost + result.cost⟩, children.integerAdditions⟩
/-- Mathematical view of the same returned data, not an executable callback. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “stage view”. Mathematical view of the same returned data, not an executable callback.
noncomputable def stageView {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
(t : Fin (n+1)) : StoredHermiteStageFields.Cache k :=
let x := view cache t
⟨x.source, x.shared, x.level,
(StoredHermiteChildGeometry.children x.parent x.level x.span x.cutoff x.midpoint).run.value,
x.grid⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “input value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem input_value {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
(t : Fin (n+1)) : (input cache t).run.value = stageView cache t := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “input cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem input_cost {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
(t : Fin (n+1)) (op : Op) :
(input cache t).run.cost op = 6 * tick .field op + 20 * tick .compare op +
29 * tick .read op + 31 * tick .write op := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “input integer additions”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem input_integerAdditions {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
(t : Fin (n+1)) : (input cache t).integerAdditions = 4 :=
StoredHermiteChildGeometry.children_integerAdditions _ _ _ _ _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “input total cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem input_total_cost {k n : ℕ} (cache : StoredHermiteSourceCache.Cache k n)
(t : Fin (n+1)) : (∑ op : Op, (input cache t).run.cost op) = 86 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “input correct”; the hypotheses and conclusion in the code panel fix its exact scope. The final bridge is unconditional apart from L>0: source, shared tables, tails, parent first/lower, and integer spans all come from global compile.
theorem inputCorrect (k n : ℕ) (L : ℝ) (hL : 0 < L) (t : Fin (n+1)) :
StoredHermiteStageFields.CacheCorrect n t.val L
(input (StoredHermiteSourceCache.compile k n L).run.value t).run.value := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “input certified”; the hypotheses and conclusion in the code panel fix its exact scope. Correctness and both operation counters refer to this very input run.
theorem input_certified (k n : ℕ) (L : ℝ) (hL : 0 < L) (t : Fin (n+1)) :
let result := input (StoredHermiteSourceCache.compile k n L).run.value t
StoredHermiteStageFields.CacheCorrect n t.val L result.run.value ∧
(∑ op : Op, result.run.cost op) = 86 ∧ result.integerAdditions = 4 :=
⟨inputCorrect k n L hL t, input_total_cost _ t, input_integerAdditions _ t⟩
commit-pinned source · Verso Blueprint panel