Lean 4 formalization of Accountable Entities (AE): six named entity kinds and their mapping to six identity regimes.
| Entity Kind | Identity Regime |
|---|---|
| Actor | ActorBound |
| Locus | LocusBound |
| Instrument | InstrumentBound |
| Event | EventBound |
| Scope | ScopeBound |
| Observation | ObservationBound |
This mapping is total and one-to-one over the six accountable entity kinds. Formal coverage properties are proven in Lean.
lake update
lake build
lake exe verify