cert
plain-language theorem explainer
Witness packing three elementary domain-cost facts into the A4ExactRS structure for the ISO 440 Hz note. Anyone citing the exact-A4 Recognition Science package uses this certificate. Construction is pure field assignment from three already-proved sibling lemmas (diagonal vanishing, nonnegativity, positive threshold).
Claim. There exists a certificate that (i) the domain cost of any nonzero real against itself is zero, (ii) the domain cost of any pair of positive reals is nonnegative, and (iii) the canonical threshold is strictly positive.
background
The module treats the ISO 16:1975 concert pitch A4 = 440 Hz inside Recognition Science. The informal claim is that 440 Hz sits near a pure phi-ladder rung: $\phi^{17}\cdot 0.123\approx 439.2$ Hz, so the standard is a near-exact RS frequency.
domainCost is the local cost functional on pairs of reals (imported Cost/Constants infrastructure). The structure A4ExactRS packages three elementary properties of that cost: it vanishes on the diagonal away from zero, it is nonnegative on the positive quadrant, and a fixed positive threshold (canonicalThreshold) is available for later comparison arguments.
Upstream, nonnegativity of recognition cost is the standard J-cost fact (cost_nonneg: "The cost of any recognition event is non-negative"), specialized here to the acoustics domain cost.
proof idea
Pure structure inhabitation. The three fields of A4ExactRS are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos respectively. No additional algebra or tactics; the certificate is just the triple of those proofs.
why it matters
Gives a single named witness that the cost side-conditions for the exact-A4 acoustics claim are discharged. The module is marked STRUCTURAL THEOREM (0 sorry, 0 axiom), so this certificate is the packaged form of that status for downstream consumers (e.g. cert_inhabited).
In the broader RS picture the interest is the near-match of 440 Hz to a pure $\phi$-power times a fixed yardstick, tying a metrological standard to the same self-similar fixed point forced at T6. No forcing-chain step (T0–T8) is proved here; the declaration only certifies the cost hygiene needed to talk about that match rigorously.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.