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 the contextual Structural Explainability layer.
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 the Structural Explainability layer. It:
- encodes neutrality constraints as predicates;
- defines conformance predicates shared by AE / EP / CEE;
- proves basic composability.
It intentionally includes no domain logic, no examples, no governance, and no interpretation. It provides a small predicate and typeclass layer for checking that downstream specifications compose without contradiction.
Use the active repositories for current work:
| Need | Use |
|---|---|
| Active Structural Explainability theory | se-theory-structural-explainability |
| Machine-readable formal contract exports | se-formal-contract |
lake update
lake build
lake exe verifynpx markdownlint-cli2 --fix