req: the symbol-grep half of RATE-002's own re-promotion bar, and the record it asked for

[avrabe]

Both artifacts state the bar themselves — "the symbols present in shipped code AND a steps: entry greping them, so the same prose-only-citation drift cannot recur." And FV-FALCON-RATE-002 says what to do when the code arrives:

NO FAILING STEP WAS ADDED HERE, deliberately … Adding grep -q 'u_delivered_frac' now would redden a required check until the branch lands … The step gets added WITH the code, as the precondition for re-promotion.

The code landed on 2026-10-13 in #556. So the step gets added. That is the artifact's own instruction, not new policy.

What this fixes

#529's complaint has two halves, and only one was about absence: "the citation is PROSE, not a step, so the gate cannot see it." #556 flipped the absence by accident; the gate still couldn't see the drift in either direction.

Four greps now bind the description's named mechanism to the code:

grep	binds to
u_delivered_frac	the struct field, relay-adrc:133
fn set_delivered_fraction	the definition, relay-adrc:245
fn last_torque_scale	the definition, relay-mix-quad:264
self.adrc.set_delivered_fraction	the call site, falcon-core:975

Each was falsified by deleting the symbol in a copy and confirming the grep fails; each matches code, not a comment. All 15 steps run and pass (run from files, one per step).

What this does not do — and both artifacts now say so

#556 landed under the title "the ring is anti-windup, not tuning." These artifacts already refute that: the root cause is #488's resync_loop_rate (filters designed for 1 kHz, stepped at 250 Hz; reverting it restores 2.47 rad/s), and "the ESO was never the problem; the filter in front of it was."

The passages asserting the symbols are absent from main are now false. They are corrected in place rather than quietly dropped — the same style the artifact used when it corrected its own earlier "are fixed".

Status stays implemented

The bar's other half is unmet. The measured benefit (2.47 → 2.02 → 1.91 rad/s) is VOID — taken on the mis-designed filter, a regime that no longer exists — and nothing has re-measured it against the fixed baseline. A gz run on 2026-10-13 (dispatch 38454332223) read 0.0015 rad/s pre-kill with the mechanism present, against 0.00174 recorded without it: no regression, and no benefit either.

Maintainer decision 2026-10-13: keep the code, re-measure against the fixed baseline, correct the record. This is the record half; the measurement is owed.

Refs #529, #270, #556

🤖 Generated with Claude Code

https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG

[github-actions]

✅ Rivet verification gate — falcon

174/174 passed

count
Passed	174
Failed	0
Skipped (bench-only — needs hardware / sim)	21
Skipped (no steps)	12

Bench-only artifacts (not run by CI)

• FV-FALCON-ARCH-001 — spar AADL architectural model — falcon cascade (v0.13)
• FV-FALCON-ARCH-002 — spar codegen --format wit recheck — works at v0.10.0 (v0.15.0)
• FV-FALCON-COV-001 — witness MC/DC structural coverage — falcon pipeline wired (v0.13)
• FV-FALCON-COV-002 — cargo-llvm-cov statement coverage — workspace-wide (v0.14.0)
• FV-FALCON-COV-003 — witness MC/DC on real Rust source — Geofence subject (v0.14.1)
• FV-FALCON-GEO-003 — Geofence safety path — miri UB/overflow check (v0.12, AI substitute)
• FV-FALCON-LYAP-002 — Strict (cross-term) Lyapunov — exponential-decay inequality + CI-gated Lean proofs (v1.105)
• FV-FALCON-LYAP-004 — Lyapunov exponential convergence — the deferred 'trajectory ⇒ converges' step, discharged (v1.107)
• FV-FALCON-MATHF32-003 — MATHF32-P03 — machine-checked (Gappa→Flocq→coqc) rounding bound for the f32 sin polynomial (v1.127)
• FV-FALCON-MATHF32-004 — MATHF32-P04 — machine-checked (Coq-Interval) approximation bound for the f32 sin polynomial (v1.128)
• FV-FALCON-MATHF32-005 — MATHF32-P05 — machine-checked rounding + approximation bounds for the f32 cosine kernel (v1.129)
• FV-FALCON-MELD-001 — meld-fuse the verified cascade into a single module (v1.5.0)
• FV-FALCON-OCI-001 — OCI-P01 — signed per-component publish, WASI-free build, and through-wasm closed-loop proof (v1.129)
• FV-FALCON-SIM-001 — PX4-SITL end-to-end loop — recipe + preset + smoke (v0.14.0)
• FV-FALCON-SIM-005 — gz-transport NavSat + Home projection — position-dependent loops (v0.18.1)
• FV-FALCON-TARGET-001 — Verified flight core as a bare-metal ARM Cortex-M ELF + sim backend (v1.6.0)
• FV-FALCON-WASMCM-001 — Verified flight core runs in wasmtime as a CM component (v1.26.0)
• FV-FALCON-WASMCM-002 — All 8 falcon CM components build and bundle script emits versioned dist/ (v1.56)
• FV-FALCON-WCET-001 — Compositional WCET + flight-cascade schedulability, kernel-checked (v1.10.0)
• FV-FALCON-WIT-001 — Verified IEKF componentized + plugged into the composed cascade (v1.4.0)
• FV-RELAY-KANICI-003 — Orphaned-proof sweep completed — flight-support + HAL + infra Kani harnesses enforced in CI (v1.108)

Source of truth: artifacts/verification/FV-FALCON-*.yaml.