Superseded Lean 4 formalization of identity-and-persistence regime families for neutral accountability substrates.
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 identity-and-persistence regime families for neutral accountability substrates.
The active theory line now treats the six regime families as a necessary lower
bound under neutrality assumptions and refines them into canonical profile kinds
in se-theory-identity-regimes.
The formalization applies to substrates intended to support:
- stability under durable interpretive disagreement;
- accountability across legal, political, and analytic frameworks;
- neutrality as exclusion of causal and normative execution;
- profile-relative identity and persistence.
It does not apply to:
- ontologies embedding causal or normative conclusions;
- systems relying on negotiated or consensus semantics;
- role-based or context-discriminated substrates;
- single-framework modeling environments.
Use the active repositories for current work:
| Need | Use |
|---|---|
| Active identity-regime theory | se-theory-identity-regimes |
| Machine-readable formal contract exports | se-formal-contract |
lake update
lake build
lake exe verify