Two values clash only while both hold

[WaylandYang]

Fixes #624. Fixes #634.

What was wrong

Three defects in how the consistency check judges asymmetric, functional and inverse_functional:

1. Identity came from scan order (Axiom violation identity depends on encounter order for asymmetry and functional constraints #624). left_fact/right_fact were the first two facts the checker happened to meet. axiom_violations is unique on (kb_id, kind, left_fact, right_fact), so the same clash read in another order became another row, and a resolved row was bypassed instead of reopened. Same disease as the cycle rotation fixed in The ledger keeps what its comments promise #620.
2. Time was ignored (Functional and asymmetry checks ignore validity time, and inverse functional is stored as functional #634). reasoning::run read every fact with its span and dropped the span before calling check. A raise (salary 28000 until 2024-02-20, 32000 from 2024-02-20) and a change of project lead were both reported as contradictions. derive::contradictions already required overlapping spans; the assertion side did not.
3. Inverse functional was stored as functional (Functional and asymmetry checks ignore validity time, and inverse functional is stored as functional #634), pointing the reviewer at the wrong end of the relation.

What changed

• utopia_reason::check takes TimedEdge. The three exclusive kinds flag two facts only when their half-open spans overlap, read exactly as derivation reads them (read_span: eternal predicates unbounded, undated events empty). Self-loops and cycles stay time-blind. That is unchanged here; see the note below.
• One finding per connected group of clashing facts: path is the whole group sorted by id, left/right are its first and last. With every order of the input the result is identical, and a long run of successive values is swept in O(n log n).
• Kind::InverseFunctional (inverse_functional), also used in derived-contradiction details.
• Persistence: an accepted group covers the facts it listed. A later group that is a subset stays silent even when its key changed, because a fact was retracted. A group that gained a fact the reviewer never saw reopens.
• Migration 0053: adds the kind to the check constraint; deletes open asymmetry/functional rows (recomputed on the next run); relabels resolved object-side rows as inverse_functional; canonicalises resolved rows to (least, greatest) with path set, keeping the earliest row when two orders were each decided.
• Review: a title for the new kind, wording that says "at once", the "N facts in the cycle" label only on cycles, "Both/All are right" by group size.

Verification

• utopia-reason: 77 tests, including every permutation for all three kinds, successions, unbounded and empty spans, and connected versus separate groups.
• New a_clash_needs_both_at_once (DB-backed):
  • three successions produce 0 rows;
  • overlaps produce one functional and one inverse_functional row;
  • the Axiom violation identity depends on encounter order for asymmetry and functional constraints #624 sequence (resolve as axiom_relaxed, flip heap order with a no-op UPDATE, re-run) gives inserted 0, reopened 1;
  • an acceptance survives a group growing and shrinking back.
• The full utopia-store suite passes locally. fmt, clippy -D warnings and pnpm build are clean.
• Migration run through sqlx on a copy of a DB at version 52, seeded with the old shapes: a reversed pair decided twice, a reversed functional row, an object-side row stored as functional, and an open row. The result matched the expectations above.
• End to end, on a copy of the temporal bench base where the old binary reported 2 false positives: POST /kbs/{id}/consistency/check now reports found: 0. After inserting two genuinely overlapping facts it reports one functional and one inverse_functional clash. Accepting one through the review endpoint and re-running gives inserted: 0, and the row stays resolved. The Review card renders the new title.

Not in this change

Cycles still ignore time: a transitive cycle whose edges never hold together is reported. Fixing that means intersecting spans along the whole path rather than pairwise overlap, so it is left for its own issue.

🤖 Generated with Claude Code