Lean 4 formal contract layer for Structural Explainability.
This repository contains the machine-checked formal substrate that authorizes the operational contracts consumed by SE constitution, kernel, mapspec, and regime repositories.
It separates formal proof obligations from operational contribution workflows. Contributors to operational SE repositories consume exported contract artifacts; they do not need to edit Lean files or discharge proof obligations.
- Lean 4 definitions for core SE formal constraints
- Machine-checked theorem status for selected invariants
- Exported contract artifacts used by operational repositories
- Versioned proof-to-contract traceability
- Operational validators
- Domain mappings
- Applied datasets
- Regime execution pipelines
- Interpretation-specific semantics
SEFormalContract/
- Basic.lean foundational types and shared predicates only
- Regime.lean identity regime declarations and regime-level constraints
- Neutrality.lean neutrality assumptions, claims, and theorem stubs/results
- Relation.lean allowed relation primitives for operational mappings
- Export.lean contract-facing declarations intended to be exported
elan self update
lake update
lake build
lake exe export_contractShow command reference
Open a machine terminal where you want the project:
git clone https://github.com/structural-explainability/se-formal-contract
cd se-formal-contract
code .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
# Run formal contract validation against
# exported artifacts (fail if contract is inconsistent)
uv run python -m se_formal_contract validate
# do chores
npx markdownlint-cli "**/*.md" --fix
uv run python -m ruff format .
uv run python -m ruff check . --fix
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