Reusable sub-proofs of verifications. The engine retrieves them before
solving and deposits new ones after a proof passes; every lemma is checked by the Lean 4 kernel at admission and ships
with the proofs that cite it. The Lemma Hub is not part of the trusted base.
| theorem | statement |
|---|
Engine.linear_zld | Engine: closed form of the linear Op Spec at integer indices. |
Engine.Implements.ofLanes | Engine: the verification contract follows from a decoder, a witness and per-lane values. |
Lemmas.online_softmax_rescale | Lemma Hub (built-in): online softmax rescaling by exp(m − m'). |
Engine.rmsnormOffset_zld | Engine: closed form of the (1 + w) RMSNorm Op Spec at integer indices. |
Lemmas.splitKV_lse_merge | Lemma Hub (built-in): split-KV merging in log-sum-exp form equals full attention. |
Engine.strided_inj3 | Engine: non-overlapping strided layouts are injective. |
Engine.sum_fin_trunc | Engine: lanes of a tile beyond the logical extent contribute nothing to a reduction. |
Engine.LemmaHub.tanh_eq_exp | Lemma Hub (built-in): tanh x = (exp 2x − 1)/(exp 2x + 1). |
Lemmas.tiled_floor_misses | Lemma Hub (built-in): ⌊n/B⌋ tiles miss the tail when B ∤ n. |
Lemmas.tiled_masked_sum | Lemma Hub (built-in): a masked tiled traversal covers [0, n) exactly once. |
Engine.tiled_range | Engine: a tiled loop accumulation equals the plain reduction (every tile size). |