Superseded Lean 4 formalization of neutral-substrate constraints for accountability-oriented systems under persistent interpretive disagreement.
This repository is superseded by the active se-theory-* and formal-contract repositories.
Active development has moved to:
This repository is retained for provenance, earlier implementation history, and compatibility with prior references. It may receive maintenance updates for tooling, build hygiene, metadata, or release alignment, but it is no longer the active theory source.
This repository provides an earlier Lean 4 formalization of structural constraints on ontological substrates intended to remain stable across incompatible interpretations, legal regimes, and analytic frameworks.
It does not define a concrete ontology or protocol. It establishes substrate-level conditions that such systems must satisfy to avoid embedding interpretation, authority, causality, or judgment into the structural core.
Use the active repositories for current work:
| Need | Use |
|---|---|
| Active neutral-substrate theory | se-theory-neutral-substrate |
| Machine-readable formal contract exports | se-formal-contract |
lake update
lake build
lake exe verify