se-verification-operational-identity

A reference-implementation check for the finite mathematical core of SE-210, Operational Identity: A Finite Audit of Declared and Implemented Rules of Sameness.

Purpose

The purpose of this project is to confirm the algorithmic and complexity claims are internally correct. It tests the core once R, the partitions, surfaces, and uses are supplied.

Checks

Two independent checkers consume the same supplied Instance:

• oracle.py: builds ~_tau, ~_sib, and ~=_d as explicit pair sets, computes closures by naive fixpoint, and applies Definitions 4.1, 4.3, 4.7, 4.8, and 4.10 by literal subset tests. No algorithmic shortcuts.
• fast.py: the near-linear procedure of Theorem 5.2: union-find closures, signature grouping for pi_d, and per-declared-block label comparison for faithfulness, witness detection, and the four-way classification, with no R x R ever materialized.

The two are diffed across four verdict fields: faithfulness, divergence-witness existence, sibling-relative classification, and regime substitution.

The diff runs across three sources of instances:

• the seven regression cases taken verbatim from the paper. These are 1) faithful/pass; 2) unpositioned; 3) sibling-aligned with substitution (Ex. 4.11); 4) aligned without substitution (Prop. 4.14); 5) sub-sibling (Prop. 4.15 and the Section 6 ruleTextVersion worked example (the same construction); 6) super-sibling (Rem. 4.16c); and 7) sibling-incomparable (Rem. 4.16d);
• an exhaustive-small deterministic sweep of 180 instances over 3 records, covering every classification pair, every surface value-partition, and four histories;
• a randomized batch, 20,000 instances by default.

Alongside the diff, the harness checks three properties directly: every extracted witness satisfies Definition 4.3; the Proposition 5.5 before/after pair flips the verdict from pass to fail when the history is extended; and a fail never reverts to pass under history extension (anti-monotonicity).

Check Failures

mutation_test.py-style injection confirms the differential catches each named failure mode:

• reversed refinement direction,
• swapped sub/super,
• dropping the restriction to declared classes, and
• conflating substitution with alignment (the error Prop. 4.14 forbids).

These mutants all get flagged.

Run

uv sync --extra dev --extra docs --upgrade

uvx se-verification-operational-identity

# or with args
uvx se-verification-operational-identity --random 20000 --seed 0

Nonzero exit from se_verification_operational_identity.check means a real disagreement: either the optimized procedure or the paper wording needs correction.

Family classifications used

Example Command Output

uv run se-verification-operational-identity --random 20000 --seed 0

====================================================================
SE-210 finite-core verification
====================================================================
regression cases        : 7/7 classified as asserted
monotonicity (Prop 5.5) : ok
exhaustive-small diffs  : 180 instances, oracle vs fast
randomized diffs        : 20000 instances (seed 0)
monotone property       : ok
--------------------------------------------------------------------
RESULT: all checks passed

Developer Command Reference

git clone https://github.com/structural-explainability/se-verification-operational-identity

cd se-verification-operational-identity
code .

uv self update
uv python pin 3.14
uv lock --upgrade
uv sync --extra dev --extra docs --upgrade

uvx pre-commit install
uvx pre-commit autoupdate

git add -A
uvx pre-commit run --all-files
# repeat if changes were made
uvx pre-commit run --all-files

# run locally with defaults
uv run se-verification-operational-identity

# or run locally with args
uv run se-verification-operational-identity --random 20000 --seed 0

# A nonzero exit from `se-verification-operational-identity` means a real
# disagreement: either the optimized procedure or the paper wording needs
# correction.

# types, tests, docs
uv run pyright
uv run pytest
uv run zensical build

# save progress
git add -A
git commit -m "update"
git push -u origin main

git fetch origin copilot/analyze-test-coverage
git switch copilot/analyze-test-coverage
uv sync --extra dev --extra docs --upgrade
uvx pre-commit run --all-files
git status

git add -A
uvx pre-commit run --all-files

uv run pyright
uv run pytest

uv run se-verification-operational-identity --random 20000 --seed 0

uv run zensical build

git add -A
git commit -m "fix copilot generated test formatting"
git push

Citation

CITATION.cff

License

MIT

Repository Manifest

SE_MANIFEST.toml