rmsnorm_contract::prop_scale_invariance asserts the ε=0 theorem against the ε=1e-6 implementation — fails whenever α²·mean(x²) ≈ ε (killed #3621 shard 1/3) #3627

What

aprender-core::contract_tests contracts::rmsnorm_contract::prop_scale_invariance FAILED on #3621 (workspace-test-shard (1/3), gx10-build, 21:21Z, job 106150239542) — TRY 1/2/3 all FAIL. Not env, not signal, not a #3621 regression (#3621 touches no rmsnorm file). The generated test asserts a property that is false in the regime its own generator reaches.

Mechanism (reproduced to 6 digits)

Minimal failing input: data = [0.0, -0.15964308], alpha = 0.012254778, tol 0.05.

y[1]        = -0.15964308 / sqrt(mean(x²)+ε)         = -1.414158   (ε = 1e-6)
y_scaled[1] = -0.00195633 / sqrt(mean((αx)²)+ε)      = -1.146122
mean((αx)²) = 1.91e-6  ≈ ε

Both numbers match the CI log exactly (sign*y[1]=-1.414158 vs y_scaled[1]=-1.1461217, diff=0.268). Once α²·mean(x²) is comparable to ε, the ε term is no longer negligible and RMSNorm(αx) ≠ sign(α)·RMSNorm(x) — by design of ε.

contracts/rmsnorm-kernel-v1.yaml says so itself: the obligation's Lean theorem is RMSNorm.rms_scale_zero_eps, notes: "Proved for ε=0". The proptest (pv probar --binding output, DO NOT EDIT) tests the ε=1e-6 implementation against the ε=0 theorem with no precondition excluding the ε-dominated regime. The "relax tolerance for small alpha" branch (tol = 0.05 when |α|<0.1) is a guess at the symptom, not the bound.

Why it presents as a flake

Proptest seeds are random per run; successes: 215 before the hit. nextest retries 2 and 3 fail in 0.005 s because proptest persisted the case to proptest-regressions/ on TRY 1 and replayed it — three tries are one failure. There is no tracked regression file for this test, so origin/main stays green until a seed lands in the regime.

Fix (owner's choice, both honest)

1. Test the ε>0 property. Exact: y_scaled = sign(α)·y·sqrt((m+ε)/(m+ε/α²)), m = mean(x²). Assert that with a relative tolerance (1e-4) — no magic 0.05.
2. Add the precondition the theorem needs. Filter the generator to α²·mean(x²) ≥ 1e4·ε (at 1e3·ε the ε term still contributes ~5e-4 relative, ×|y|≤√n ≈ 2.8e-3 absolute > tol 1e-3) and keep the ε=0 assertion.

The change goes in contracts/rmsnorm-kernel-v1.yaml (obligation Scale invariance: the ε>0 formal, Lean note naming the regime the ε=0 theorem covers) and the tracked test, hand-edited — see the withdrawn item below for why not pv probar. Ruled 21:40Z: option 1 (ε>0 form) — it tests what the code computes and excludes no regime.

done_when

• contracts/rmsnorm-kernel-v1.yaml Scale invariance obligation carries either the ε>0 formal or the α²·mean(x²) ≫ ε precondition; pv validate passes
• regenerated with pv probar --binding WITHDRAWN 21:40Z — b3 measured that pv probar --binding emits 7 #[ignore = "no binding available"] stubs for this contract; the tracked file's 5 real tests were produced by the pre-monorepo external generator (20dda945b, 2026-02-18) and the header is false (class row: 51 contract test files say 'DO NOT EDIT — regenerate with pv probar --binding' and pv probar cannot produce any of them — obeying the header replaces real tests with ignored stubs #3630). Instead: the tracked test is edited directly, the commit says so, and the file's header is replaced by a true one (hand-maintained, contract-bound)
• the minimal input above ([0.0, -0.15964308], α=0.012254778) is a committed regression case that PASSES under the new assertion (i.e. the fixed test is exercised on the exact input that killed PMAT-3430 Phases 3-4: three ggml enums become one (M1 complete) #3621), and a mutation that restores the ε=0 assertion turns it RED
• cargo nextest run -p aprender-core --test contract_tests prop_scale_invariance × 20 seeds green

Blocks #3621 (T-0 PR for 0.69.0). Do not re-run #3621 into this; land the fix first.