A4ExactRS
plain-language theorem explainer
Packages the three structural axioms for the RS acoustics certificate of concert A (A4 = 440 Hz): domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the A4 exact-RS certificate or its inhabitance proof uses this bundle. It is a pure structure definition; no proof work lives here.
Claim. An exact-RS A4 certificate is a record of three facts: (i) for every nonzero real $r$, the domain cost of the pair $(r,r)$ is zero; (ii) for all positive reals $m,e$, the domain cost of $(m,e)$ is nonnegative; (iii) the canonical threshold is strictly positive.
background
The module treats concert A under ISO 16:1975 (A4 = 440 Hz) inside Recognition Science. The informal RS check is that $440$ sits near a pure $\varphi$-power: $\varphi^{17}\cdot 0.123 \approx 439.2$ Hz, so the standard is a near-ladder hit rather than an exact rung.
Domain cost is the local cost functional on pairs of positive reals used in this acoustics layer; the diagonal identity $\mathrm{cost}(r,r)=0$ is the fixed-point / matched-ratio minimum. Nonnegativity mirrors the global recognition-cost law: upstream, any recognition event has nonnegative cost via $J$-cost nonnegativity at positive state.
The canonical threshold is the positive cutoff against which the A4 match is certified. This structure does not compute 440 Hz; it only names the three inequalities the certificate must carry.
proof idea
No proof body: this is a structure declaration. The three fields are Prop-valued requirements (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is deferred to the sibling cert, which fills the fields by domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives the typed interface for the structural A4 exact-RS claim in the acoustics layer. Downstream, cert builds a concrete inhabitant and cert_inhabited records Nonempty of that type, closing the module's zero-sorry structural theorem status.
In the broader RS picture this is an applied consistency check against the $\varphi$-ladder (T6 self-similar fixed point), not a step of the T0–T8 forcing chain. It ties the ISO pitch standard to the same cost geometry used elsewhere (nonnegative $J$-type cost, matched-ratio zero). It does not derive 440 from first principles; it certifies that the local cost/threshold package is coherent for that standard.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.