Seven papers establishing the theoretical foundations of governed intelligence. All proofs are machine-checked in Rocq 8.19 with zero admitted lemmas.
Formal analysis of the structural gap in AI effect governance. Every effectful system has two boundaries (expressiveness and governance) that are almost never identical. Rice's theorem proves the gap is permanent for Turing-complete systems. Proposes coterminous governance as testable criterion.
Five foundational results mechanized in Rocq 8.19 with zero admitted lemmas. ~12,000 lines across 36 modules, 454 theorems. Establishes Governed Cognitive Completeness as capstone. Extraction to OCaml NIF for the BEAM runtime governance kernel.
Machine-checked formalization proving effect-level governance can be imposed without reducing computational expressivity. Establishes seven properties including governed Turing completeness and subsumption asymmetry.
Algebraic semantics for governed AI execution. Defines GovernanceAlgebra (three axioms) and shows it gives rise to a symmetric monoidal category with verified coherence. All mechanized in Rocq with extraction to verified OCaml NIF.
Certified purity architecture converting governance enforcement from runtime convention to structural capability boundary. Four mechanisms: restricted WASM compilation, purity certificates, runtime verification gate, remote attestation.
Cryptographic distribution provenance system addressing dependency confusion attacks. Three components: registry identity (Ed25519), dual-signature model, authoritative namespace binding. Comparison across eight ecosystems.
Introduces governed homoiconicity: code-as-data manipulation is pure computation, data-as-code materialization is a governed effect. Machine forms are first-class values subject to structural inspection before materialization.
A six-part work laying out the complete argument: why current approaches fail, the four laws of governed intelligence, algebraic formulation, proof outlines, an existence proof via implementation, and implications for the field.