SE Theory: Persistence

Lean 4 formalization of foundational persistence theory for Structural Explainability (SE).

Persistence asks when something should still count as the same identity after it has been transformed.

This repository defines the formal vocabulary and relations needed to reason about identity survival, breakage, invariance, and equivalence under transformation.

It does not own transformation theory itself, identity regimes, domain-specific survival criteria, accountable entities, evolution protocols, or operational policy.

For the full documentation, see docs/en/index.md.

Authority

Lean source files are authoritative for formal definitions, predicates, axioms, theorems, proof obligations, and reference rules.

Reference artifacts under reference/ and generated artifacts under data/persistence/ mirror the Lean public surface. They do not define theory semantics independently of Lean.

Import

Downstream Lean projects should import the public surface:

import SE.Persistence

The public import surface is curated in:

SE/Persistence.lean

Developer

Maintain:

• lakefile.toml
• lean-toolchain
• reference/theory-reference.toml - hand-maintained configuration
• reference/*.toml - hand-maintained/scaffolded reference source artifacts
• Lean source + RR comments - hand-maintained theory source

Clone and Open Project in VS Code

Open a machine terminal where you want the project:

git clone https://github.com/structural-explainability/se-theory-persistence

cd se-theory-persistence
code .

Setup and Run

Use VS Code Menu: View / Command Palette / Developer: Reload Window to refresh.

.\sit.ps1
.\rel.ps1

# inspect shared theory-reference command surface
uvx se-theory-reference-kit@latest --help
uvx se-theory-reference-kit@latest validate --help
uvx se-theory-reference-kit@latest scaffold --help
uvx se-theory-reference-kit@latest export --help
uvx se-theory-reference-kit@latest catalog --help
uvx se-theory-reference-kit@latest inspect --help

# validate reference artifacts against the declared Lean public surface
uvx se-theory-reference-kit@latest validate
uvx se-theory-reference-kit@latest validate --strict

# scaffold reference artifacts from Lean public declarations
uvx se-theory-reference-kit@latest scaffold
uvx se-theory-reference-kit@latest scaffold --dry-run
uvx se-theory-reference-kit@latest scaffold --overwrite

# regenerate or check generated JSON artifacts from reference TOML
uvx se-theory-reference-kit@latest export
uvx se-theory-reference-kit@latest export --check

# build or verify the generated reference catalog
uvx se-theory-reference-kit@latest catalog
uvx se-theory-reference-kit@latest catalog --check

# inspect resolved repository configuration and reference declarations
uvx se-theory-reference-kit@latest inspect

# validate SE manifest file
uvx se-manifest-schema validate-manifest --path SE_MANIFEST.toml --strict

# save progress
git add -A
git commit -m "update"
git push -u origin main

Authority Manifest

.accountability/surfaces.toml

Changelog

CHANGELOG.md

Citation

CITATION.cff

Documentation

Documentation

License

MIT

Repository Manifest

SE_MANIFEST.toml