SE Theory: Identity Regimes¶

Lean 4 formalization of the identity regimes of Structural Explainability.

This repository defines the six canonical identity regimes and the derived regime-profile structure over admissible neutral substrates.

It does not define substrate primitives, persistence behavior, domain semantics, or operational validation.

Boundary¶

This documentation is non-authoritative. All formal definitions, invariants, and theorems are defined exclusively in Lean source files under IdentityRegimes/.

If documentation and Lean diverge, Lean is correct.

Purpose¶

The identity regimes establish the structure of identity binding over admissible substrates.

They answer:

• What kinds of identity bindings are permitted?
• What structural roles do identities play?
• What requirements govern valid regime application?
• How are regime profiles derived from regimes?

They do not define the substrate on which they operate.

Scope¶

Includes¶

• Six canonical identity regimes
• Regime requirement structure
• Derived regime-profile structure (nine profiles)
• Profile-generating axes:
• identity basis
• split transformation
• Admissibility conditions for regime application over neutral substrates
• Necessity and sufficiency theorem structure
• Machine-checked Lean theorems

Excludes¶

• Neutral substrate primitives
• Substrate well-formedness
• Substrate separation constraints
• Persistence behavior
• Mapping semantics
• Domain-specific data or examples
• Operational validation logic
• Runtime systems

Basic¶

Identity regimes are defined over neutral substrates imported from se-theory-neutral-substrate.

The basic vocabulary introduces:

• Regime: a typeclass parameterized over an admissible neutral substrate
• RegimeKind: an enumeration of the six canonical regime identifiers
• RegimeBinding: the relationship between a regime and a locus

No regime semantics are defined at this layer. Basic provides names and structure only.

Formal definitions: IdentityRegimes.Basic

Structure¶

The root file provides a single import surface:

import IdentityRegimes

Internal module paths are not part of the public interface. The dependency order is:

Basic > Regimes > Requirements > Profiles > Transformations
> Admissibility > Embedding > LowerBound > NonCollapse > Theorems

Regimes¶

The six canonical identity regimes are:

Regimes are canonical and not derived from one another. They define identity-binding structure, not implementation behavior.

Formal definitions: IdentityRegimes.Regimes

Requirements¶

Each regime imposes structural requirements on the substrate loci to which it may be applied.

Requirements are organized as:

• Necessary conditions: what must hold for a regime binding to be valid
• Sufficient conditions: what guarantees a regime binding is admissible
• Exclusion conditions: what disqualifies a locus from a given regime

Requirements are regime-specific and non-overlapping by construction.

Formal definitions: IdentityRegimes.Requirements

Profiles¶

Regime profiles refine regimes along two axes of derivation. Profiles are not additional regimes; they are derived structure.

The nine canonical profiles are:

Profiles are finite, canonical, and exhaustive over the derivation axes.

Formal definitions: IdentityRegimes.Profiles

Transformations¶

Profiles are generated by two derivation axes applied to regimes:

Identity basis axis:

• single, content, structure, extension, locus, instrument

Split transformation axis:

• none (regime remains atomic)
• RF (refinement split)
• AD (decomposition split)
• BF (branching split)

A regime combined with an applicable split transformation yields a profile. Not all combinations are valid; validity is governed by regime requirements.

Formal definitions: IdentityRegimes.Transformations

Admissibility¶

A regime may only be applied over a substrate that is admissible in the sense defined by se-theory-neutral-substrate.

This repository assumes admissibility as a precondition and does not redefine it. The admissibility layer here establishes:

• that each regime binding is compatible with substrate admissibility
• that regime application does not violate substrate separation

Formal definitions: IdentityRegimes.Admissibility

Embedding¶

The embedding layer establishes how identity regimes are positioned over admissible neutral substrates.

An embedding is a structure-preserving map from a regime's requirement structure into the locus space of a given substrate.

Key properties:

• Embeddings are injective over loci
• Embeddings preserve regime requirements
• No two regimes produce the same embedding over the same substrate

Formal definitions: IdentityRegimes.Embedding

LowerBound¶

The lower bound results establish the minimum structural complexity required for a substrate to support a given regime.

For each regime, a lower bound theorem states:

• the minimum number of distinct loci required
• the minimum requirement conditions that must be satisfied

Lower bounds are tight: the witness constructions in Witness achieve them exactly.

Formal definitions: IdentityRegimes.LowerBound

NonCollapse¶

The non-collapse results establish that the six regimes are structurally distinct and cannot be identified with one another.

For each pair of regimes R₁, R₂:

• there exists a substrate and locus configuration that satisfies R₁ but not R₂
• the requirements of R₁ and R₂ are not equivalent

Non-collapse is necessary to establish that the regime enumeration is non-redundant and that profiles derived from distinct regimes remain distinct.

Formal definitions: IdentityRegimes.NonCollapse

Theorems¶

Machine-checked theorems established at this layer:

• Regime requirements are satisfiable: for each regime, at least one admissible substrate configuration satisfies its requirements
• Profiles are derivable: every canonical profile is reachable via the transformation axes from its parent regime
• Non-collapse: no two regimes are requirement-equivalent
• Lower bounds are tight: witness constructions achieve the stated lower bounds exactly
• Embedding injectivity: distinct loci map to distinct positions under any valid regime embedding

Formal proofs: IdentityRegimes.Theorems

Witness¶

Minimal concrete witnesses demonstrating satisfiability of each regime:

Each witness is a pair (S, L) where S is an admissible neutral substrate and L is a locus configuration satisfying the regime's requirements. Witnesses are constructed to achieve lower bounds.

Witnesses establish that all six regimes and all nine profiles have non-vacuous definitions.

Formal definitions: IdentityRegimes.Witness

ReferenceRequirements¶

Cross-reference index of regime requirements and the theorems that depend on them.

This section provides traceability between:

• requirement definitions in IdentityRegimes.Requirements
• admissibility conditions in IdentityRegimes.Admissibility
• theorems in IdentityRegimes.Theorems that cite those requirements

Formal definitions: IdentityRegimes.ReferenceRequirements

Design Principles¶

Regime Primacy¶

The six regimes are canonical and not derived:

• OBL
• NOR
• OCC
• CTX
• REC
• ENR

They define identity-binding structure, not implementation.

Profiles as Derived Structure¶

Regime profiles refine regimes.

• Profiles are not additional regimes
• Profiles are derived via explicit axes
• Profiles are canonical and finite (nine)

Axes of Derivation¶

Profiles are generated by two dimensions:

• Identity basis: single, content, structure, extension, locus, instrument
• Split transformation: none, RF, AD, BF

Separation¶

Identity regime definitions remain independent from:

• substrate construction
• persistence behavior
• interpretation
• operational concerns

Lean as Authority¶

All correctness is expressed and verified in Lean.

No external system defines or validates theory semantics.

Relationship to Other Theory Repositories¶

se-theory-neutral-substrate¶

Defines the admissible structural substrate.

This repository imports it.

se-theory-structural-explainability¶

Integrates substrate and regimes into cross-cutting theorems.

Imports both this repository and the neutral substrate repository.

Build¶

elan self update
lake update
lake build

Tooling¶

Python tooling is used for:

• documentation generation (Zensical)
• repository hygiene (pre-commit, ruff)

Python tooling must not:

• define correctness
• validate theory semantics
• replace Lean proofs