cert
plain-language theorem explainer
Packages the three structural facts of the RS harmonic-distortion model into one certificate: domain cost vanishes on the diagonal, is nonnegative for positive arguments, and the canonical THD threshold is positive. Anyone wiring the J-cost audibility bound (about 1.39%) cites this witness. Construction is a pure structure fill from three sibling lemmas.
Claim. There is a harmonic-distortion certificate asserting: (i) for every $r\neq 0$, the domain cost at equal measured and expected values vanishes, $\mathrm{cost}(r,r)=0$; (ii) for all $m,e>0$, $\mathrm{cost}(m,e)\ge 0$; (iii) the canonical THD threshold is strictly positive.
background
The module treats total harmonic distortion (THD) under Recognition Science. Empirically, THD becomes audible near $0.5$–$1%$. The raw J-cost at the golden ratio, $J(\varphi)$, is about $11.8%$, too large. Raising to the spatial factor $D-1$ with $D=3$ gives $J(\varphi)^{2}\approx 1.39%$, matching the audibility band.
Domain cost is the RS cost functional specialized to a measured/expected pair in this acoustics setting; it inherits nonnegativity from the global recognition cost (ObserverForcing: "the cost of any recognition event is non-negative"). The certificate structure simply records diagonal vanishing, nonnegativity, and positivity of the canonical threshold used as the THD cutoff.
proof idea
Pure structure construction. The three fields of HarmonicDistCert are filled by the sibling lemmas domainCost_at_eq (diagonal vanishing), domainCost_nonneg (nonnegativity for positive arguments), and canonicalThreshold_pos (strict positivity of the threshold). No extra algebra or tactics.
why it matters
This is the inhabited structural witness for the RS harmonic-distortion claim in the module doc: THD audibility equals $J(\varphi)^{D-1}=J(\varphi)^{2}\approx 1.39%$, consistent with the $\sim 1%$ experimental band. It sits on the forcing landmarks T5 (J-uniqueness) and T8 ($D=3$), which justify both the cost shape and the exponent $D-1$. No downstream consumers are wired yet; the sibling cert_inhabited is the natural next use. Status is structural (zero sorry, zero axiom): it certifies the cost interface, not a numerical fit to lab data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.