SE Theory: Structural Explainability

Lean 4 formalization of Structural Explainability integration.

Composes the neutral structural substrate and identity regimes into cross-cutting theorems, traceability relationships, and system-level structural invariants.

Theory Repositories: Context

• NeutralSubstrate defines admissible structure
• IdentityRegimes defines identity mechanisms
• StructuralExplainability composes them into system-level theorems

Owns

• Integration of neutral substrate and identity regimes
• Cross-cutting Structural Explainability theorems
• Traceability across substrate and regime layers
• Composition of admissibility and regime application
• System-level structural invariants
• Machine-checked Lean theorems

Does not own

• Neutral substrate primitives
• Identity regime definitions (OBL, NOR, OCC, CTX, REC, ENR)
• Regime requirement structure
• Regime-profile derivation
• Persistence behavior
• Mapping semantics
• Domain examples
• Operational validation
• Runtime systems

Design Constraints

• Lean is the only source of truth for correctness
• No executable entry points
• No exported runtime artifacts
• No cross-repo coupling beyond imports
• All guarantees are expressed as theorems

Documentation Constraints

• The documentation layer is descriptive only.
• Documentation sections must mirror Lean module structure.

Authority

• Lean source files are the only authoritative definition of:

  • types
  • predicates
  • theorems
  • proof obligations

• Documentation must not introduce or redefine formal semantics.

Prohibited in docs

• Restating formal definitions in alternative form
• Introducing new terminology not present in Lean
• Encoding rules or invariants not present in Lean
• Diverging naming from Lean modules

Allowed in docs

• Explanatory summaries
• Structural descriptions
• Navigation and orientation
• Non-authoritative theorem descriptions

Import

Single import surface:

import StructuralExplainability

Build

elan self update
lake update
lake build

Tooling

Python and other tooling may be used for:

• documentation generation
• formatting and linting
• repository automation

They must not:

• define correctness
• validate theory semantics
• replace Lean proofs

Command Reference

Show command reference

In a machine terminal

Open a machine terminal where you want the project:

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

cd se-theory-structural-explainability
code .

In a VS Code terminal

uv self update
uv python pin 3.15
uv sync --extra dev --extra docs --upgrade

uvx pre-commit install

git add -A
uvx pre-commit run --all-files
# repeat if changes were made
git add -A
uvx pre-commit run --all-files

# do chores
npx markdownlint-cli "**/*.md" --fix
uv run python -m zensical build

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

Citation

CITATION.cff

License

MIT

Manifest

SE_MANIFEST.toml