A research program on how records stay the same, or stop being the same, as they change, built on a foundation that makes no causal or normative claims of its own.
Structural Explainability (SE) is a research program on how a record stays the same thing, or stops being it, as it changes: forks, revisions, merges, replications, a body of law like 40 CFR whose parts change while the whole persists. People mostly agree on these verdicts in practice. The aim is to find out how they decide, and to write the rules down explicitly enough that two defensible rules can be compared and their disagreement traced to specific commitments, instead of being buried in an identifier.
The foundation is a neutral substrate, designed to be pre-causal and pre-normative. It makes no causal or normative claims of its own; such claims can enter only as attributed assertions with a source. Parties who disagree can still share the same records when the stated assumptions hold. This foundation is formalized in Lean under stated assumptions.
What is open is which kinds of things need distinct identity treatment, and why they must differ. That remains active research. Papers, specifications, and other repositories written before this work may use an older inventory of kinds and are being revised as the theory settles.
SE keeps structural commitments separate from the claims built on them. The foundation records identity, structure, transformation, and change; interpretive claims sit above it, each attributed to a source.
Structural Explainability is not anti-interpretation; it is anti-implicit interpretation. Interpretation is welcome when it is stated, attributed, and open to dispute, so disagreement remains explicit, attributable, and contestable over time.
SE supports independently developed accounts of identity and change without requiring a single authority, ontology, or interpretation.
Lean 4 formalizations of SE concepts, relationships, and mathematical results.
Each repository owns its definitions, scientific claims, evidence, implementation, documentation, and release information.
Mathlib Mini is a small, unofficial, Mathlib-inspired foundation for Lean 4.
It provides the limited mathematical primitives needed by Structural Explainability theory repositories without requiring the full Mathlib library.
Mathlib Mini depends only on Lean core. Compatibility with corresponding Mathlib definitions and operations is verified separately.
- Repository: mathlib-mini/mathlib-mini
- Documentation: Mathlib Mini
Independent (leaf) theories require no other SE theory repository. Deps indicates a direct dependency on MM=MathlibMini or "-" for none.
| Deps | Repository | Role in Structural Explainability |
|---|---|---|
| MM | se-theory-neutral-substrate | Neutral structural and referential foundations, admissibility, and interpretive boundaries. |
| MM | se-theory-persistence | Identity survival and breakage under change, and the commitment calculus (consistency, required, forbidden, undetermined) other theories build on. |
| - | se-theory-transformation | Structural transformation vocabulary, operators, and intrinsic change semantics. |
| MM | se-theory-structural-assurability | Claim-relative evidentiary capabilities, observational limits, and conditions for resolving or failing to resolve claims about systems. |
Dependent and integrative theories are built on other theories. Deps lists direct SE theory dependencies, excluding transitive dependencies.
MM=MathlibMini, NS=neutral substrate, PS=persistence, TR=transformation, IND=individuation, IR=identity regimes.
| Deps | Repository | Role in Structural Explainability |
|---|---|---|
| MM+NS | se-theory-common-ground | Conditions under which a bounded referential fragment is compatible with a class of interpretive frameworks. |
| MM+NS+PS | se-theory-individuation | Conditions under which a presentation picks out one whole, and same-unit and distinct-unit judgments between presentations. |
| NS+PS | se-theory-coreference | Context-indexed co-reference judgments, the identity they generate, and the distinct-commitments kept separate from them. |
| PS+TR | se-theory-transformation-persistence | Connections between transformation classifications and persistence semantics. |
| NS+PS | se-theory-identity-regimes | Regime-relative identity criteria and their relationships to transformations. |
| PS | se-theory-operational-identity | Relationships between declared identity semantics and identity behavior induced by implementations. |
| TBD | se-theory-interpretive-kernel | Equivalence relationships and interpretation across distinct carriers. |
| NS+IR | se-theory-structural-explainability | Integration of foundational SE concepts and their structural relationships. |
| Repository | Role |
|---|---|
| se-theory-reference-kit | Shared validation, documentation, cataloging, and reference-artifact tooling for Lean theories. |
| se-protocols-research | Scientific source audits, theory construction, independent review, and theory acceptance procedures. |
Research papers develop and communicate the scientific and mathematical foundations of Structural Explainability.
| Repository | Subject |
|---|---|
| paper-100-neutral-substrate | SE-100: Neutral Substrates |
| paper-110-common-ground | SE-110: Common Ground |
| paper-200-identity-regimes | SE-200: Referential Regimes |
| paper-210-operational-identity | SE-210: Operational Identity |
| paper-220-interpretive-kernel | SE-220: Interpretive Kernel |
| paper-320-structural-assurability | SE-320: Structural Assurability |
Formal claims and their verification should be evaluated against the authoritative sources identified within each research repository.
Research pilots evaluate the applicability, explanatory value, and limitations of SE concepts against concrete cases and external evidence.
| Repository | Research Role |
|---|---|
| se-pilot-individuation-comparison | Source-grounded comparison of independently documented individuation accounts. |
| se-pilot-identity-preservation-supply-chain-software | Identity-preservation conformance across software supply-chain representations, including SBOM formats. |
| se-pilot-structural-assurability | Applied investigation of assurance claims, evidence capabilities, and evaluation limitations. |
These repositories provide executable constructions, independent checks, or domain-specific verification.
| Repository | Role |
|---|---|
| se-verification-self-similarity | Lean 4 mathematical cases testing individuation, co-reference, and persistence. |
| se-verification-operational-identity | Executable verification of finite Operational Identity constructions and algorithms. |
| se-verification-vulnerability-matching | Examination of identity semantics in software vulnerability matching. |
| se-verification-judicial-record | Structural verification for accountable judicial record systems. |
| se-interpretive-kernel | Executable finite interpretive-kernel constructions and witnesses. |
Reactive Research originated within Structural Explainability and is under active development as an independently implementable approach for use across research programs, disciplines, and organizations.
It models research objects and their typed relationships so that changes to definitions, evidence, implementations, or other research artifacts can generate explicit downstream revalidation obligations.
| Repository | Role |
|---|---|
| reactive-research-spec | Defines the research-object model, typed relationships, and change-impact semantics. |
| reactive-research-registry | Provides resolvable research objects, provenance, graph snapshots, and impact tracking. |
| reactive-research | Implements extraction, validation, resolution, and impact analysis tools. |
The SE Manifest Schema provides shared repository metadata validation and dependency-graph checks for the Structural Explainability research program.
These repositories apply SE structures and mapping concepts to external domains and information systems.
| Repository | Role |
|---|---|
| se-df | Domain formalization toolkit. |
| se-mapping-assurance | Structural mappings between assurance frameworks and SE assurance concepts. |
Government-source repositories and other domain resources are available through the organization repository index.
Structural Explainability develops through related but distinct activities:
- Papers develop and communicate scientific arguments.
- Theory repositories formalize definitions, assumptions, and mathematical consequences.
- Research pilots investigate whether proposed concepts apply faithfully to independently documented cases.
- Verification repositories examine specified formal, algorithmic, or implementation properties.
- Research protocols govern source analysis, adversarial review, and scientific acceptance.
For example,
se-theory-individuation develops formal constructions concerning individuation,
while se-pilot-individuation-comparison investigates the
source-grounded comparison of individuation accounts.