Lean 4 formalization of the neutral structural substrate of Structural Explainability.
This repository defines the formal substrate conditions needed for Structural Explainability theory without encoding identity regimes, persistence behavior, domain semantics, or operational behavior.
For the full documentation, see docs/en/index.md.
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/neutral-substrate/ mirror the Lean public surface.
They do not define theory semantics independently of Lean.
Downstream Lean projects should import the public surface:
import NeutralSubstrate
The public import surface is curated in:
NeutralSubstrate.lean
NeutralSubstrate/Surface.lean
Use VS Code Menu:
View / Command Palette / Developer: Reload Window to refresh.
elan self update
lake update
lake build
lake build TestAll
uv run se-ref-validate
uv run se-ref-export --check
uv run se-validate --strictShow command reference
Open a machine terminal where you want the project:
git clone https://github.com/structural-explainability/se-theory-neutral-substrate
cd se-theory-neutral-substrate
code .uv self update
uv python pin 3.15
uv sync --extra dev --extra docs --upgrade
# install git hooks once per clone
uvx pre-commit install
# build Lean (source of truth)
lake build
lake build TestAll
# generate/check registry artifacts
uv run se-validate --strict
uv run se-ref-validate
uv run se-ref-export
uv run se-ref-export --check
# autofix and manual fix issues
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
uv run python -m pyright
uv run python -m pytest
uv run python -m zensical build
# save progress
git add -A
git commit -m "update"
git push -u origin main