Lean 4 formalization of the contextual structural explainability layer.
This repository provides a Lean 4 formalization of the Structural Explainability layer. It:
- encodes the 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 ensuring downstream specs compose without contradiction.
It depends only on spec-se.
lake update
lake build
lake exe verify