# Persistence

This module defines the abstract persistence interface used by a referential regime.

Persistence concerns strict diachronic identity: whether eligible whole stages count as stages of the same continuing unit across two settings.

This module exposes only the boundary required by Neutral Substrate. It does not provide the substantive persistence theory that determines which criteria, stages, settings, paths, or histories are scientifically warranted.

In particular, this interface does not identify persistence with:

• temporal proximity;
• continuity alone;
• transformation;
• provenance;
• succession;
• carrier equality;
• individuation;
• co-reference.

No path quantifier, route semantics, stage-membership relation, existence-at-setting relation, equivalence-relation laws, decidability, finiteness, enumeration, or computational representation is assumed here.

structure SE.Substrate.PersistenceAccount (Referent : Type u) : Type (u + 1)

A persistence account for one referent kind.

The account itself represents the governing persistence criterion.

Setting supplies the settings between which persistence may be evaluated. Stage supplies the eligible whole-stage candidates to which a persistence judgment may apply.

The Referent parameter records the referent kind governed by this account. No generic stage-to-referent membership relation is introduced here.

• Setting : Type u

  Settings relevant to persistence judgments.

• Stage : Type u

  Candidate stages relevant to persistence judgments.

• eligibleStage : self.Setting → self.Stage → Prop

  Whether a candidate stage is eligible for persistence evaluation at the selected setting.

  Eligibility is distinct from a positive persistence judgment.

• persists : self.Setting → self.Setting → self.Stage → self.Stage → Prop

  Whether two eligible stages stand in strict persistence across the selected settings.

  This is a diachronic-identity judgment. It is not merely continuity, provenance, succession, or transformation.

structure SE.Substrate.PersistenceRegime (R : Referent.ReferentCarriers) : Type (u + 1)

The persistence accounts for the three referent kinds distinguished by Structural Explainability.

Each referent kind has its own persistence account. The substantive persistence theory governing those accounts remains external to this interface.

• entity : PersistenceAccount R.Entity

  Persistence account for entities.

• occurrence : PersistenceAccount R.Occurrence

  Persistence account for occurrences.

• institutionalArtifact : PersistenceAccount R.InstitutionalArtifact

  Persistence account for institutional artifacts.