SE Theory: Individuation

Lean 4 formalization of foundational individuation theory for Structural Explainability (SE).

Individuation asks under what formal conditions a presentation picks out exactly one whole, given a stated criterion of whole co-membership.

This repository defines the formal vocabulary and relations needed to reason about structural settings, successful presentations, and same-unit and distinct-unit judgments.

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

Downstream Lean projects should import the public surface:

import SE.Individuation

The public import surface is curated in:

SE/Individuation.lean

Developer

Maintain:

• 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:

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

cd se-theory-individuation
code .

Setup and Run

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

.\sit.ps1
.\rel.ps1

# inspect shared theory-reference command surface
uvx se-theory-reference-kit@latest --help
uvx se-theory-reference-kit@latest validate --help
uvx se-theory-reference-kit@latest scaffold --help
uvx se-theory-reference-kit@latest export --help
uvx se-theory-reference-kit@latest catalog --help
uvx se-theory-reference-kit@latest inspect --help

# validate reference artifacts against the declared Lean public surface
uvx se-theory-reference-kit@latest validate
uvx se-theory-reference-kit@latest validate --strict

# scaffold reference artifacts from Lean public declarations
uvx se-theory-reference-kit@latest scaffold
uvx se-theory-reference-kit@latest scaffold --dry-run
uvx se-theory-reference-kit@latest scaffold --overwrite

# regenerate or check generated JSON artifacts from reference TOML
uvx se-theory-reference-kit@latest export
uvx se-theory-reference-kit@latest export --check

# build or verify the generated reference catalog
uvx se-theory-reference-kit@latest catalog
uvx se-theory-reference-kit@latest catalog --check

# inspect resolved repository configuration and reference declarations
uvx se-theory-reference-kit@latest inspect

# 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

License

Apache 2.0

Repository Manifest

SE_MANIFEST.toml