Status: Retired October 2026. No longer maintained.
This repository preserves an earlier Lean 4 formalization developed during the Structural Explainability research program. It informed the current research, which no longer builds on it.
Its definitions, assumptions, and results no longer authoritative and do not reflect current Structural Explainability theory.
It is preserved unchanged for historical reference and research provenance.
Current formalizations are maintained in Structural Explainability in the
se-theory-repositories.
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