Logical-contradiction invariant for syn verify (spike, SYN-283 / #271)

Executive summary

syn verify proves storage coherence (index = a reproducible build of the Markdown) but not logical coherence. The one gap that matters: a contradiction introduced by a direct Markdown edit that bypasses the propose/accept gate, the gate’s SYN-242 detection never sees it, and storage-coherence invariants pass because the index faithfully mirrors the (now-inconsistent) Markdown. Recommendation: GO. A small, deterministic, O(N) invariant (INV-13) over the already-indexed valid-time columns catches the decidable cases without any model. Ship it in syn verify --deep (opt-in, like INV-4) as a follow-up; this doc is the design.

1. Context and premisses

Assumes v1.0/v1.2 shipped: the bitemporal model (ADR-027/031, valid-time columns

• entity_field_history from ADR-046) and the verify engine (INV-1/2/3/5, plus --deep INV-4 and --since INV-12). SYN-242 already detects contradictions at propose-time and forces the gate; there is no invariant verify can attest over the historical graph.

2. Analysis

2.1 What counts as a deterministic contradiction

Decidable without judgement, relative to valid-time (ADR-027):

• C1: two live mutually-exclusive values. The same entity carries two open (valid_until IS NULL) values of a single-valued field (status) over overlapping valid-time. After ADR-046 the live value is one column + a closed history, so C1 reduces to: a history row with valid_until IS NULL (a history entry must always be closed) or an overlap between a history interval and the live interval. Pure column check.
• C2: supersession cycle / dangling close. x-supersedes forms a cycle, or a fact is closed (valid_until set, x-invalidated-at) but nothing supersedes it and it is not a correction, an orphaned invalidation. Graph check over the supersedes column.
• C3: present-and-tombstoned. An entity both exists as a live row and is referenced as invalidated/removed by another fact. Column check.

Explicitly excluded (need a model): “the note says X but the linked decision implies not-X”, any natural-language disagreement. Out of scope by discipline.

What this means for Synapse: the decidable set is exactly the overlap / cycle / orphan checks over entities.valid_from/until/supersedes and entity_field_history: all already indexed. No new schema.

2.2 Reuse of core::contradiction

The propose-time rules (update_status field-flip, link rel-flip) are the pairwise core of C1/C3. The historical sweep differs only in that it runs over the whole index rather than one proposed pair, and adds the valid-time-overlap predicate. So: lift the comparison, add the interval overlap, a thin new function in core::verify that calls the same equality/flip logic. No duplication of the detection semantics.

What this means for Synapse: ~one new InvariantResult producer + a helper; the “what is a contradiction” definition stays single-sourced.

2.3 Cost

C1/C3 are O(N) with a GROUP BY (type,id,field) over entity_field_history + one pass over entities. C2 is O(E) over the supersedes edges (a forest, not a dense graph). No unbounded pairwise scan. Fits the verify --deep budget.

What this means for Synapse: bounded and cheap; safe to gate behind --deep (where INV-4 already lives) so the default verify stays fast.

2.4 Single-user value vs the gate

SYN-242 was scoped as “the human sees the diff at the gate”, which covers proposed writes. INV-13’s incremental value is the bypass path: a user (or a script, or a bad merge) editing Markdown directly never hits the gate, so a direct edit that opens a second live status is invisible today: verify passes because the index mirrors the Markdown. INV-13 is the only check that catches it. That is genuine, on-brand value (“the memory your agents can’t silently corrupt” extends to “…or you can’t silently corrupt by hand”).

What this means for Synapse: the invariant is not redundant with the gate; it guards the un-gated edit path, single-user included.

3. Recommendation

GO: ship INV-13 in syn verify --deep (opt-in), as a follow-up issue (SYN-316, v1.4). Deterministic, O(N), model-free, reuses core::contradiction semantics, guards the bypass path. Signed into the synapse.verify-report/1 like the other invariants. Discipline held: decidable cases only; semantic contradiction stays rejected. Not shipped in this spike (design-only per plan 012); the implementation is its own gated change with proptests over planted overlaps.

4. Open questions (for the build)

• Exact remediation UX when INV-13 fails: report the conflicting (type,id,field, intervals) like INV-1’s --rebuild list; never auto-resolve (that is the gate’s job).
• Whether a genuine real-world overlap (two truly-concurrent valid facts of a multi-valued field) must be distinguishable from a single-valued clash: key off the field’s cardinality in the registry (status is single-valued).