The compiler doesn't take your word for it.

While developing Sounio's octonion backend, we found a combinatorial fact that does not appear to have been stated explicitly in the literature: the number of ordered triples (i, j, k) in {1,…,7}³ for which the octonion associator [e_i, e_j, e_k] is nonzero is exactly 168 = |PSL(2,7)|. The decomposition reads 343 = 133 + 42 + 168.

The computation was performed in Sounio and independently reproduced in Python/NumPy. Verification repository: agourakis82/168-sedenion-bijection (14/14 pytest passing).

Paper: "The 168 Theorem: PSL(2,7) Governs Non-Associativity and Zero-Divisor Structure in the Cayley-Dickson Tower" — Agourakis & Gerenutti (2026). Submitted to Advances in Applied Clifford Algebras.

Sounio bootstraps from a 2,792-line C compiler (bootstrap/stage0.c) through a multi-stage chain into a self-hosted compiler. Stage 2 and Stage 3 produce byte-identical binaries — the canonical definition of a self-hosted fixed point. This was achieved on 2026-03-23.

Reproduce:

# Stage 0 → gen1 (from C compiler)
./artifacts/self-hosted/souc-self-hosted-x86_64 \
    self-hosted/compiler/lean_single.sio gen1.elf

# gen1 → gen2 (first self-hosted compile)
./gen1.elf self-hosted/compiler/lean_single.sio gen2.elf

# gen2 → gen3 (fixed-point check)
./gen2.elf self-hosted/compiler/lean_single.sio gen3.elf

# Verify
sha256sum gen2.elf gen3.elf

Expected: identical hashes. Recorded fixed-point SHA-256 (CHANGELOG): 7b588877f870e0011a9ace62eb12c7cd (741 KB). Cycle parity artifact: true.

ASHP 2020 §8.3 requires ε ≥ 0.82 for AUC-guided vancomycin dosing. The Sounio test tests/compile-fail/vancomycin_low_conf.sio attempts to pass a value with ε = 0.40 to a function with the signature fn prescribe_vancomycin(dose: Knowledge[f64, ε >= 0.82]). The compiler rejects the program. Not a lint, not a test suite — the type checker refuses to emit the program.

//@ compile-fail
//@ error-pattern: ε

// Vancomycin prescription safety: compile-time ε-bound enforcement.
//
// ASHP 2020 §8.3 mandates ε >= 0.82 before AUC-guided dosing is permitted.
// A dose derived solely from Cockcroft-Gault (ε=0.40, CV ~60%) is too uncertain.
// The compiler must reject assignment to the prescription slot at compile time.

// Prescribing function: only accepts dose estimates with ε >= 0.82.
fn prescribe_vancomycin(dose: Knowledge[f64, ε >= 0.82]) with IO {
    println("Vancomycin prescribed")
}

fn main() with IO {
    // CrCl-derived dose: 40% confidence only (severe renal impairment + age 84,
    // CG formula CV >> 28%, multiple co-morbidities).
    let risky_dose: Knowledge[f64, ε=0.40] = Knowledge { value: 500.0, epsilon: 0.40 }

    // ERROR: ε=0.40 violates the ε >= 0.82 lower bound required by
    // prescribe_vancomycin.  The compiler must reject this call.
    prescribe_vancomycin(risky_dose)
}

error: Type mismatch — expected confidence level not satisfied: Knowledge ε boundary violation at line 27

typecheck: failed

The committed stdlib reliability gate reports stdlib reliability · not in CI · artifact 2026-05-12 · engine unnamed (source: artifacts/stdlib/stdlib_reliability_status.v1.json). If this page disagrees with README.md or the artifacts, those sources win.

$ bash scripts/stdlib_reliability_gate.sh

stdlib reliability · not in CI · artifact 2026-05-12 · engine unnamed
# numeral withheld — engine unnamed, not in CI

The formal/ directory contains Lean 4 proofs of the core invariants of the epistemic type system — in particular, that uncertainty propagation preserves monotonicity and that confidence gates are sound under composition. No sorry. No Mathlib.