Skip to content

README.md

Latest commit

 

History

History
165 lines (115 loc) · 4.59 KB

README.md

File metadata and controls

165 lines (115 loc) · 4.59 KB

SE Theory: Structural Explainability

Docs Site Repo Tooling License

CI-Lean CI Docs Links

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