SE Theory: Neutral Substrate

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.

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/neutral-substrate/ 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.NeutralSubstrate

The public import surface is curated in:

SE.NeutralSubstrate.lean
SE.NeutralSubstrate/Surface.lean

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-neutral-substrate

cd se-theory-neutral-substrate
code .

In a VS Code terminal

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

elan self update
lake update

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

# Validate reference TOML against Lean symbols and public-surface coverage.
uv run se-ref-validate --strict
# Getting a warn lean_symbol declared as 'abbrev' for 'Ontology'` is ok.

# Regenerate JSON artifacts from reference TOML.
uv run se-ref-export

# Confirm generated JSON artifacts are current.
uv run se-ref-export --check

# Run the full repo validation gate:
# strict reference validation plus generated-export freshness check.
uv run se-validate --strict

# validate manifest file
uvx --from se-manifest-schema se-manifest validate-manifest --strict

# fix issues
git add -A
uvx pre-commit run --all-files
# repeat if changes were made
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

Citation

CITATION.cff

License

MIT

Manifest

SE_MANIFEST.toml