2.16. The requirements at a glance — the traceability matrix
The requirements fall into two kinds of obligation. A verifiable requirement is a truth-apt claim about the calculus — one that is either true or false of it — discharged by a checked theorem: PropertyKindCalculus proves it. An expressiveness requirement is a capability the type system must afford — general-versus-individual (R3), units as chosen values of a kind (R8) — discharged not by a theorem but by a construction that typechecks: that the witnessing declaration elaborates under CI is the demonstration. Conflating the two would make a capability look like an unfinished proof; separating them lets each be reported in its own honest vocabulary.
PropertyKindCalculus proves all 20 verifiable requirements and demonstrates all 8 expressiveness requirements — the capabilities a type system affords by construction rather than by theorem.
The matrix below is generated from the typed @[requirement …] annotations
carried by the Lean declarations (harvested by PropertyKindCalculus.Requirements),
not maintained by hand. It is organized by the requirement groups introduced
above; within each group, every requirement lists the declarations that
specify, prove, implement, or exemplify it, linked to that declaration's
blueprint node. The Status column is likewise derived, not asserted, in the
vocabulary of each requirement's kind: a verifiable requirement reads proved
and shows links to the very theorems that discharge it; an expressiveness
requirement reads demonstrated and links to the constructions that exhibit it;
an undischarged one reads specified (addressed) or unaddressed.
Because every annotation attaches to a real declaration and every status is a function of those annotations and the requirement's kind, the matrix cannot drift from the source — a renamed declaration or a missing proof is a build-time fact, not a stale cell. (This replaces the hand-maintained requirements-at-a-glance table.)
Requirement | Status | Role | This work | Note |
|---|---|---|---|---|
Kind structure |
|
|
|
|
R1 — Kinds are first-class and discriminate within a dimension | specifies | Quantity k R records the kind as a type index | ||
|
| specifies | the kind-indexed value type; distinct kinds are distinct types | |
|
| proves | distinct kinds collapse to one dimension — dim is not injective | |
|
| exemplifies |
| volumetric vs gravimetric water content: two dimension-one kinds, provably distinct |
R2 — Specialization is a lattice, with comparability but not identity |
| specifies |
| widening: the one-way lift of a quantity along a proved specialization, magnitude untouched |
|
| specifies | the reflexive–transitive specialization closure (a preorder) | |
|
| specifies | sub-kinds sharing a super-kind stay mutually comparable | |
|
| specifies | individuation by examination principle, not by name | |
|
| specifies |
| the comparison of comparable kinds, gated by order at the join |
|
| specifies |
| the sum of comparable kinds lands at the join, and only there |
|
| specifies |
| the curated join table: T + V elaborates at the kind both terms provably specialize |
|
| proves |
| widening is functorial on the specialization preorder |
|
| proves | kinds with different examination principles are distinct | |
|
| proves | specialization is transitive | |
|
| proves |
| a registered join is a witnessed comparability fact |
|
| exemplifies |
| kinetic and potential energy: distinct kinds, mutually comparable, and the Hamiltonian lands at the join — the benchmark probe that minted the specialization lift |
|
| exemplifies |
| width and height specialize length, comparable yet distinct by examination principle |
R3 — General versus individual is type versus term |
| specifies | an individual measured value is a term of that type | |
|
| specifies | a kind is a type | |
|
| exemplifies |
|
a specific pencil's width — a term instantiating the kind |
R19 — A quantity characterizes an object; object identity is carried in the type |
| specifies | a quantity that characterizes an object — the object rides in the type, alongside the kind | |
|
| proves |
| the kind-level half: differing sorts ⇒ differing dedicated kinds; within a sort, differing objects ⇒ differing quantity types |
|
| exemplifies |
|
the volumetric water content of a specific soil sample — an |
R22 — A quantity is dedicated to a named component of a named system; dedications of distinct systems are provably distinct, so a part-quantity of one system cannot stand in for a part-quantity of another |
| specifies | the System — Component ; kind dedication triple, the System slot naming the sort | |
|
| proves |
| dedications of distinct sorts are distinct; the particular is the object index's, where cross-system substitution is a type error |
|
| exemplifies |
| same kind, different object: the tagging dilemma resolved by two independent axes rather than a dimension tag |
Operation gating |
|
|
|
|
R4 — Operations are gated by kind (the additive law) | proves | the same-kind additivity laws (comm, assoc, unit), one proof for every lawful carrier | ||
|
| implements |
| same-kind addition; cross-kind addition is a type error |
|
| exemplifies |
| same-kind Int lengths add (3 + 5 = 8); adding a length to a mass is a type error |
R5 — The interaction algebra is a partial, typed, ternary product | specifies | the division dual of the kind product | ||
|
| specifies |
| the curated partial ternary product KMul (Flater App. C) |
|
| proves | multiplication and division are inverse (a × b = c ⇔ c / b = a) | |
|
| exemplifies | torque × angle = energy is sanctioned, though torque and energy share a dimension | |
R6 — Operator availability is gated by scale, monotonically | specifies | the four operator-based scale types, ordered by richness | ||
|
| proves | a richer scale licenses every operation a poorer one does (monotonicity) | |
|
| exemplifies |
| a nominal blood group admits only =/≠; a ratio length admits ×, ÷ |
Soundness bridges |
|
|
|
|
R7 — Dimension certifies coherence; it does not decide legality | specifies | the forgetful functor dim : Kind → Dimension | ||
|
| proves | dim is a homomorphism over the interaction algebra | |
|
| exemplifies |
| torque and energy share the dimension M·L²·T⁻² yet are different kinds |
R8 — Units are chosen values of a kind |
| specifies | a metrological unit is one chosen value of a kind — the referenced kind together with its unit symbol | |
|
| exemplifies |
|
the centimetre — a metrological unit built as a chosen value of the length kind ( |
R16 — Unit references are faithful: commensurability is an equivalence and the number-and-reference form round-trips |
trans, | specifies |
| the number-and-reference form: measuring a numeral against a unit's reference (§13.3.3) |
|
| specifies |
| commensurability — "of the same kind", the only relation a unit converts along |
|
| proves | commensurability is transitive — completing the equivalence a description logic cannot state | |
|
| proves |
| commensurability is symmetric |
|
| proves |
| quantity / unit = number: the numeral reads back off a measured value |
|
| proves |
| commensurability is reflexive |
|
| proves | number × unit = quantity: re-applying the unit to a value's numeral recovers it — the faithful round-trip | |
|
| exemplifies |
| measuring 5 of the centimetre reads back as 5, and re-applying the unit recovers the value — the number-and-reference round-trip |
R17 — Unit conversion between commensurable units is a faithful round-trip (an exact, reciprocal power-of-radix factor — SI decimal or IEC binary) |
| specifies |
| the §1.22 conversion factor of a prefixed unit, read off as an exponent |
|
| specifies | the SI decimal prefix — the §1.22 conversion factor as a power-of-ten exponent | |
|
| specifies | the IEC 80000-13 binary prefix — the same conversion factor at radix two (kibi = 2¹⁰) | |
|
| specifies | a prefixed unit: a unit related to a base by a power-of-radix conversion factor (decimal or binary) | |
|
| specifies |
| the §1.22 conversion factor as a real number, 10 ^ (power-of-ten shift) |
|
| specifies | a unit as a chosen reference quantity of a kind, carrying the nonzero-magnitude license | |
|
| proves |
| over ℝ, converting a magnitude between units and back is the identity (10 ^ shift · 10 ^ (−shift) = 1) |
|
| proves |
| the two conversion factors between commensurable units are reciprocal (their exponents cancel) |
|
| proves | converting a magnitude between units and back recovers it exactly — the faithful round-trip, exact over Int | |
|
| proves |
| the two conversion factors between two units of a kind are reciprocal, for an arbitrary chosen reference |
|
| proves |
| measuring and re-applying a real-valued unit is a bijection — the §13.3.3 number-and-reference round-trip over ℝ |
|
| exemplifies |
| over ℝ at radix 2, a KiB magnitude converted to MiB and back returns exactly — the same theorem |
|
| exemplifies |
| over ℝ, a cm magnitude converted to km and back returns exactly (×10⁵ then ×10⁻⁵) |
|
| exemplifies |
| KiB → MiB → KiB recovers exactly at radix two — the same convertExp_roundtrip, no new proof |
|
| exemplifies |
| cm → km → cm recovers any magnitude's decimal exponent exactly (the km/cm factor is 10⁵, its reciprocal 10⁻⁵) |
Aggregation |
|
|
|
|
R9 — Extensive quantities aggregate additively over parts; intensive ones do not |
extensive_additive, mixing_subadditive, leafSum_invariant, | specifies |
| a count kind — how many atomic parts fall under a sortal predicate |
|
| specifies | a re-carving of a whole, carrying the obligation that the whole is preserved | |
|
| specifies | extensive kinds aggregate additively over a decomposition | |
|
| specifies | intensive kinds are constant under composition, on parts that agree | |
|
| specifies | whole-proper kinds — the whole's value produced by no aggregation | |
|
| specifies | extensivity relative to a shared parameter — an axis, an origin, a datum | |
|
| specifies |
| the transport law relating two parameters, with the correction as data |
|
| specifies | the weighted carving with its kinds on: the weight kind's additivity is a field, so a carving of a kind that does not sum cannot be built | |
|
| specifies | a weighted carving: parts, weights, and the nonzero-total license a mean needs, at any carrier | |
|
| specifies |
| the weighted mean — the centre-of-mass mode, the one aggregation that divides |
|
| specifies |
| the kinded weighted mean — the product and quotient licenses say the three kinds are related the way a mean needs |
|
| specifies | additivity to within a named per-join tolerance — §13.5.2, the branch of Bunge's four that is about measurement rather than mereology | |
|
| proves | the ∀-quantified additive law lifts to the whole decomposition | |
|
| proves | volume on mixing is sub-additive — a checked non-extensive counterexample | |
|
| proves | every licensed aggregate is re-carving invariant, however many parts the map leaves | |
|
| proves |
| parts read about their own parameters aggregate to the whole once each is transported |
|
| proves | a count is extensive over a fixed carving, and yet not a property of the whole | |
|
| proves | assembling a whole-proper kind reports the wrong number on an exhibited carving | |
|
| proves | a uniform carving reads its parts' common value, to arbitrary depth | |
|
| proves | the mean of a constant is that constant — the law that distinguishes a mean from a sum, at the carrier whose cancellation can prove it | |
|
| proves |
| the run-time constructor refuses exactly the carvings whose total weight is the carrier's zero |
|
| proves | an intensive kind is not extensive wherever a reading is nonzero | |
|
| proves |
| summing readings taken about different parameters is wrong by exactly the corrections |
|
| proves | the kinded mean erases to the carrier mean, so every numerical theorem about magnitudes applies to it unchanged | |
|
| proves | the discrepancy over a whole carving is at most the join count times the tolerance | |
|
| proves | the parallel-axis theorem: a moment of inertia transports between axes by a correction built from the carving's own first moment and total mass | |
|
| proves |
| a tolerance below the contraction is refuted: volume on mixing is not quasiextensive under 4 mL |
|
| proves | §13.5.1 is §13.5.2 at zero tolerance, in both directions | |
|
| implements | the license established at run time rather than assumed: a carving with no weight is refused | |
|
| exemplifies |
| mass is extensive: a three-sample rock assembly (3+5+7) reads 15 over its parts |
Representation parametricity |
|
|
|
|
R10 — A quantity value is parametric in its numeric representation type | add_refines, mul_refines, div_refines, mean_div_refines, refinementFixes_iff_exactRepresentable | specifies | the bridge's division law, unconditional only because the spec carrier totalizes x / 0 | |
|
| specifies | the numeric-representation typeclass bounding the carrier | |
|
| specifies |
| the lawful carrier over which additivity is proved once |
|
| specifies | the bridge's multiplicative law — the same forgetful map and rounding, for the product | |
|
| specifies | the exec/spec carrier refinement bridge | |
|
| specifies |
| flag-freedom said with the refinement's own rounding rather than the format's |
|
| proves | a law over the spec carrier descends to the exec carrier as one rounding step | |
|
| proves | the bridge crosses a licensed kind product: the exec product is the rounded spec product, at the product kind | |
|
| proves | and a licensed kind quotient — the rung a ratio, a conversion factor, or a weighted mean's denominator rides | |
|
| proves | the quotient bridge read at a model-level site: the mean's own division node | |
|
| proves | the refinement's rounding is the format's, so the exactness half of the adequacy capstone is a CarrierRefinement statement | |
|
| exemplifies |
|
the same Quantity layer runs at |
R11 — Units are scalar; a vector quantity is a numerical array times one scalar unit | proves | the additivity laws transfer to the vector carrier by the same parametric proof | ||
|
| implements |
| a function-space carrier: a vector quantity is a numerical array under one scalar unit |
|
| exemplifies |
| the licensed operation is a scalar quantity acting on a vector one (2 · east = 6 on the first axis); a pointwise product of two displacements does not typecheck, because the unit is scalar |
|
| exemplifies |
| a three-axis displacement is one kind over an indexed carrier, and additivity transfers to it with no vector-specific proof |
R20 — A vector quantity's numbers are coefficients in a chosen basis, so a reading is indexed by that basis and by the law its coefficients obey when the basis changes; readings in different bases do not combine, the change acts functorially, and a contraction of two readings is basis-independent while each coefficient separately is not |
| specifies |
| components read in a named frame at a stated variance |
|
| specifies |
| a coordinate frame: the choice components are read relative to |
|
| specifies |
| the transformation law a quantity's components obey (scalar / vector / rank-2) |
|
| specifies |
| a change of frame, and orthonormality as a hypothesis on it rather than a field of it |
|
| specifies |
| the scalar gate: which carriers' × is the multiplication of magnitudes, so a numerical-array carrier cannot sign a pointwise product as a product of kinds |
|
| proves |
| a change of frame is an action: composing two changes is the composite change |
|
| proves |
| a change of frame is an action: the identity change acts as the identity |
|
| proves |
| the scalar product is invariant under an orthonormal change of frame — the sense in which a change of representation does not change the physics |
|
| proves |
| and a component is not invariant — stated with a witness, so the previous result cannot be over-read |
|
| exemplifies |
| and a component of the same quantity does move between the two frames — one quantity, two frames, not two quantities |
|
| exemplifies |
|
the kinetic-energy contraction |
Classification |
|
|
|
|
R12 — A classification is a certificate, not an assertion |
| specifies | the by-construction product certificate | |
|
| specifies | the product kind-law family | |
|
| specifies | the quotient kind-law family | |
|
| specifies | the reciprocal kind-law family | |
|
| proves |
| the smart-constructed product satisfies its certificate by construction |
|
| exemplifies |
|
a length built through the kind-law, classified |
|
| exemplifies |
|
the kind-law |
R13 — Unit classification needs a third category: scale-spanning units |
| specifies |
| the licensed energetic combination: incoherent sources add in power, role-independently — forbidding + costs no expressiveness |
|
| specifies |
| a level kind: the logarithmic presentation of a ratio root kind against a named reference — reference and power-role are kind identity (dBm ≠ dBW) |
|
| specifies |
| ISO 80000-1's power / root-power dichotomy, as kind data fixing the level factor (10 vs 20) |
|
| specifies |
| a level is ordinal as a kind: its only same-kind operation is order; its differences are heterogeneous |
|
| specifies | the three-way unit classification (base / derived / scale-spanning) | |
|
| specifies | a scale-spanning unit: dimensionally dependent, retained via a coefficient | |
|
| specifies |
| the torsor pair: level − level = gain, level + gain = level — the whole additive vocabulary of a level |
|
| specifies | the mechanical-reducibility criterion the dimension layer can detect | |
|
| proves |
| the certified addition is unprovable at a level kind — L₁ + L₂ is a type error, not a lint |
|
| proves |
| the reference cancels in differences: the gain kind is reference-independent, by rfl |
|
| proves | scale-spanning is not a function of dimension alone | |
|
| exemplifies | the ampere is a genuine physical base — not scale-spanning — the contrast unit | |
|
| exemplifies | the kelvin's scale-spanning character is invisible to the dimension layer (Θ kept independent) | |
Uncertainty and numerical adequacy |
|
|
|
|
R14 — Output uncertainty is computed by a provably nested ladder of methods |
willinkCumulants_cons, gum_eq_willink_of_normal, | specifies |
| the (κ₂, κ₄) cumulant combine-monoid the ladder rests on |
|
| proves | T1 — independent contributions add: the cumulant-additivity law | |
|
| proves | the ladder nests: GUM is the faithful κ₄ = 0 restriction of Willink | |
|
| proves |
| T2 — the Willink combine's second cumulant is exactly the GUM variance |
|
| implements | GUM linearized combined standard uncertainty √(Σ cᵢ² uᵢ²) | |
|
| implements | Willink cumulant combine → (u_Y, γ_Y) | |
|
| exemplifies |
| two Gaussian inputs (κ₄ = 0, c = 3, 4) where the GUM and Willink combines agree |
R15 — A floating-point representation is numerically adequate iff it loses no information at the scale of the input uncertainties |
mean_fp32_within_errBound, | specifies |
| a weighted mean compiled into the evaluation DAG whose rounding the adequacy layer bounds |
|
| specifies |
| forgetting a binary32 carving to the real carving it specifies, taking the specification's own license as an argument |
|
| specifies |
| the accumulated adequacy report (swamping + cancellation site counts) |
|
| specifies |
| flag-freedom as a condition on the exact real evaluation: every node's exact value is a binary32 number |
|
| proves | the binary32 weighted mean is within the DAG's accumulated rounding budget of the exact real mean | |
|
| proves |
| the mean's regularity is two conditions, one per rung — the rounded total and the exact total |
|
| proves | the absorption flag is sound and complete: flag ⇔ the contribution is lost | |
|
| proves |
| the adequacy capstone's exact case in the bridge's vocabulary: forgetting the executable evaluation is the exact evaluation |
|
| proves |
| at a cancellation site the relative uncertainty reaches ≥ 100% |
|
| proves |
| rounding fixes exactly the representable reals — what makes the checkable condition minimal |
|
| proves | the checkable condition and the floating-point one cut out the same inputs | |
|
| implements | the executable numerical-adequacy carrier over Float | |
|
| exemplifies |
| a 1-perturbation of grid value 80 (ulp 8) is absorbed: fl(80 + 1) = 80 |
|
| exemplifies |
| the absorption verdict is exactly right on a concrete value (A3) |
|
| exemplifies |
| near-equal subtraction is Sterbenz-exact yet amplifies relative uncertainty to 100% |
|
| exemplifies |
| a doubling chain is flag-free at both all-ones and all-zeros inputs, so the box equality holds with nothing assumed |
R18 — The recorded variance certifies a coverage interval: distribution-free (Chebyshev ≥ 1 − 1/k²), exact for bounded families |
| specifies | the standard uncertainty u = √variance the coverage interval is measured in | |
|
| proves |
| the per-join tolerance as a coverage statement: |D| < k·u holds with probability ≥ 1 − 1/k², distribution-free |
|
| proves |
| Tier 1 (half-width): coverage of the interval of half-width c is ≥ 1 − variance/c² (Chebyshev) |
|
| proves | Tier 1 (coverage factor): the k-standard-uncertainty interval has coverage ≥ 1 − 1/k², distribution-free | |
|
| proves | Tier 2 (uniform): the centred interval [m−h, m+h] of a uniform on [m−δ, m+δ] has coverage exactly h/δ | |
|
| exemplifies |
| the central half [-1,1] of a uniform on [-2,2] has coverage exactly 1/2 |
Ergonomics and erasure |
|
|
|
|
R21 — The kind layer erases: the kinded authoring computes exactly the bare-carrier value, and the operator-table form elaborates to the same term as the longhand form — the ceremony is pure |
| specifies |
| the curated division table |
|
| specifies |
the curated multiplication table: kind-directed | |
|
| proves |
| the operator form is definitionally the longhand form — one rfl transports every certificate |
|
| proves |
| the division twin of the same erasure |
|
| exemplifies |
|
the OperatorTable form |
|
| exemplifies |
| the most verbose authoring (PKC longhand) computes exactly the least verbose one (bare reals), at the potential-energy model |
R25 — A kinded definition renders back as typeset mathematics from its own elaborated source, with the kind bookkeeping suppressed |
| specifies |
| the presentation term language the elaborated definition is lifted into |
|
| implements |
| the harvest of every @[pkc_math]-rendered declaration, for the index page |
|
| implements |
| precedence-aware pretty-printing of a lifted definition to a LaTeX equation |
|
| exemplifies |
|
the AVS backscatter model rendered to |
Provenance and audit |
|
|
|
|
R23 — A value's provenance is recordable and auditable: a kind-typed value-flow graph with a declared boundary contract, checked against what the scope actually computes |
| specifies | the declared boundary an author claims for a scope | |
|
| specifies |
| the kind-typed value-flow graph: ports, evidence-tiered intros, hyperedge occurrences, exits |
|
| implements | well-formedness of the recorded graph, decidably | |
|
| implements |
| whether one contract discharges another — the claim checked against what the scope computes |
|
| exemplifies |
| the WCM forward's declared boundary — three uncertain inputs, four expert-carried calibration params — pinned to agree with what the scope computes, the calibration rendered as unbudgeted sources by the port budget |
R24 — An audit is a claim about its scope, never about the library: the unkinded surface of a scope is enumerable, and a blessed scope only grows |
| specifies |
| the boundary tier vocabulary — including the interface tier that keeps an audit honest about its scope |
|
| implements |
| the per-scope kind ledger the ratchet compares against |
|
| implements |
| enumeration of the unkinded boundary sites of a scope |
|
| exemplifies |
| the same directory's ingest boundary, measured rather than gated — 72 unkinded positions enumerated so growth is visible — while the silent mint ratchet lets the blessed scope grow only by attestation |
|
| exemplifies |
| the kinded interior of a whole PhysLib directory, gated unkinded-empty: a naked binder added to the scope is a build failure |
R26 — A module's behavior is a checked measurement model: a declared boundary carries relation edges whose witnesses are kernel-checked theorems, every relation kind has a conclusion-shape check, a bound names a kinded tolerance, and every rung beyond the witness's own is answered for by a named repair or restatement |
| specifies | one rung of an edge's license clause — a claim beyond the witness's own rung is answered for by a named repair or restatement, because side conditions do not transfer | |
|
| specifies | the theorem edge between two declared boundaries: what is claimed, the witness, the kinded tolerance, the named side conditions, the per-rung licenses | |
|
| implements |
| the full check of one edge: witness a sorry-free theorem, conclusion in the claimed shape per relation kind, tolerance a Quantity at an output port's kind, hypotheses mentioned, licenses answered for, both boundaries named |
|
| implements |
| the decider clause's hygiene: a named case-decider governs a conditional port and exists |
|
| exemplifies |
| the WCM theorem edge: the closed-form retrieval inverts the forward at ℝ, its side condition named (soilGainNonzero) and its license list honestly empty — nothing claimed beyond the witness's rung |
R27 — A module's distribution is licensed by declared extensivity: output ports carry aggregation classes, and recarving or sharding a batch axis is licensed by theorem from those declarations, with the quasi-extensive tolerance tied to the rounding budget where the carrier demands it | specifies | the aggregation class of a produced port — the declared mereology of a boundary, in the §13.5 vocabulary the mereology layer proves laws over | ||
|
| proves | the distribution license: one re-carving of the batch axis preserves every declared-extensive output's total — the quantified boundary-level form of leafSum_invariant | |
|
| implements |
| the aggregation clause's hygiene: a class governs a produced port; a named tolerance is a Quantity at that port's kind; a named condition, sortal, transport, or cancellation law exists |
R28 — A module's requirements are stated with their evidence: every produced port of a model boundary is governed by a requirement or exempted with a reason; a provable requirement's witness is a sorry-free theorem or theorem edge naming no referent, with spot checks evaluated where the model runs; an empirical requirement names marked referents and a gate mentioning one; and an attestation never stands beside a discharge |
| specifies | the objects a requirement quantifies over — every object the boundary is evaluated for, a sort, named sorted objects, or a decider's selection | |
|
| specifies | a requirement on a declared boundary: the statement in the author's words, the governed model boundary and port, the scope, and the evidence — witness and spot checks, a claimed absence, referents and gate — or the attestation that defers it | |
|
| specifies | the two categories, told apart by the statement's constants: a provable requirement's witness names no referent, an empirical requirement's gate names one | |
|
| specifies | which side of a requirement a declared boundary stands on: a model boundary is governed; a specification boundary is checked against and is the subject of no requirement | |
|
| implements |
| the full check of one requirement: the governed boundary a model's, the port one it declares, the scope a sort, sorted objects or a decider, the witness sorry-free and naming no referent, a claimed absence absent, the referents marked and the gate naming one, every spot check true, an attestation never beside a discharge |
|
| implements |
| the coverage census: every produced port of every model boundary in scope governed, exempted with a reason, or UNGOVERNED, with the category tallies and the attested count |
|
| exemplifies |
| HE5 — an empirical requirement over every spring of a sort, attested until the datasheet band is declared as referents |
|
| exemplifies |
|
HP1 — a provable requirement on the oscillator's static compliance, discharged by a |
|
| exemplifies |
| HP6 — a negative provable requirement, discharged by the absence of the license that would assemble angular frequency over the pair |