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 and GPU 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. On Qwen2.5-0.5B Q4_K_M, the recorded GPU benchmarks reached 113,099 tokens/s on a 512-token prompt and 973.8 tokens/s generating 128 tokens on an RTX 5080: 1.79× and 1.11× llama.cpp's CUDA backend on the same model and device. An earlier CPU run on Qwen3.5-0.8B Q8_0 reached 2.45× prefill and 1.76× decode on an i9-14900KF. The results page gives the GPU workloads and measurements; the earlier CPU results give the other comparison.

The aim is local inference on consumer hardware, with proofs for the kernels serving each token. The complete engine refinement is ahead.

Selected algebra and performance records are explained on the results page, with their source snapshots and measurement conditions.

Results and evidence · Discuss collaboration, funding or a contract.