SE Theory: Individuation

Lean 4 formalization of foundational Individuation theory for Structural Explainability.

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

This repository formalizes structural settings, the conditions a presentation must meet to succeed, same-unit and distinct-unit judgments, one connectivity construction of whole co-membership, transport of these results between settings, and the connection to the Persistence commitment calculus.

• Lean API Reference
• GitHub Repository

Individuation

A structural setting fixes a granularity. It supplies eligible atoms, a presentation-admissibility predicate, a support function from presentations to sets of atoms, and an equivalence relation on eligible atoms read as whole co-membership. That relation is not strict identity of atoms.

A presentation succeeds when it is admissible and its support is exactly one equivalence class of eligible atoms. Same-unit and distinct-unit judgments are guarded by success: two successful presentations identify the same unit when their supports are equal, and distinct units when their supports share no atom.

One construction of whole co-membership is the equivalence relation generated by a bond relation on eligible atoms. Bonds read as same-whole commitments, and independently warranted separation commitments are checked against the generated relation using Persistence.

These relations are formal constructions. The construction is exclusive-whole and extensional, and neither commitment is a requirement of individuation in general. Why bond-connected atoms belong to the same intended whole, and which wholes are of the intended kind, depend on independently justified criteria supplied outside this repository.

Agreement on observed properties or structural descriptors does not establish identity of the intended referents. Distinct referents may agree on every recorded descriptor. Support equality establishes same-unit only within this construction, whose support interpretation and whole co-membership criterion require independent scientific justification for the intended kind.

Likewise, failure to establish sameness from available evidence does not establish distinctness. This limitation does not alter the formal same-or-distinct result for successful presentations within the exclusive-whole construction.

Dependencies

This repository is a theory-layer repository for Structural Explainability.

It depends on Mathlib and on two Structural Explainability theory repositories:

• Neutral Substrate, for the individuation account that the construction instantiates
• Persistence, for the commitment calculus

It does not import Transformation's operator taxonomy, effect dimensions, or state models.

The connection to Persistence is stated for carriers in Type, so those modules specialize atoms and presentations to universe 0.

Scope

Repository scope is defined in SE_MANIFEST.toml.

Exclusions

Repository exclusions are defined in SE_MANIFEST.toml.

Import

Downstream Lean projects should import the public surface:

import SE.Individuation