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