From ef62a40a9aa152e2603aa343f40469876e1de06c Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 20 Sep 2026 23:36:42 +0200 Subject: [PATCH 1/4] PMAT-3627 step 1 (RED): the input that killed #3621, as a committed regression case RED FIRST. Only the regression test lands; the proptest, the contract and the header are untouched. On THIS commit: test regression_3627_scale_invariance_in_the_eps_dominated_regime ... FAILED 3627 regression: sign*y[1]=-1.414158 vs y_scaled[1]=-1.1461217, diff=0.26803625 Input: data = [0.0, -0.15964308], alpha = 0.012254778. alpha^2 * mean(x^2) = 1.91e-6, eps = 1e-6 (RMSNorm::without_affine, group_norm.rs:275). Ratio 1.91: the eps term is not negligible and RMSNorm(alpha*x) != sign(alpha)*RMSNorm(x), by design of eps. The numbers were re-derived in f64 independently of the CI log and match to six digits; the eps>0 identity y_scaled = sign(a)*y*sqrt((m+eps)/(m+eps/a^2)) predicts -1.146122 with relative error 2e-16. The implementation is right; the assertion was wrong. Refs #3627, #3621 Pmat-Ticket: PMAT-3627 Co-Authored-By: Claude Opus 5 (1M context) --- .../tests/contracts/rmsnorm_contract.rs | 34 +++++++++++++++++++ 1 file changed, 34 insertions(+) diff --git a/crates/aprender-core/tests/contracts/rmsnorm_contract.rs b/crates/aprender-core/tests/contracts/rmsnorm_contract.rs index 7efae34bfe..3ace5baddf 100644 --- a/crates/aprender-core/tests/contracts/rmsnorm_contract.rs +++ b/crates/aprender-core/tests/contracts/rmsnorm_contract.rs @@ -167,3 +167,37 @@ 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 = 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 sign = alpha.signum(); + for i in 0..n { + let expected = sign * y.data()[i]; + let diff = (expected - y_scaled.data()[i]).abs(); + let tol = if alpha.abs() < 0.1 { 0.05 } else { 1e-3 }; + assert!( + diff < tol, + "3627 regression: sign*y[{i}]={expected} vs y_scaled[{i}]={}, diff={diff} (ε=0 assertion)", + y_scaled.data()[i] + ); + } +} From dad51cb93c3c22cffedb162c52743db51e4e90c1 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Sun, 20 Sep 2026 23:46:21 +0200 Subject: [PATCH 2/4] PMAT-3627 step 2 (GREEN): assert the eps>0 scale-invariance property, not the eps=0 theorem Same regression case as the RED commit, now green, plus the proptest, the contract and the file's header. THE PROPERTY. With eps in the denominator, RMSNorm(a*x) = sign(a) * RMSNorm(x) * sqrt((m+eps) / (m+eps/a^2)), m = mean(x^2), exactly (re-derived in f64: relative error 2e-16 on the killing input). The eps=0 theorem RMSNorm.rms_scale_zero_eps is the k -> 1 limit and is false whenever a^2*m is comparable to eps. The proptest and the regression case now assert the eps>0 form with a relative tolerance of 1e-4 -- testing what the implementation computes, in every regime the generator reaches -- and the guessed `tol = 0.05 if |alpha| < 0.1` branch is gone. Option 1 from the issue, chosen over the precondition: it is the stronger property and excludes nothing. regression_3627_... ok prop_scale_invariance x 20 runs, fresh seed each 20/20 ok MUTATION (k := 1, the eps=0 form restored) RED: rel=0.18953769 -- the 19% the whole rmsnorm suite 12 passed, 0 failed The regression case also pins y_scaled[1] = -1.146122 and k = 0.810462, so it is anchored to the incident's numbers, not only to the identity. THE CONTRACT. RN-INV-005's formal now states the eps>0 property (carries Sigma symbols: forall, ne, sqrt, arrows), and its Lean notes say precisely which regime the eps=0 theorem covers. FALSIFY-RN-002 names both tests and the mutation. pv validate clean; cargo test -p aprender-contracts --lib 1666/1666 (sigma armed). The edit adds no file and no triple, so census/graph/README are unchanged -- checked by regenerating. THE HEADER. This file said "DO NOT EDIT -- regenerate with `pv probar --binding`". That is false: 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 (20dda945b, 2026-02-18). Obeying the header would have replaced five real property tests with seven ignored stubs. This is a declared HAND EDIT, and the header now says so; the issue's "regenerated, no hand edit" item was withdrawn on that measurement. The same false header stands on ~50 other tests/contracts/ files: #3630. RETRIES ARE THEATER FOR PROPERTY TESTS. nextest [profile.ci] retries = 2 replayed the case proptest persisted to proptest-regressions/ on TRY 1, so TRY 2 and 3 failed in 0.005 s each: three tries, one failure. A retry cannot un-persist a counterexample. Refs #3627, #3621, #3630 Pmat-Ticket: PMAT-3627 Co-Authored-By: Claude Opus 5 (1M context) --- contracts/rmsnorm-kernel-v1.yaml | 11 ++-- .../tests/contracts/rmsnorm_contract.rs | 54 ++++++++++++++----- 2 files changed, 46 insertions(+), 19 deletions(-) diff --git a/contracts/rmsnorm-kernel-v1.yaml b/contracts/rmsnorm-kernel-v1.yaml index 3d30928605..a709b49f19 100644 --- a/contracts/rmsnorm-kernel-v1.yaml +++ b/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' diff --git a/crates/aprender-core/tests/contracts/rmsnorm_contract.rs b/crates/aprender-core/tests/contracts/rmsnorm_contract.rs index 3ace5baddf..3f6ccefad8 100644 --- a/crates/aprender-core/tests/contracts/rmsnorm_contract.rs +++ b/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::() / 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] ); } @@ -189,15 +205,25 @@ fn regression_3627_scale_invariance_in_the_eps_dominated_regime() { 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::() / 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]; - let diff = (expected - y_scaled.data()[i]).abs(); - let tol = if alpha.abs() < 0.1 { 0.05 } else { 1e-3 }; + let expected = sign * y.data()[i] * k; + let denom = expected.abs().max(1e-3); + let rel = (expected - y_scaled.data()[i]).abs() / denom; assert!( - diff < tol, - "3627 regression: sign*y[{i}]={expected} vs y_scaled[{i}]={}, diff={diff} (ε=0 assertion)", + 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}"); } From fd068099fd8ad3a31c802c18ee1655944dfad49e Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 21 Sep 2026 00:42:41 +0200 Subject: [PATCH 3/4] PMAT-3627: register the ticket (fragment + aggregate) so the AD-04 quorum can run docs/roadmaps/entries/PMAT-3627.yaml hand-entered from issue #3627 (title, done_when as notes), roadmap.yaml regenerated by make roadmap-aggregate. quorum-review.sh refuses unless `pmat work status PMAT-3627` resolves, and the item existed only as a GitHub issue. Four roadmap guards rc=0. No renumbering, no separate PR. Pmat-Ticket: PMAT-3627 Co-Authored-By: Claude Opus 5 (1M context) --- docs/roadmaps/entries/PMAT-3627.yaml | 17 +++++++++++++++++ docs/roadmaps/roadmap.yaml | 17 +++++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 docs/roadmaps/entries/PMAT-3627.yaml diff --git a/docs/roadmaps/entries/PMAT-3627.yaml b/docs/roadmaps/entries/PMAT-3627.yaml new file mode 100644 index 0000000000..0c8bb6aa53 --- /dev/null +++ b/docs/roadmaps/entries/PMAT-3627.yaml @@ -0,0 +1,17 @@ +- id: PMAT-3627 + github_issue: 3627 + item_type: task + title: 'rmsnorm_contract::prop_scale_invariance asserts the ε=0 theorem against the ε=1e-6 implementation — fails whenever α²·mean(x²) ≈ ε (killed #3621 shard 1/3)' + status: planned + priority: critical + assigned_to: null + created: 2026-09-20T21:27:27Z + updated: 2026-09-20T21:27:27Z + spec: null + acceptance_criteria: [] + phases: [] + subtasks: [] + estimated_effort: null + labels: + - kind:code + notes: 'ACCEPTANCE (hand-entered from issue #3627 done_when; minted on the PR branch so the AD-04 quorum can run -- pmat work status refuses a missing item). 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: #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 #3621), and a mutation that restores the ε=0 assertion turns it RED cargo' diff --git a/docs/roadmaps/roadmap.yaml b/docs/roadmaps/roadmap.yaml index 3a90bd6297..6f580635c5 100644 --- a/docs/roadmaps/roadmap.yaml +++ b/docs/roadmaps/roadmap.yaml @@ -18848,3 +18848,20 @@ roadmap: labels: - kind:code notes: 'ACCEPTANCE (hand-entered; pmat work add derived neither spec: nor acceptance_criteria: — defect paiml-mcp-agent-toolkit#1414). Spec: docs/specifications/ruling-receipts-under-contract.md (operator ruling 2026-09-20). Done when: contracts/parity-receipt-v1.yaml with its shape on origin/main; extract:parity-receipt implemented; pv lint --gate shapes --path evidence/ in the required check; PR body shows 7 older receipts RED before back-fill and 0 after, plant violation = 1, mutation RED, pc_shape fired; check_parity_receipt.sh folded into the shape or its remainder listed under not_expressible; ONT-4c3 bound with the parity receipt as focus node; verdict rendered on a fleet host once the pv pin lands, else checkout-only: true. Sigma parent bound: json. Back-fill denominator: 7. STOP: subset-insufficient; shared-file-touched without the guard label; any threshold typed into the shape instead of resolved from thresholds.yaml.' +- id: PMAT-3627 + github_issue: 3627 + item_type: task + title: 'rmsnorm_contract::prop_scale_invariance asserts the ε=0 theorem against the ε=1e-6 implementation — fails whenever α²·mean(x²) ≈ ε (killed #3621 shard 1/3)' + status: planned + priority: critical + assigned_to: null + created: 2026-09-20T21:27:27Z + updated: 2026-09-20T21:27:27Z + spec: null + acceptance_criteria: [] + phases: [] + subtasks: [] + estimated_effort: null + labels: + - kind:code + notes: 'ACCEPTANCE (hand-entered from issue #3627 done_when; minted on the PR branch so the AD-04 quorum can run -- pmat work status refuses a missing item). 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: #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 #3621), and a mutation that restores the ε=0 assertion turns it RED cargo' From 30493c1e2cc841ee2e3a1245984062319253a3a3 Mon Sep 17 00:00:00 2001 From: Noah Gift Date: Mon, 21 Sep 2026 00:49:41 +0200 Subject: [PATCH 4/4] =?UTF-8?q?PMAT-3627:=20AD-04=20quorum=20receipt=20?= =?UTF-8?q?=E2=80=94=203/3=20PASS,=20three=20independent=20lanes?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit docs/audits/quorum-PMAT-3627.json from quorum-review.sh --base origin/main --pr 3631, executor agy, width 3, models gemini-3.1-pro-high / gemini-3.8-flash-high / gemini-3.7-flash-high, none in the author's family. Independence inspected: every lane file has zero references to a sibling lane, $WORK or the .lanes/ dir. Dissent: none. Pmat-Ticket: PMAT-3627 Co-Authored-By: Claude Opus 5 (1M context) --- docs/audits/quorum-PMAT-3627.json | 190 ++++++++++++++++++++++++++++++ 1 file changed, 190 insertions(+) create mode 100644 docs/audits/quorum-PMAT-3627.json diff --git a/docs/audits/quorum-PMAT-3627.json b/docs/audits/quorum-PMAT-3627.json new file mode 100644 index 0000000000..e134fbbe49 --- /dev/null +++ b/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" + } +}