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/ declare the repository-owned classification, traceability, and export intent for the Lean public surface.

Generated artifacts under data/neutral-substrate/ are outputs. They do not define theory semantics independently of Lean or the reference artifacts.

The reusable se-theory-reference-kit owns the generic validation, scaffolding, cataloging, inspection, and export machinery. This repository owns its Lean source, reference declarations, and generated neutral-substrate artifacts.

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

Reference Configuration

The theory-reference workflow is configured by:

reference/theory-reference.toml

That file declares this repository's Lean public modules, reference artifact layout, export targets, and validation commands. Public symbols are declared in the reference artifacts themselves, not duplicated in Python configuration.

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

# inspect shared theory-reference command surface
uv run se-theory-reference --help
uv run se-theory-reference validate --help
uv run se-theory-reference scaffold --help
uv run se-theory-reference export --help
uv run se-theory-reference catalog --help
uv run se-theory-reference inspect --help

# validate reference artifacts against the declared Lean public surface
uv run se-theory-reference validate
uv run se-theory-reference validate --strict

# scaffold reference artifacts from Lean public declarations
uv run se-theory-reference scaffold
uv run se-theory-reference scaffold --dry-run
uv run se-theory-reference scaffold --overwrite

# regenerate or check generated JSON artifacts from reference TOML
uv run se-theory-reference export
uv run se-theory-reference export --check

# build or verify the generated reference catalog
uv run se-theory-reference catalog
uv run se-theory-reference catalog --check

# inspect resolved repository configuration and reference declarations
uv run se-theory-reference inspect

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

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

# build docs
uv run python -m zensical build

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

Authority Manifest

.accountability/surfaces.toml

Citation

CITATION.cff

License

MIT

Repository Manifest

SE_MANIFEST.toml