PMAT-3627: rmsnorm scale invariance asserts the ε>0 property — the ε=0 theorem was false where the generator reaches

contracts/rmsnorm-kernel-v1.yaml

@@ -50,7 +50,7 @@ proof_obligations:
 - id: RN-INV-005
   type: invariant
   property: Scale invariance
-  formal: RMSNorm(α·x) = sign(α) · RMSNorm(x) for α ≠ 0
+  formal: "∀ α ≠ 0: RMSNorm(α·x) = sign(α) · RMSNorm(x) · √((m + ε) / (m + ε/α²)), m = mean(x²); the factor → 1 as α²·m/ε → ∞"
   applies_to: all
   lean:
     theorem: RMSNorm.rms_scale_zero_eps
@@ -62,7 +62,8 @@ proof_obligations:
     - Real.sqrt_sq_eq_abs
     mathlib_imports:
     - Mathlib.Data.Real.Sqrt
-    notes: Proved for ε=0; RMS(αx) = |α|·RMS(x). Full RMSNorm scale invariance follows.
+    notes: "Proved for ε=0: RMS(αx) = |α|·RMS(x), i.e. the formal's factor is exactly 1. That is the α²·mean(x²) ≫ ε regime ONLY. With ε = 1e-6 in the implementation the factor is < 1 whenever α²·mean(x²) is comparable to ε -- PMAT-3627: data = [0, -0.15964308], α = 0.012254778 gives α²·m = 1.91e-6 and a 19% discrepancy from the ε=0 form. The proptest asserts the ε>0 formal with a relative tolerance; the ε=0 theorem is its limit, not its statement."
+
 - id: RN-BND-006
   type: bound
   property: RMS denominator is positive
@@ -184,9 +185,9 @@ falsification_tests:
   if_fails: Division by zero when ε too small
 - id: FALSIFY-RN-002
   rule: Scale invariance
-  prediction: RMSNorm(α·x) ≈ sign(α)·RMSNorm(x) for α ≠ 0
-  test: proptest scaling random vectors by random α
-  if_fails: Epsilon not scale-invariant in implementation
+  prediction: "RMSNorm(α·x) = sign(α)·RMSNorm(x)·√((m+ε)/(m+ε/α²)) to relative 1e-4, for every α the generator reaches -- including α²·m ≈ ε, where the ε=0 form is off by ~19%"
+  test: "proptest scaling random vectors by random α (prop_scale_invariance) + the committed #3621 killing input (regression_3627_scale_invariance_in_the_eps_dominated_regime)"
+  if_fails: "The implementation's ε does not enter the denominator as sqrt(m+ε), or the test has regressed to the ε=0 form -- the regression case turns RED on exactly that mutation (rel=0.19)"
 - id: FALSIFY-RN-003
   rule: SIMD equivalence
   prediction: '|rmsnorm_avx2(x) - rmsnorm_scalar(x)| < 4 ULP'

crates/aprender-core/tests/contracts/rmsnorm_contract.rs

@@ -1,7 +1,13 @@
 // CONTRACT: rmsnorm-kernel-v1.yaml
-// HASH: sha256:a1c7f2e8d3b49061
-// Generated by: pv probar --binding
-// DO NOT EDIT — regenerate with `pv probar --binding`
+// HAND-MAINTAINED, contract-bound. Every test here is named by an obligation or a
+// FALSIFY-NORM row in contracts/rmsnorm-kernel-v1.yaml; edit both together.
+//
+// This file once said "DO NOT EDIT — regenerate with `pv probar --binding`". That was
+// false (PMAT-3627, measured 2026-09-20): the in-tree `pv probar` emits seven
+// `#[ignore = "no binding available"]` stubs for this contract and cannot produce these
+// bodies, which came from the pre-monorepo generator on 2026-02-18. Obeying the old
+// header would have replaced five real property tests with seven ignored stubs. The
+// same false header stands on the rest of tests/contracts/ -- that is #3630.
 
 use aprender::autograd::Tensor;
 use aprender::nn::Module;
@@ -46,17 +52,27 @@ proptest! {
         let y_orig = norm.forward(&x);
         let y_scaled = norm.forward(&x_scaled);
 
+        // The eps>0 property (PMAT-3627). With eps = 1e-6 in the denominator,
+        //     RMSNorm(alpha*x) = sign(alpha) * RMSNorm(x) * sqrt((m+eps) / (m+eps/alpha^2)),
+        //     m = mean(x^2),
+        // exactly. The eps=0 theorem (RMSNorm.rms_scale_zero_eps) is the k -> 1 limit
+        // and is FALSE whenever alpha^2*m is comparable to eps: the input that killed
+        // #3621 had alpha^2*m = 1.91e-6 and a 19% discrepancy. Asserting the eps>0 form
+        // tests what the implementation computes, in every regime the generator
+        // reaches, with a relative tolerance instead of the guessed `0.05 if |alpha|<0.1`.
+        let eps = 1e-6f32;
+        let m: f32 = data.iter().map(|&v| v * v).sum::<f32>() / n as f32;
+        let k = ((m + eps) / (m + eps / (alpha * alpha))).sqrt();
         let sign = alpha.signum();
         let orig_data = y_orig.data();
         let scaled_data = y_scaled.data();
         for i in 0..n {
-            let expected = sign * orig_data[i];
-            let diff = (expected - scaled_data[i]).abs();
-            // Relax tolerance for small alpha (FP32 precision degrades near zero)
-            let tol = if alpha.abs() < 0.1 { 0.05 } else { 1e-3 };
+            let expected = sign * orig_data[i] * k;
+            let denom = expected.abs().max(1e-3);
+            let rel = (expected - scaled_data[i]).abs() / denom;
             prop_assert!(
-                diff < tol,
-                "scale invariance: sign*y[{i}]={expected} vs y_scaled[{i}]={}, diff={diff}",
+                rel < 1e-4,
+                "scale invariance (eps>0 form): sign*y[{i}]*k={expected} vs y_scaled[{i}]={}, rel={rel}, k={k}, alpha={alpha}, m={m}",
                 scaled_data[i]
             );
         }
@@ -167,3 +183,47 @@ fn falsify_norm_003_rmsnorm_sign_preservation() {
         );
     }
 }
+
+/// Regression for #3627 — the exact input that killed #3621's shard 1/3.
+///
+/// α²·mean(x²) = 1.91e-6 ≈ ε = 1e-6, so the ε term is not negligible and
+/// RMSNorm(αx) ≠ sign(α)·RMSNorm(x). The ε=0 theorem (`RMSNorm.rms_scale_zero_eps`,
+/// "Proved for ε=0") does not apply in this regime; the implementation is correct and
+/// the old assertion was wrong. Numbers reproduced to 6 digits independently of the
+/// CI log: y[1] = -1.414158, y_scaled[1] = -1.146122, diff 0.268 > tol 0.05.
+///
+/// This case must PASS under the ε>0 assertion and turn RED when the ε=0 one is
+/// restored — that is the mutation #3627's done_when asks for.
+#[test]
+fn regression_3627_scale_invariance_in_the_eps_dominated_regime() {
+    let data = [0.0f32, -0.159_643_08];
+    let alpha = 0.012_254_778f32;
+    let n = data.len();
+    let norm = RMSNorm::without_affine(&[n]);
+    let x = Tensor::new(&data, &[1, n]);
+    let scaled: Vec<f32> = data.iter().map(|&v| v * alpha).collect();
+    let x_scaled = Tensor::new(&scaled, &[1, n]);
+    let y = norm.forward(&x);
+    let y_scaled = norm.forward(&x_scaled);
+    let eps = 1e-6f32;
+    let m: f32 = data.iter().map(|&v| v * v).sum::<f32>() / n as f32;
+    let k = ((m + eps) / (m + eps / (alpha * alpha))).sqrt();
+    let sign = alpha.signum();
+    for i in 0..n {
+        let expected = sign * y.data()[i] * k;
+        let denom = expected.abs().max(1e-3);
+        let rel = (expected - y_scaled.data()[i]).abs() / denom;
+        assert!(
+            rel < 1e-4,
+            "3627 regression (eps>0 form): sign*y[{i}]*k={expected} vs y_scaled[{i}]={}, rel={rel}, k={k}",
+            y_scaled.data()[i]
+        );
+    }
+    // and the number the CI log reported, so the case is anchored to the incident
+    assert!(
+        (y_scaled.data()[1] - (-1.146_122f32)).abs() < 1e-5,
+        "y_scaled[1]={}",
+        y_scaled.data()[1]
+    );
+    assert!((k - 0.810_462f32).abs() < 1e-5, "k={k}");
+}

docs/audits/quorum-PMAT-3627.json

@@ -0,0 +1,190 @@
+{
+  "ticket": "PMAT-3627",
+  "base": "origin/main",
+  "base_resolved": "origin/main",
+  "base_note": "no origin/origin/main exists; judged against the local ref",
+  "head": "fd068099fd8ad3a31c802c18ee1655944dfad49e",
+  "diff_sha256": "f5e1d823ea1181490c7c8a8d37c2a70428b100218e63e0cbe5053083af65bb92",
+  "width": 3,
+  "executor": "agy",
+  "prompt_mode": "inline",
+  "prompt_bytes": 12982,
+  "author": {
+    "model": "claude-opus-5",
+    "family": "claude",
+    "source": "flag"
+  },
+  "agreed": true,
+  "lanes": [
+    {
+      "lane": 1,
+      "status": "SUCCESS",
+      "verdict": "PASS",
+      "summary": "The PMAT-3627 diff has been thoroughly reviewed and mathematically verified. It perfectly implements the acceptance criteria by replacing the incorrect ε=0 scale invariance theorem with the exact ε>0 invariant, tightening the gate to a 1e-4 relative tolerance, and explicitly anchoring the #3621 incident vector in a new regression case. The file headers are properly updated, and the PMAT-3627 roadmap entry is cleanly appended. No refutations found; the fix is correct.",
+      "findings": [
+        {
+          "claim": "The updated scale-invariance proptest (prop_scale_invariance) correctly introduces the ε>0 scaling factor √((m + ε) / (m + ε/α²)) which resolves the 19% discrepancy when α²·mean(x²) ≈ ε. Additionally, the test gate is structurally tightened from an absolute tolerance of 0.05 (for small α) to a much stricter 1e-4 relative error.",
+          "file": "crates/aprender-core/tests/contracts/rmsnorm_contract.rs",
+          "grounding": "cited",
+          "line": 55
+        },
+        {
+          "claim": "The #3621 regression input data=[0.0, -0.15964308], α=0.012254778 is explicitly anchored in the committed regression test `regression_3627_scale_invariance_in_the_eps_dominated_regime` and precisely matches the expected y_scaled[1] value of -1.146122 and discrepancy. The test correctly enforces that a mutation restoring the ε=0 assertion turns RED.",
+          "file": "crates/aprender-core/tests/contracts/rmsnorm_contract.rs",
+          "grounding": "cited",
+          "line": 198
+        },
+        {
+          "claim": "Contracts schema (contracts/rmsnorm-kernel-v1.yaml) is correctly updated to carry the ε>0 formal invariant (RN-INV-005) and FALSIFY-RN-002, matching the requested acceptance criteria. The test file header is properly replaced to indicate its hand-maintained status, resolving the false generator header.",
+          "file": "contracts/rmsnorm-kernel-v1.yaml",
+          "grounding": "cited",
+          "line": 53
+        }
+      ],
+      "raw_bytes": 5826,
+      "err_bytes": 100,
+      "envelope_status": "SUCCESS",
+      "verdict_source": "structured_output",
+      "grounding_check": "parity",
+      "model": "gemini-3.1-pro-high",
+      "model_measured": "gemini-3.1-pro-high",
+      "model_source": "measured",
+      "family": "gemini"
+    },
+    {
+      "lane": 2,
+      "status": "SUCCESS",
+      "verdict": "PASS",
+      "summary": "Diff verified against PMAT-3627:\n1. `contracts/rmsnorm-kernel-v1.yaml`: RN-INV-005 formal property updated to the exact ε>0 scale-invariance identity with Lean notes clarifying the ε=0 regime; FALSIFY-RN-002 updated with the new test and regression test. Validated with `pv validate contracts/rmsnorm-kernel-v1.yaml` (0 error(s), 0 warning(s)).\n2. `crates/aprender-core/tests/contracts/rmsnorm_contract.rs`: Updated header honestly documenting hand-maintained contract-bound status after pv probar --binding withdrawal; `prop_scale_invariance` updated to assert the exact ε>0 identity with relative tolerance 1e-4; committed regression test `regression_3627_scale_invariance_in_the_eps_dominated_regime` reproducing the #3621 killing input ([0.0, -0.15964308], α=0.012254778) passes cleanly and turns RED on ε=0 mutation (rel ≈ 0.1895 > 1e-4).\n3. All rmsnorm tests pass (12 passed; 0 failed), and aprender-contracts suite passes (1666 passed; 0 failed).\n4. Roadmap fragment and aggregated roadmap.yaml are valid and idempotent (`make roadmap-aggregate-check` passed).\nNo gates weakened, no unrequested changes found. Diff cannot be refuted.",
+      "findings": [],
+      "raw_bytes": 4516,
+      "err_bytes": 0,
+      "envelope_status": "SUCCESS",
+      "verdict_source": "structured_output",
+      "grounding_check": "parity",
+      "model": "gemini-3.8-flash-high",
+      "model_measured": "gemini-3.8-flash-high",
+      "model_source": "measured",
+      "family": "gemini"
+    },
+    {
+      "lane": 3,
+      "status": "SUCCESS",
+      "verdict": "PASS",
+      "summary": "Diff for PMAT-3627 satisfies all ticket requirements and acceptance criteria without refutations:\n1. Replaces the eps=0 scale invariance theorem with the exact eps>0 invariant in contracts/rmsnorm-kernel-v1.yaml (RN-INV-005 and FALSIFY-RN-002).\n2. Fixes prop_scale_invariance in rmsnorm_contract.rs to assert the eps>0 invariant with relative tolerance 1e-4, removing the fragile arbitrary tolerance branch.\n3. Adds the committed regression test regression_3627_scale_invariance_in_the_eps_dominated_regime anchoring the exact killing input ([0.0, -0.15964308], alpha=0.012254778) from #3621.\n4. Updates file header to accurately reflect hand-maintained contract-bound status.\n5. Registers PMAT-3627 in roadmap fragment and aggregate, passing all roadmap checks.\n6. Mutation to eps=0 form turns the regression test RED as specified. All contract tests pass.",
+      "findings": [
+        {
+          "claim": "The updated scale-invariance proptest (prop_scale_invariance) and the committed regression test (regression_3627_scale_invariance_in_the_eps_dominated_regime) compile and pass across all active tests in contract_tests for rmsnorm.",
+          "command": "cargo test -p aprender-core --test contract_tests rmsnorm -- --nocapture",
+          "file": "crates/aprender-core/tests/contracts/rmsnorm_contract.rs",
+          "grounding": "measured",
+          "line": 55,
+          "output": "test contracts::rmsnorm_contract::falsify_norm_002_rmsnorm_zero_input ... ok\ntest contracts::rmsnorm_contract::falsify_norm_003_rmsnorm_sign_preservation ... ok\ntest contracts::rmsnorm_contract::falsify_norm_001_rmsnorm_unit_rms ... ok\ntest contracts::rmsnorm_contract::prop_simd_matches_scalar_within_ulp ... ignored, SIMD equivalence — trueno domain\ntest contracts::rmsnorm_contract::regression_3627_scale_invariance_in_the_eps_dominated_regime ... ok\ntest contracts::rmsnorm_contract::prop_normalized_rms_approx_1 ... ok\ntest contracts::rmsnorm_contract::prop_output_is_finite ... ok\ntest contracts::rmsnorm_contract::prop_rms_denominator_positive ... ok\ntest contracts::rmsnorm_contract::prop_scale_invariance ... ok\n\ntest result: ok. 12 passed; 0 failed; 1 ignored; 0 measured; 357 filtered out"
+        },
+        {
+          "claim": "The updated contract schema in contracts/rmsnorm-kernel-v1.yaml passes schema and rule validation with 0 errors and 0 warnings under pv validate.",
+          "command": "pv validate contracts/rmsnorm-kernel-v1.yaml",
+          "file": "contracts/rmsnorm-kernel-v1.yaml",
+          "grounding": "measured",
+          "line": 53,
+          "output": "0 error(s), 0 warning(s)\nContract is valid."
+        },
+        {
+          "claim": "The killing input from #3621 (data=[0.0, -0.15964308], alpha=0.012254778) produces an 18.95% (~19%) discrepancy against the eps=0 formula, which is correctly matched by the eps>0 formulation (k=0.810462), and a mutation to the eps=0 form (k=1) yields diff=0.26803625 (rel=0.1895 > 1e-4) which turns the test RED.",
+          "command": "python3 -c 'import numpy as np; data = np.array([0.0, -0.15964308], dtype=np.float32); alpha = np.float32(0.012254778); eps = np.float32(1e-6); m = np.mean(data**2); y = data / np.sqrt(m + eps); y_scaled = (data * alpha) / np.sqrt(np.mean((data * alpha)**2) + eps); k = np.sqrt((m + eps) / (m + eps / (alpha**2))); print(f\"diff_eps0={np.abs(np.sign(alpha)*y - y_scaled)[1]:.8f}, rel={(np.abs(np.sign(alpha)*y - y_scaled)[1]/np.abs(y[1])):.8f}, k={k:.6f}, diff_eps={np.abs(np.sign(alpha)*y*k - y_scaled)[1]:.8f}\")'",
+          "file": "crates/aprender-core/tests/contracts/rmsnorm_contract.rs",
+          "grounding": "measured",
+          "line": 198,
+          "output": "diff_eps0=0.26803625, rel=0.18953773, k=0.810462, diff_eps=0.00000000"
+        },
+        {
+          "claim": "Roadmap entry PMAT-3627 is registered in both fragment and aggregate, and satisfies all four roadmap check gates.",
+          "command": "bash scripts/check_roadmap_fragment_required.sh && bash scripts/check_roadmap_ids_unique.sh && bash scripts/check_roadmap_sorted.sh && bash scripts/check_roadmap_diff_additive.sh",
+          "file": "docs/roadmaps/roadmap.yaml",
+          "grounding": "measured",
+          "line": 18851,
+          "output": "PASS  check_roadmap_fragment_required.sh: 1 changed entry/entries, each with its fragment; the aggregate is regenerated\nPASS  936 ids in /mnt/nvme-raid0/agent-wt/rmsnorm-3627/docs/roadmaps/roadmap.yaml, all unique (nested records included)\nPASS  /mnt/nvme-raid0/agent-wt/rmsnorm-3627/docs/roadmaps/roadmap.yaml: 936 top-level id(s), sorted within each id-prefix, no duplicates, no tracked .bak/.lock\nPASS"
+        },
+        {
+          "claim": "RN-INV-005 and FALSIFY-RN-002 update the formal obligation, prediction, and test mapping to the eps>0 invariant: RMSNorm(alpha*x) = sign(alpha)*RMSNorm(x)*sqrt((m+eps)/(m+eps/alpha^2)).",
+          "file": "contracts/rmsnorm-kernel-v1.yaml",
+          "grounding": "cited",
+          "line": 53
+        }
+      ],
+      "raw_bytes": 15170,
+      "err_bytes": 59,
+      "envelope_status": "SUCCESS",
+      "verdict_source": "structured_output",
+      "grounding_check": "parity",
+      "model": "gemini-3.7-flash-high",
+      "model_measured": "gemini-3.7-flash-high",
+      "model_source": "measured",
+      "family": "gemini"
+    }
+  ],
+  "dissent": [],
+  "dedup": [
+    {
+      "file": "contracts/rmsnorm-kernel-v1.yaml",
+      "line": 53,
+      "lanes_agreeing": [
+        1,
+        3
+      ],
+      "claims": [
+        "Contracts schema (contracts/rmsnorm-kernel-v1.yaml) is correctly updated to carry the ε>0 formal invariant (RN-INV-005) and FALSIFY-RN-002, matching the requested acceptance criteria. The test file header is properly replaced to indicate its hand-maintained status, resolving the false generator header.",
+        "RN-INV-005 and FALSIFY-RN-002 update the formal obligation, prediction, and test mapping to the eps>0 invariant: RMSNorm(alpha*x) = sign(alpha)*RMSNorm(x)*sqrt((m+eps)/(m+eps/alpha^2)).",
+        "The updated contract schema in contracts/rmsnorm-kernel-v1.yaml passes schema and rule validation with 0 errors and 0 warnings under pv validate."
+      ]
+    },
+    {
+      "file": "crates/aprender-core/tests/contracts/rmsnorm_contract.rs",
+      "line": 55,
+      "lanes_agreeing": [
+        1,
+        3
+      ],
+      "claims": [
+        "The updated scale-invariance proptest (prop_scale_invariance) and the committed regression test (regression_3627_scale_invariance_in_the_eps_dominated_regime) compile and pass across all active tests in contract_tests for rmsnorm.",
+        "The updated scale-invariance proptest (prop_scale_invariance) correctly introduces the ε>0 scaling factor √((m + ε) / (m + ε/α²)) which resolves the 19% discrepancy when α²·mean(x²) ≈ ε. Additionally, the test gate is structurally tightened from an absolute tolerance of 0.05 (for small α) to a much stricter 1e-4 relative error."
+      ]
+    },
+    {
+      "file": "crates/aprender-core/tests/contracts/rmsnorm_contract.rs",
+      "line": 198,
+      "lanes_agreeing": [
+        1,
+        3
+      ],
+      "claims": [
+        "The #3621 regression input data=[0.0, -0.15964308], α=0.012254778 is explicitly anchored in the committed regression test `regression_3627_scale_invariance_in_the_eps_dominated_regime` and precisely matches the expected y_scaled[1] value of -1.146122 and discrepancy. The test correctly enforces that a mutation restoring the ε=0 assertion turns RED.",
+        "The killing input from #3621 (data=[0.0, -0.15964308], alpha=0.012254778) produces an 18.95% (~19%) discrepancy against the eps=0 formula, which is correctly matched by the eps>0 formulation (k=0.810462), and a mutation to the eps=0 form (k=1) yields diff=0.26803625 (rel=0.1895 > 1e-4) which turns the test RED."
+      ]
+    },
+    {
+      "file": "docs/roadmaps/roadmap.yaml",
+      "line": 18851,
+      "lanes_agreeing": [
+        3
+      ],
+      "claims": [
+        "Roadmap entry PMAT-3627 is registered in both fragment and aggregate, and satisfies all four roadmap check gates."
+      ]
+    }
+  ],
+  "uncovered": [],
+  "coverage_source": "lanes",
+  "partial": false,
+  "partial_reasons": [],
+  "auto_merge": {
+    "checked": true,
+    "was_armed": false,
+    "disarmed": false,
+    "note": "auto-merge not armed"
+  },
+  "lint": {
+    "ok": true,
+    "output": "receipt complete: kind=artifact lanes=3 author=claude-opus-5/claude"
+  }
+}