Source commit f0e32e2b8aae6a710892c5559d353da7ea70d637. Original-data numerical verification of two literal two-stage integrator witnesses.
Single Release adapter, no solver or optimal-family completeness claim; microbenchmark excludes resolution, setup, rendering and end-to-end use; limiter not established.
Seven measured batches of 28000 calls per fixture, after seven warmup batches. Each interval contains verify_trajectory, per-call literal checks, report assignment and consumption of every returned report; resolution and setup are outside. Values are batch elapsed time divided by calls, in nanoseconds per call. No comparator or speedup is claimed.
| Witness | Trials | Checked calls | Failures | Median ns/call | Min ns/call | Max ns/call |
|---|---|---|---|---|---|---|
| valid | 7 | 196000 | 0 | 3025.49 | 2813.37 | 3556.36 |
| violating | 7 | 196000 | 0 | 2907.27 | 2834.23 | 2988.21 |
| Witness | Bindings | Feasibility | Objective | Optimality | Completeness | Validated | Recomputed objective |
|---|---|---|---|---|---|---|---|
| valid | numerical_pass | numerical_pass | numerical_pass | unsupported | unsupported | unsupported | 1 |
| violating | numerical_pass | violation | numerical_pass | unsupported | unsupported | unsupported | 1 |
| Witness | Field | Violation | Scale | Tolerance | Satisfied |
|---|---|---|---|---|---|
| valid | initial[0] | 0 | 0 | 1e-08 | true |
| valid | states[0].singleton[0] | 0 | 0 | 1e-08 | true |
| valid | states[2].singleton[0] | 0 | 1 | 2e-08 | true |
| valid | controls[0].inequalities[0] | 0 | 1 | 2e-08 | true |
| valid | controls[0].inequalities[1] | 0 | 0.25 | 1.2499999999999999e-08 | true |
| valid | dynamics[0][0] | 0 | 0.25 | 1.2499999999999999e-08 | true |
| valid | controls[1].inequalities[0] | 0 | 1 | 2e-08 | true |
| valid | controls[1].inequalities[1] | 0 | 0.75 | 1.7500000000000001e-08 | true |
| valid | dynamics[1][0] | 0 | 1 | 2e-08 | true |
| valid | objective | 0 | 1 | 2e-08 | true |
| violating | initial[0] | 0 | 0 | 1e-08 | true |
| violating | states[0].singleton[0] | 0 | 0 | 1e-08 | true |
| violating | states[2].singleton[0] | 0 | 1 | 2e-08 | true |
| violating | controls[0].inequalities[0] | 0 | 1 | 2e-08 | true |
| violating | controls[0].inequalities[1] | 0 | 0.25 | 1.2499999999999999e-08 | true |
| violating | dynamics[0][0] | 0 | 0.25 | 1.2499999999999999e-08 | true |
| violating | controls[1].inequalities[0] | 0.25 | 1.25 | 2.25e-08 | false |
| violating | controls[1].inequalities[1] | 0 | 1.25 | 2.25e-08 | true |
| violating | dynamics[1][0] | 0.5 | 1.5 | 2.5000000000000002e-08 | false |
| violating | objective | 0 | 1 | 2e-08 | true |
The valid witness passes original transitions, domains and objective. The deliberately altered final control violates an original domain and transition. Both retain unsupported optimal-family completeness and validated-proof claims.
Hardware, compiler, pilot, timer overhead, and separate process CPU and memory observations are in the raw records and sidecars. The separate sample does not identify a source-level hotspot or establish the limiter. Setup, end-to-end latency, and internal phase counters were not measured.