Apeiron

Two primitives. The first is ℝ[x]/(x² − σ): Cell<R> over a ring R, with σ passed as a value to every operation, so the elliptic, parabolic and hyperbolic faces share one implementation. Background: One multiplication, three geometries. The second is a hash table whose only write is insert_with; sets, maps, counters and adjacency lists are choices of merge function.

The choice of scalar is part of the specification. Over i64 the operations are ℤ/2⁶⁴, where commutativity, associativity and multiplicativity of the norm hold but the classification of faces does not (ℤ/2⁶⁴ has nilpotents at every σ). A dyadic scalar, m/2ᵉ, carries the idempotents (1 ± x)/2 and refuses on overflow instead of rounding. The idempotent constructors require a Halve bound, so Cell::<i64>::idem_plus() does not compile.

§Verification

The Rust is the executing artifact. Charon and Aeneas extract it to Lean 4, and each extracted function is proved to refine a canonical definition in the Lean corpus. Current state: the 64-bit cell multiplication and norm are refined (word_mul_denote, word_norm_denote). The growable table and most of the engine are not yet; the repository tracks which claims have proofs, which have tests, and which have neither.

§Inference engine

A CPU engine for quantised language models, built on the same primitives: GGUF loading, low-bit dequantisation, matrix-vector kernels, attention, RoPE, mixture-of-experts routing, Hadamard rotation and sampling. Benchmarks run against llama.cpp on a dedicated quiet host, and results are recorded with the commit and command that produced them. Numbers will be published with those receipts.

The target is local inference on consumer hardware with the kernels that serve each token refined against their specification. That target is not met.