SE Theory: Coreference

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

Coreference asks when two references are treated as referring to the same referent, in a stated context.

This repository defines the formal vocabulary and relations needed to reason about context-indexed co-reference judgments, the identity relation those judgments generate, and the distinct-commitments kept separate from them.

It does not own the abstract co-reference account (Neutral Substrate), the commitment calculus (Persistence), or whole formation and same-unit judgments (Individuation). It does not yet settle when a co-reference judgment is warranted or what licenses its continuation across contexts; that remains active research.

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.

Import

Downstream Lean projects should import the public surface:

import SE.Coreference

The public import surface is curated in:

SE/Coreference.lean

Developer

Maintain:

• lakefile.toml
• lean-toolchain
• reference/theory-reference.toml - hand-maintained configuration
• reference/*.toml - hand-maintained/scaffolded reference source artifacts
• Lean source + RR comments - 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-coreference

cd se-theory-coreference
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

MIT

Repository Manifest

SE_MANIFEST.toml