SE Theory: Transformation

Lean 4 formalization of foundational transformation theory for Structural Explainability.

This repository defines structural transformation vocabulary and relations.

It does not decide what persists through a transformation. Persistence, identity-regime behavior, domain-specific survival criteria, and operational policy belong downstream.

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

Import

Downstream Lean projects should import the public surface:

import SETheoryTransformation

The public import surface is curated in:

SETheoryTransformation.lean
SETheoryTransformation/Surface.lean

Build

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 --strict

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-transformation

cd se-theory-transformation
code .

In a VS Code terminal

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
uv run se-ref-validate
uv run se-ref-export
uv run se-ref-export --check
uv run se-validate --strict

# 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

Citation

CITATION.cff

License

MIT

Manifest

SE_MANIFEST.toml