SE Theory: Neutral Substrate

Lean 4 formalization of the neutral structural substrate of Structural Explainability.

Scope and exclusions are defined in SE_MANIFEST.toml. The Lean source states what is proved and under which assumptions. This library states neutrality conditions in the abstract; it does not certify any concrete realization, which must justify its own referential fixing and framework compatibility.

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/ mirror the Lean public surface. They do not define theory semantics independently of Lean.

The CI-Lean workflow builds the declared public Lean surface with lake build --wfail, failing on reported warnings, including sorry. Successful compilation verifies formal declarations against their stated assumptions; it does not establish the scientific adequacy of those assumptions or interpretations.

Import

Import the public theory surface:

import SE.NeutralSubstrate

Developer

Maintain:

• scripts/get-basis.ps1 update $ExpectedItemCount from the paper
• formalization/source/se100-lean-basis.md - from the paper
• lakefile.toml
• lean-toolchain
• reference/theory-reference.toml - hand-maintained configuration
• reference/*.toml - reference source artifacts
• Lean source and RR traceability comments (-- RR.DEFINES, -- RR.IMPLEMENTS) - hand-maintained theory source

Clone and Open Project in VS Code

Open a machine terminal where you want the project and open in VS Code:

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

cd se-theory-neutral-substrate
code .

Setup and Run

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

.\sit.ps1
.\rel.ps1

# shared theory-reference tooling: commands and options
uvx se-theory-reference-kit@latest --help

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

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

Authority Manifest

.accountability/surfaces.toml

Changelog

CHANGELOG.md

Citation

CITATION.cff

Documentation

Documentation - descriptive orientation

Formal Semantics

Lean

License

Apache 2.0

Repository Manifest

SE_MANIFEST.toml - repository semantic ownership/scope

Reference

reference/ - public-surface classification and traceability