CI step names: "Prove" over a fixed sample (Refs #2161)

[gHashTag]

The remaining strong-named steps, read against what their tools do:

step name	evidence
Prove generated RTL == GF-T model (bit-exact)	14 topologies from a list, one seeded training run
Prove GF-T primitives bit-exact across C + Rust + model	N = 600 pairs drawn from 48 values
Prove the WHOLE trainer bit-exact in C	STEPS = 80, seeded
Exhaustive, every arm, whole domain	genuinely enumerates — "wherever the space is small"

Three name a proof over a fixed sample. The fourth is the real thing, and its own first line says exactly where the real thing stops.

The distinction was already in this repository — in the tools, in careful prose, by an author who plainly understood it. It had never reached the step names, and the step name is what a green check shows.

I checked for the wrong failure first

I expected an unseeded sample, which would make a "proof" draw different inputs every run. It is seeded (random.seed(202), random.seed(101)) and two consecutive runs are byte-identical. That is a strength with a shadow worth naming: the sample never moves, so a disagreement outside those 600 pairs cannot be found here however often CI runs.

Renamed to name the evidence, with DOES NOT CHECK blocks, and a WHAT THIS DOES NOT ESTABLISH section added to verify_emit_bitexact.py, which had none: the topologies are a list not a space, the run is fixed, and "synthesizes" is yosys reaching a cell count — not place-and-route, not timing, not silicon.

Two on the instrument

• My first scope note was invisible to tri claims because I wrote it in my own words. The fix was to use the repository's vocabulary, not to widen the detector — an established vocabulary is worth more than any single statement made in it, and widening it once per author ends in a regex that matches everything.
• tri claims reads workflows, so a limit stated in the tool is invisible to it. verify_exhaustive.py has the most careful scope statement in the tree and is reported as having none. Named in the tool's own docstring rather than papered over: a flag means worth reading.

§94 and §95.

Refs #2161

[github-actions]

📓 NotebookLM Notebook linked to this PR

• Notebook ID: b83263109fb055dc
• URL: https://notebooklm.google.com/notebook/b83263109fb055dc

This notebook contains session context, decisions, and artifacts for this work.

[github-actions]

PR Dashboard

Generated at: 2026-08-23 20:35:52 UTC

• CI step names: "Prove" over a fixed sample (Refs #2161) #2602 CI step names: "Prove" over a fixed sample (Refs #2161) | Created: 2026-08-23 | Updated: 2026-08-23 | 19 failing / 27 total
• Unbreak FPGA CI and correct two unbacked hardware claims #2081 Unbreak FPGA CI and correct two unbacked hardware claims | Created: 2026-08-11 | Updated: 2026-08-20 | 5 failing / 27 total

Summary

Status	Count
Total Open PRs	2
PRs with Failing Checks	1
PRs with All Checks Green	1
READY	0
FAILING	1
PENDING	0

Seal Status

• ⚠️ STALE -- sha256(compiler.rs)=76fdc57c6caa != manifest seal=87e5cbd3ad94.
  The committed NMSE numbers were certified against an older compiler.rs.
  Run scripts/reseal-check.sh locally for the two-step reseal command (advisory; not a merge gate).