# Finite-model results

Assertions passed: 120

Initial budget: 1500 ms, satisfied.
After one local base edit: 1650 ms, satisfied.
After selected cosmetic update: 1650 ms, satisfied; exact pins differ.
Outside budget/consumer/global case: exact records unchanged.
Updated left baseline: 750 controls2:ms; current: 900 controls1:ms; declared kind controls2:Duration.
Right instance/base/map: exact original.
Contract path projection: data1/Code -> data2/Code and data1/Operation -> data2/Operation.
Changed field cardinality: selective candidate rejected.
Strict revision identity: old/new refs unequal.
Same-origin typed compatibility: cosmetic revision accepted; Energy/Torque, other origin, changed contract rejected.
Bridge alternative: 2 explicit validated direct witnesses; changed contracts rejected.
Stable vocabulary alternative: exact common pin survives pattern change; vocabulary change remains unresolved without compatibility/migration.
Subjectless explicit C+K selected; unrelated G omitted; selected G requires Q boundary.
OA/SA: explicit pinned counterpart or independent local derivative; refined reverse counterpart fails exact transformed contract.

D1: 28df5ea3447918dfee3c6ed4243d8f986c689f93a54d89c6181b47d6c2f39b33
D2: a35102e04b9f6822ab409ab43f83eded33edd0a3a3c1f589245bb7b123ce4779
D3: 4b05d6a15115448e318d0c5d567ebb0bb9e0ab6438bd238e5f3a0716c7db1ee8

This dialect uses opaque symbolic identities, a restricted AST, one package per import and scalar integer-millisecond arithmetic. It is not Studio source, a full package dependency solver, production UUID allocation, complete data/operation/transition admission, REST or native acceptance.