SE Theory: Common Ground

Lean 4 formalization of fragment-relative common ground in Structural Explainability.

People who interpret a shared record in different ways can still agree on part of it: what it's about and what it records. The agreed part is common ground. This library asks when a small, bounded set of such agreed facts, a fragment, can coexist with every party's interpretation without contradiction.

Being an acceptable interpretation does not by itself guarantee that. The library states the extra condition an interpretation must meet, in terms of what it permits about the fragment's vocabulary, and separates what follows from the definitions from what must be assumed or justified.

Scope and exclusions are defined in SE_MANIFEST.toml. The Lean source states what is proved and under which assumptions. Results hold for a stated fragment and class of frameworks. This library states conditions in the abstract; it does not certify any concrete realization, which must justify its own referential fixing and framework class.

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.CommonGround

Developer

Maintain:

• scripts/get-basis.ps1 update $ExpectedItemCount from the paper
• formalization/source/se110-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-common-ground

cd se-theory-common-ground
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