Not whether the system produced a good outcome, but whether it was entitled to decide.
Why agentic AI alignment is downstream of legitimacy — and why the Constitution
needs a compiler.
A Lean 4 formalization proving that capacity-achieving input priors are unique for finite-alphabet
Markov kernels with full-rank row matrices, together with a compact-Polish discharged theorem and
a measure-theoretic packaging theorem. Three layered results; sorry-free; Mathlib-only.
Prediction markets work best when the future doesn't care what the market thinks. An
incompleteness result: the more powerful they become, the larger the class of events they cannot price.
What changes when AI works inside a formal type system and hallucination is structurally rejected on contact.
Agentic coding is optimization, not authorship — and language choice determines the quality of the
feedback signal. Why Rust's type system makes the compiler an unambiguous oracle.
Every context switch leaves behind a shard of attention. Tabs multiply, threads blur. We spend more
time reconstructing state than building. The founding argument for anticipatory AI.