A Property Kind Calculus for Measurement Metrology

2.14. Requirement validation — the ForPhysLib benchmark🔗

R21–R25 did not come from introspection; they came from validation, in the systems engineering sense: not "did we build the calculus right" (verification — the traceability matrix below) but "did we specify the right calculus". The instrument is the ForPhysLib benchmark (ForPhysLib/REQUIREMENTS.md, MR1–MR32): thirty-two requirements stated design-neutrally against concrete physics — the same harmonic oscillator typed four honest ways, and a survey of PhysLib's twelve API-map.yaml files — where each MR is scored not only for PKC but for three rival designs and for a shipping library none of them authored. Where an MR restates an R, that is the R validated adversarially: R1 asserts PKC discriminates within a dimension; MR4 hands the same claim a physics problem that plain reals, WithDim, and Buckingham-π tagging attempt first and fail structurally. The benchmark can also fail PKC — it scores MR11 against it — which is what makes its confirmations evidence rather than advertising.

The trace, in both directions:

  • Adversarial restatements — the MR is the R given a physics test case: MR4 ↔ R1; MR5 ↔ R6; MR7 ↔ R19; MR8 ↔ R9; MR13 and MR27 ↔ R10; MR17 ↔ R11; MR18 and MR26 ↔ R20; MR28 ↔ R12; MR20 ↔ R22; MR24 ↔ R23; MR30 and MR31 ↔ R24; MR11 ↔ R21; MR12 ↔ R25.

  • Delegated — the MR is discharged by the layer beneath the kind layer, which the calculus consumes rather than reproves: MR1 → R7 + R4, MR2 → R5 + R7, MR3 → R17 + R16. This is why the benchmark's Tier 1 is the tier PhysLib's own WithDim wins outright, and it is a feature of the layering, not a gap in it.

  • A numbering trap, recorded so it stays harmless: MR15 (exec and spec agree) traces to R10 — the CarrierRefinement bridge and Quantity.add_refines — and not to R15, despite the number. R15 is the strictly sharper claim (adequacy relative to the input uncertainties, not mere rounding-step refinement), and no MR states it yet; it appears in the unvalidated list below.

  • Minted — MRs whose obligations no R stated, now R21–R25: the erasure and operator-table purity of MR11 (R21), the rendering of MR12 (R25), the system-scale dedication of MR20 (R22), the provenance of MR24 (R23), and the audit-scope discipline of MR30/MR31 (R24).

  • Deliberately not minted — MR23 (interface quantities naming both systems they join) and MR25 (genericity over the geometric dimension) have no PKC machinery to annotate yet, and a catalogue row with no possible annotation is exactly the drift the matrix exists to prevent. They are staged in ForPhysLib/PLAN.md and enter the catalogue when their first declaration does.

  • Not yet validated — R13 (scale-spanning units), R14 (the uncertainty ladder), R15 (numerical adequacy), and R18 (coverage intervals) have no MR counterpart. For R13, R14 and R18 the benchmark's physics lacks the phenomena; R15 falls with R14, being defined relative to input uncertainties. That bounds what the benchmark's confirmation is evidence for, and ForPhysLib/PLAN.md stages the case studies that would reach them.

  • Validated late, in both directions — R2 (the specialization lattice) was the near miss: the oscillator's H = T + V is a specialization family the first scoring pass never interrogated. MR32, appended, now does — probes in all four attempts and the scorecard — and validates R2's lattice while exposing what nothing above it consumed: Quantity's addition was same-kind and no quantity-level operation took a Specializes proof, so the licensed sum at the join (T + V landing at the kind both terms provably specialize) was machinery owed — the specialization twin of R9's licensed aggregation. That debt is now paid: SpecializationLift supplies Quantity.widen (the one-way lift along a proved specialization), the sum and the comparison at the join, and the curated KindJoin table through which T + V elaborates — and the MR32 probes flipped from ⚠️ to ✅, leaving MR11 (whose residue kind_algebra has since pushed to the kind equations themselves) as the one requirement the calculus's own benchmark does not let it sweep.