CORTEXA
← Browse
arxivcs.LOcs.AI2026-07-22

Operational Identity: A Finite Audit of Declared and Implemented Rules of Sameness

Denise M. Case

A record system declares when two records refer to the same entity, occurrence, scope, or rule. Its disclosed implementation mechanisms induce a corresponding operational identity relation. The declared and implemented relations may diverge systematically without producing a provenance gap or detectable contradiction. A system can apply, consistently and with every record individually correct, a rule of sameness that no artifact declares. This paper formalizes that implemented relation. A declared identity regime partitions a finite record domain into co-reference classes; a disclosed mechanism, through its typed identity-relevant outcomes, induces an operational identity partition of the same domain. The audit compares these partitions in the refinement lattice. A mechanism is faithful when the declared partition refines the operational partition, so no declared class is split. A divergence witness is a pair the declaration merges and the mechanism separates; such witnesses are decidable by pair enumeration. When an imported sibling basis also splits a declared class, local comparison with its partition yields sibling-aligned, sub-sibling, super-sibling, or sibling-incomparable divergence. This result reports only the relationship; it does not identify the basis carried by the mechanism. Global equality of the operational and sibling partitions is defined separately as regime substitution and does not follow from sibling alignment. A version field incremented on every textual edit inhabits the sub-sibling case by splitting declared classes more finely than either imported basis. The audit is three-valued and relative to the disclosed artifacts, evaluated surfaces, and identified uses; each boundary has a finite refuting witness. A passing verdict is non-monotone because extending the transformation history can merge declared classes and create a witness among records already examined.

View free PDFSource page

Related papers

arxivcs.LOcs.AIcs.SE2026-07-23

Encoding Event-B Proof Rules in Prolog: An Interactive Sequent Prover for ProB

Katharina Engels, Jan Gruteser, Michael Leuschel

Event-B is a formal method rooted in predicate logic and set theory. We encoded over 600 proof rules in Prolog, enabling a systematic, comprehensible proof analysis and construction. By integrating the proof rules into the Prolog-based validation tool ProB, we obtain an interacti…

View free PDFSource page
arxivcs.LOcs.AIcs.CCcs.CL2026-06-26

The Unverifiability of Artificial General Intelligence (AGI) Alignment, Static and Dynamic: From Trakhtenbrot's Wall to the Safety-Generality Tension

Jose Pascual Gumbau Mezquita

We establish the mathematical limits of AGI safety in two forms: verifying a fixed system, and verifying that a certified safety property persists once the system self-modifies. In the static case, no algorithm can certify a highly expressive AGI's safe behaviour infallibly, comp…

View free PDFSource page