cert_inhabited
plain-language theorem explainer
The certificate structure for exact A4 (440 Hz) in Recognition Science is inhabited: there exists at least one witness packing the domain-cost identities and positive threshold. Acoustics or RS-constants workers cite it to discharge Nonempty obligations. The proof is a one-constructor term that feeds the prebuilt certificate into Nonempty.
Claim. The type of exact-A4 Recognition Science certificates is nonempty: there exists a record whose domain cost vanishes on the diagonal ($C(r,r)=0$ for $r\neq 0$), is nonnegative for positive arguments, and whose canonical threshold is strictly positive.
background
The module treats the ISO 16:1975 concert pitch A4 = 440 Hz as an RS structural claim. The informal link is that $440$ sits near $\varphi^{17}\cdot 0.123\approx 439.2$, so the standard is a rounded phi-ladder rung rather than an independent acoustic constant.
Domain cost is the local cost functional on pairs of real amplitudes (imported from the Cost layer); the certificate demands it be zero on equal nonzero arguments and nonnegative when both arguments are positive. The canonical threshold is a positive real cutoff used to separate exact match from near-miss on that cost.
A4ExactRS is the structure bundling those three properties. The sibling cert is a concrete inhabitant already assembled in-module; this theorem only records that the type is nonempty.
proof idea
One-line term proof. Lean’s Nonempty is witnessed by a single constructor; the proof supplies the existing in-module certificate cert as that witness. No tactics, no further lemmas, no unfolding of the cost identities.
why it matters
Closes the structural side of the A4 exact-RS module: status is proved with zero sorry and zero axioms. Downstream pages can assume an A4 certificate exists without rebuilding the cost and threshold facts. In the broader RS picture this is an acoustics-domain sanity check that a named SI frequency sits on (or at a controlled defect from) the phi ladder, consistent with the same J-cost and self-similar fixed point $\varphi$ forced in the T5–T6 segment of the unified forcing chain. No parent theorems currently depend on it; it is a leaf certificate of inhabitance.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.