HumanVoiceRangeRS
plain-language theorem explainer
Packages the three structural axioms for an RS human-voice-range certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical threshold is positive. Anyone citing the inhabited certificate for the phi^9--phi^12 Hz voice band uses this type. It is a pure structure definition with no proof body.
Claim. A human-voice-range RS certificate is a record of three properties: the domain cost satisfies $C(r,r)=0$ for every $r\neq 0$; $C(m,e)\ge 0$ whenever $m>0$ and $e>0$; and the canonical threshold $\tau$ obeys $\tau>0$.
background
The module treats the human fundamental voice band (classically ~80--300 Hz) as the RS interval from $\varphi^9$ Hz (~76 Hz, bass bottom) through $\varphi^{12}$ Hz (~322 Hz, soprano top). Domain cost is the local cost functional on pairs of positive reals (measure vs expectation, or ratio data) used to score recognition events in this acoustic setting; the canonical threshold is the positive cutoff against which that cost is compared.
Upstream, nonnegativity of recognition cost is already forced in the foundation layer: every recognition event has cost $\ge 0$, via nonnegativity of the J-cost $J(x)=(x+x^{-1})/2-1$ for $x>0$. The present structure specializes that discipline to the voice-range domain cost and records the diagonal-vanishing and threshold-positivity side conditions needed for a certificate.
proof idea
No proof: this is a structure declaration. Its three fields are Prop-valued hypotheses (diagonal vanishing of domain cost, nonnegativity on the positive quadrant, positivity of the canonical threshold). Inhabitation is supplied downstream by wiring the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos into a concrete term.
why it matters
Gives the typed interface that the module's certificate cert inhabits, and thereby makes Nonempty HumanVoiceRangeRS provable. That closes the structural theorem announced in the module doc (0 sorry, 0 axiom) for the claim that the human voice fundamental sits on the phi-ladder window $\varphi^9$--$\varphi^{12}$.
In the broader RS picture this is an acoustics-side application of the same cost calculus forced by the T5 J-uniqueness step and the self-similar fixed point $\varphi$ (T6). It does not itself re-derive those forcing steps; it records the local cost/threshold axioms so downstream acoustic certificates can cite a single inhabited bundle rather than three loose lemmas.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.