This record groups the data and proof fields needed for “cache”. A proposition-valued field is a requirement until a constructor supplies it.
structure Cache (k n : ℕ) where
source : Vector ℝ (2 * k + 1 + 1)
shared : StoredHermiteSharedTables.Tables (2 * k + 1)
tails : StoredHermiteGeometry.TailCache n
origin : ℝ
parents : Vector StoredBinaryCoordinates.Point (n + 1)
spans : Vector ℕ (n + 1)
/-- SourceRun's ordinary and exponential fields are inherited unchanged.
The additional counters describe only selected integer supplier operations. -/
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “cache run”. A proposition-valued field is a requirement until a constructor supplies it. SourceRun's ordinary and exponential fields are inherited unchanged.
structure CacheRun (α : Type) extends SourceRun α where
quotientCalls : ℕ
remainderCalls : ℕ
integerDoublings : ℕ
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “inputs”. A proposition-valued field is a requirement until a constructor supplies it.
structure Inputs where
origin : ℝ
grid : ℝ
cutoff : ℕ
/-- Reuse the actual root-level tail width, never recompute pi*L or cast an
integer address. Root/table and numeric payload reads are separately charged. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “inputs”. Reuse the actual root-level tail width, never recompute pi*L or cast an integer address.
noncomputable def inputs {n : ℕ} (tail : StoredHermiteGeometry.TailCache n) : Run Inputs := do
let root ← StoredHermiteGeometry.atStage tail 0
let width ← charge .read root.width
let origin ← StoredGivens.sub 0 width
let grid ← charge .read tail.grid
let cutoff ← charge .read tail.cutoff
pure ⟨origin, grid, cutoff⟩
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “inputs value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem inputs_value (n : ℕ) (L : ℝ) (hL : 0 < L) :
(inputs (StoredHermiteGeometry.tailCache n L).run.value).value.origin = -Real.pi * L ∧
(inputs (StoredHermiteGeometry.tailCache n L).run.value).value.grid = gridStep n L ∧
(inputs (StoredHermiteGeometry.tailCache n L).run.value).value.cutoff = cutIndex n L := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “inputs cost”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem inputs_cost {n : ℕ} (tail : StoredHermiteGeometry.TailCache n) (op : Op) :
(inputs tail).cost op = 4 * tick .read op + tick .field op := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “store cache”. Explicit fixed-size record materialization; arrays and tables are already stored and are preserved by reference rather than regenerated.
def storeCache {k n : ℕ} (source : Vector ℝ (2*k+1+1))
(shared : StoredHermiteSharedTables.Tables (2*k+1))
(tails : StoredHermiteGeometry.TailCache n) (origin : ℝ)
(parents : Vector StoredBinaryCoordinates.Point (n+1))
(spans : Vector ℕ (n+1)) : Run (Cache k n) :=
⟨⟨source, shared, tails, origin, parents, spans⟩, 6 • tick .write⟩
/-- Actual deterministic source cache, with no hypothetical supplier input. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “compile”. Actual deterministic source cache, with no hypothetical supplier input.
noncomputable def compile (k n : ℕ) (L : ℝ) : CacheRun (Cache k n) :=
let source := StoredHermiteCoefficients.compile k
let shared := StoredHermiteSharedTables.compile (2*k+1)
let tails := StoredHermiteGeometry.tailCache n L
let scalar := inputs tails.run.value
let parents := StoredBinaryCoordinates.parents n scalar.value.cutoff
scalar.value.origin scalar.value.grid
let spans := StoredDyadicSpans.spans n
let stored := storeCache source.run.value shared.value tails.run.value
scalar.value.origin parents.run.value spans.run.value
⟨⟨⟨stored.value,
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile source”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_source (k n : ℕ) (L : ℝ) (i : Fin (2*k+1+1)) :
(compile k n L).run.value.source[i.val] =
HermiteBernstein.sourceBernsteinCoefficient k i.val :=
StoredHermiteCoefficients.compile_value k i
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile shared false”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_shared_false (k n : ℕ) (L : ℝ) :
denote (compile k n L).run.value.shared.falseTable = sharedCore (2*k+1) false :=
StoredHermiteSharedTables.compile_false (2*k+1)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile shared true”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_shared_true (k n : ℕ) (L : ℝ) :
denote (compile k n L).run.value.shared.trueTable = sharedCore (2*k+1) true :=
StoredHermiteSharedTables.compile_true (2*k+1)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile tails”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_tails (k n : ℕ) (L : ℝ) (hL : 0 < L) :
(compile k n L).run.value.tails.cutoff = cutIndex n L ∧
(compile k n L).run.value.tails.grid = gridStep n L ∧
∀ r : Fin (n+1),
((compile k n L).run.value.tails.levels[r.val]).width = gridStep n L * (2 : ℝ)^r.val ∧
((compile k n L).run.value.tails.levels[r.val]).factor =
Real.exp (-gridStep n L * (2 : ℝ)^r.val) :=
StoredHermiteGeometry.tailCache_value n L hL
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile origin”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_origin (k n : ℕ) (L : ℝ) (hL : 0 < L) :
(compile k n L).run.value.origin = -Real.pi * L :=
(inputs_value n L hL).1
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile parents first”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_parents_first (k n : ℕ) (L : ℝ) (hL : 0 < L) (t : Fin (n+1)) :
((compile k n L).run.value.parents[t.val]).first =
boundarySchedule (cutIndex n L) (n - t.val + 1) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile parents lower”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_parents_lower (k n : ℕ) (L : ℝ) (hL : 0 < L) (t : Fin (n+1)) :
((compile k n L).run.value.parents[t.val]).lower =
affinePoint (-Real.pi * L) (gridStep n L)
(boundarySchedule (cutIndex n L) (n - t.val + 1)) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile spans”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_spans (k n : ℕ) (L : ℝ) (r : Fin (n+1)) :
(compile k n L).run.value.spans[r.val] = 2^r.val :=
StoredDyadicSpans.spans_value n r
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile exponential calls”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_exponentialCalls (k n : ℕ) (L : ℝ) :
(compile k n L).exponentialCalls = n + 2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile quotient calls”; the hypotheses and conclusion in the code panel fix its exact scope. These are the selected calls in the exact parent run stored in compile.
theorem compile_quotientCalls (k n : ℕ) (L : ℝ) :
(compile k n L).quotientCalls = (n+1)*(n+2) :=
StoredBinaryCoordinates.parents_quotients _ _ _ _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile remainder calls”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_remainderCalls (k n : ℕ) (L : ℝ) :
(compile k n L).remainderCalls = (n+1)^2 :=
StoredBinaryCoordinates.parents_remainders _ _ _ _
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile integer doublings”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_integerDoublings (k n : ℕ) (L : ℝ) :
(compile k n L).integerDoublings = n := StoredDyadicSpans.spans_integerDoublings n
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_cost_le (k n : ℕ) (L : ℝ) (op : Op) :
(compile k n L).run.cost op ≤ 400*(k+1)^2 + 32*(n+1)^2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “compile total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem compile_total_cost_le (k n : ℕ) (L : ℝ) :
(∑ op : Op, (compile k n L).run.cost op) ≤
3200*(k+1)^2 + 256*(n+1)^2 := by
commit-pinned source · Verso Blueprint panel