docs(plan): record the real blocking structure — neither v0.7.1 nor v0.7.2 is cuttable

[avrabe]

Re-checked both plans against the live trackers and rivet list, not against the
plans' own prose.

T3's supply half — the only startable item — has landed

proofs/lean/PartitionSupply.lean discharges supplyGuarantee unconditionally
(0 sorry / 0 admit / 0 axiom / 0 native_decide), with the raw-budget
unsoundness machine-checked by decide rather than asserted, and the
Θ_eff = Θ − k side condition carried as an explicit hypothesis in the shape the
plan asked for. Its precondition (#286/#288 — proofs/lean/ was never compiled by
any workflow) is satisfied now that the lean job gates //proofs/lean:all.

REQ-OS-SCHED-001 still stays proposed, correctly — the demand half needs C_i,
and C_i needs T4.

Everything else is gated

item	release	blocked on	live state
T2 REQ-OS-OBJVERIFY-001	v0.7.2	synth#1057	open; 64% union coverage on synth 0.60.0
T3 demand half	v0.7.2	T4	supply half done
T4 REQ-OS-WCET-001	v0.7.2	scry#144 + synth#1063	both open
REQ-OS-TARGET-RV32-001	v0.7.1	synth#1102	open; 0 of 13 drivers cross
REQ-DRV-COMPONENT-001	v0.7.1	silicon (wdg G474+F100, adc F100)	hardware-gated
REQ-OS-PARTITION-TENANT-001	v0.7.1	silicon	hardware-gated

Neither release is cuttable, and no local work changes that — four upstream
trackers and one board stand between here and either cut.

Recording it because v0.6.0's failure mode was scope deferred silently, and a plan
that reads "in progress" while every item is gated reproduces that in a quieter form.

Where a release could come from instead — nowhere, and that is the finding

An earlier draft of this PR said v0.8.0 was "the honest place to look" because it
holds four verified artifacts with no cut against them. That was wrong, and
wrong in the direction that wastes a release cycle. The evidence for all four
shipped several tags ago:

artifact	evidence	tags containing it
REQ/VER-OS-TIMER-001	gust_timer_probe, added 2026-07-22	v0.5.0, v0.6.0, v0.7.0
REQ/VER-OS-TRITRACK-001	proofs/executor_proofs.v, added 2026-07-16	v0.4.0 … v0.7.0

Cutting a v0.8.0 from these would ship nothing new.

Every other release follows the convention release: = the release the work shipped
in (v0.3.0 holds 21 verified, v0.6.0 holds 7, v0.7.0 holds 6). A verified
artifact pointing at a release that does not exist yet is the anomaly — and it makes
the readiness query lie in the most misleading direction: it reports already
delivered scope as ready to ship.

This PR does not re-point those fields. Whether to correct them or keep them as a
deliberate hold is a scope decision, and moving scope silently is the thing this
document exists to argue against. REQ-TARGET-MODEL-001 / VER-TARGET-IWDG-001 at
v0.10.0 may be the same shape.

No artifact statuses are changed by this PR. It is a status record, not a scope move.

🤖 Generated with Claude Code

https://claude.ai/code/session_011QG86sovTbfnPNY9SfhSmo

[avrabe]

Closing temporarily to stay under gale's CI queue ceiling — each PR is ~60 jobs, and #312/#314 are mid-drain. The branch docs/release-blocking-structure is pushed and unchanged; reopening once those two merge.

Nothing here is time-sensitive: it is a status record, not a scope move.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!