This record groups the data and proof fields needed for “fields”. A proposition-valued field is a requirement until a constructor supplies it. P=2k+2, written in the definitional form used by InjectionBond.
structure Fields (k : ℕ) where
leftPartial : Bool
leftInjection : ℝ
leftFree : ℝ
middlePartial : Bool
middleInjection : Vector ℝ (2 * k + 1 + 1)
shared : StoredMatrix (2 * k + 1 + 1) (2 * k + 1 + 1)
rightCore : ℝ
/-- Mathematical block interpretation; not used to evaluate stored entries. -/
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “block view”. Mathematical block interpretation; not used to evaluate stored entries.
def blockView {k : ℕ} (f : Fields k) :
HermiteFiniteBond k → HermiteFiniteBond k → ℝ
| .inl none, .inl none => if f.leftPartial then 1 else 0
| .inl none, .inl (some _) => f.leftInjection
| .inl (some _), .inl (some _) => f.leftFree
| .inr (.inl none), .inr (.inl none) => if f.middlePartial then 1 else 0
| .inr (.inl none), .inr (.inl (some j)) => f.middleInjection[j.val]
| .inr (.inl (some i)), .inr (.inl (some j)) => denote f.shared i j
| .inr (.inr _), .inr (.inr _) => f.rightCore
| _, _ => 0
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “stored block”. Actual stored-word readers and literal-zero blocks.
def storedBlock {k : ℕ} (f : Fields k)
(a b : HermiteFiniteBond k) : Run ℝ :=
let result : Run ℝ := match a, b with
| .inl none, .inl none => do
let flag ← charge .read f.leftPartial
charge .compare (if flag then 1 else 0)
| .inl none, .inl (some _) => charge .read f.leftInjection
| .inl (some _), .inl (some _) => charge .read f.leftFree
| .inr (.inl none), .inr (.inl none) => do
let flag ← charge .read f.middlePartial
charge .compare (if flag then 1 else 0)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “stored block value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem storedBlock_value {k : ℕ} (f : Fields k) (a b : HermiteFiniteBond k) :
(storedBlock f a b).value = blockView f a b := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “decode”. The production explicit equivalence is executable, not a cardinality choice.
def decode (k : ℕ) (a : Fin (2 * k + 6)) : Run (HermiteFiniteBond k) :=
⟨HermiteExplicitBond.bondEquiv k a, 8 • tick .compare⟩
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “entry”.
def entry {k : ℕ} (fields : Vector (Fields k) 2)
(a : Fin (2 * k + 6)) (out : Fin 2 × Fin (2 * k + 6)) : Run ℝ := do
let f ← StoredGivens.read fields out.1
let row ← decode k a
let col ← decode k out.2
storedBlock f row col
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “entry value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem entry_value {k : ℕ} (fields : Vector (Fields k) 2)
(a : Fin (2 * k + 6)) (out : Fin 2 × Fin (2 * k + 6)) :
(entry fields a out).value = blockView fields[out.1.val]
(HermiteExplicitBond.bondEquiv k a) (HermiteExplicitBond.bondEquiv k out.2) := by
commit-pinned source · Verso Blueprint panel
This definition gives the library's named construction or computation for “assemble”. Output columns are exactly finProdFinEquiv (bit, outgoing bond), as in StoredTensorTrain.denoteCore.
def assemble {k : ℕ} (fields : Vector (Fields k) 2) :
Run (StoredCore (2 * k + 6) (2 * k + 6)) :=
materialize fun a j => entry fields a (finProdFinEquiv.symm j)
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “assemble value”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem assemble_value {k : ℕ} (fields : Vector (Fields k) 2)
(a : Fin (2 * k + 6)) (out : Fin 2 × Fin (2 * k + 6)) :
denoteCore (assemble fields).value a out = blockView fields[out.1.val]
(HermiteExplicitBond.bondEquiv k a) (HermiteExplicitBond.bondEquiv k out.2) := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “stored block cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem storedBlock_cost_le {k : ℕ} (f : Fields k)
(a b : HermiteFiniteBond k) (op : Op) : (storedBlock f a b).cost op ≤ 12 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “entry cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem entry_cost_le {k : ℕ} (fields : Vector (Fields k) 2)
(a : Fin (2 * k + 6)) (out : Fin 2 × Fin (2 * k + 6)) (op : Op) :
(entry fields a out).cost op ≤ 29 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “assemble cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem assemble_cost_le {k : ℕ} (fields : Vector (Fields k) 2) (op : Op) :
(assemble fields).cost op ≤ 72 * (2 * k + 6)^2 := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “assemble total cost le”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem assemble_total_cost_le {k : ℕ} (fields : Vector (Fields k) 2) :
(∑ op : Op, (assemble fields).cost op) ≤ 576 * (2 * k + 6)^2 := by
commit-pinned source · Verso Blueprint panel
This record groups the data and proof fields needed for “source correct”. A proposition-valued field is a requirement until a constructor supplies it. Explicit supplier obligations.
structure SourceCorrect (k n t : ℕ) (L : ℝ) (bit : Fin 2) (f : Fields k) : Prop where
leftPartial : f.leftPartial = decide (Partial 0 (cutIndex n L)
(selectedChild (boundarySchedule (cutIndex n L)) (n - t) (decide (bit = 1)))
(2^(n-t)))
leftInjection : f.leftInjection = if Full 0 (cutIndex n L)
(selectedChild (boundarySchedule (cutIndex n L)) (n - t) (decide (bit = 1)))
(2^(n-t)) then leftInject (-Real.pi * L) (gridStep n L)
(selectedChild (boundarySchedule (cutIndex n L)) (n - t) (decide (bit = 1)))
(n-t) else 0
leftFree : f.leftFree = HermiteBoundaryInjection.leftFree (gridStep n L) (n-t)
(decide (bit = 1))
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “block view source”; the hypotheses and conclusion in the code panel fix its exact scope.
theorem blockView_source {k n t : ℕ} {L : ℝ} {bit : Fin 2} {f : Fields k}
(h : SourceCorrect k n t L bit f) (a b : HermiteFiniteBond k) :
blockView f a b = hermiteKernel k n L (n-t) (decide (bit = 1)) a b := by
commit-pinned source · Verso Blueprint panel
Lean checks the proposition indexed as “assemble source”; the hypotheses and conclusion in the code panel fix its exact scope. Strong entry refinement to the exact explicit layout kernel.
theorem assemble_source {k n t : ℕ} {L : ℝ} (fields : Vector (Fields k) 2)
(correct : ∀ bit : Fin 2, SourceCorrect k n t L bit fields[bit.val])
(a : Fin (2*k+6)) (out : Fin 2 × Fin (2*k+6)) :
denoteCore (assemble fields).value a out =
HermiteExplicitBond.kernel k n L t out.1 a out.2 := by
commit-pinned source · Verso Blueprint panel