# Record 005 proof artifact

This package is a bounded, executable counterexample for a data migration. It
uses one synthetic account and three synthetic state-setting events. It contains
no employer names, data, schemas, policies, incidents, or performance figures.

The legacy rows and target rows use different field names. After the declared
migration mapping, they are identical. Nine checks pass: row counts, canonical
rows, identifiers, required values, canonical types, ISO dates, canonical row
hashes, references, and selected aggregates.

The consumer still changes its answer.

The reference consumer reconstructs state in effective-time order. The flawed
target consumer orders the same eligible events by recorded time. A late-arriving
event is therefore applied in a different position. Under the frozen synthetic
thresholds, the reference returns `HOLD` while the flawed target returns
`REVIEW` for four of the sixteen declared `(as_of, known_at)` scenarios.

## Reproduce

Requirements: Python 3.10 or newer. The implementation uses only Python's
standard library and its bundled SQLite interface.

From this directory, run:

```sh
python3 run.py
python3 run.py --verify-committed
python3 verify.py
```

`run.py` loads both representations into an in-memory SQLite database, performs
the structural checks, evaluates the bounded scenario grid, and automatically
reduces every divergence to a subset-minimal event history. It then verifies
the corrected target against the same frozen manifest and runs an incomplete
manifest as a negative control.

`verify.py` is an independent implementation. It does not import `run.py` and
does not use SQLite. It reconstructs the rows and replay with ordinary Python,
checks every file hash in `receipt.json`, and confirms the committed claims.

Machine-readable outputs:

- `results.json` contains every check, replay result, and minimal witness.
- `receipt.json` binds the results and documentation to SHA-256 file hashes.

## Outcome vocabulary

- `PROMOTE`: every declared consumer-visible result matches inside this bounded
  manifest.
- `SEMANTIC_DIVERGENCE`: at least one declared consumer-visible result differs,
  with a reproducible witness.
- `UNCOVERED`: a required semantic rule is missing, so the checker refuses to
  imply safety.

## Proof boundary

This artifact proves one narrow existential claim: rows can match under the
listed structural checks while a declared consumer decision changes because
event-order semantics changed. It also proves that the corrected implementation
matches the reference for all sixteen scenarios in this manifest.

It does **not** prove that these checks are exhaustive, that sixteen scenarios
cover a real system, that every migration needs this exact mechanism, or that
`PROMOTE` means universally safe. The score thresholds and routes are synthetic
teaching devices, not recommended policy. A production manifest would have to
name its actual consumers, observables, histories, time semantics, tolerances,
and approved behavioural changes.