cert
plain-language theorem explainer
Certificate that the Middle-C frequency recognition structure is inhabited: domain cost vanishes on the diagonal, stays nonnegative for positive arguments, and the canonical threshold is positive. Cited by anyone packaging the RS acoustics match middle C ≈ 261.63 Hz ≈ φ^14 × 0.31 Hz. The body is a structure instance that wires three local lemmas.
Claim. There exists a witness that the domain cost $C$ on positive reals satisfies $C(r,r)=0$ for all $r\neq 0$, $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and the canonical threshold $T$ obeys $T>0$.
background
The module packages the Recognition Science claim that middle C (261.63 Hz) sits on the φ-ladder via φ^14 × 0.31 ≈ 261.3 Hz. Status is structural: zero sorry, zero axioms.
MiddleCFreqRS is the certificate structure for that claim. Its three fields demand: (i) domain cost vanishes when measured equals expected (diagonal identity), (ii) domain cost is nonnegative for positive measured and expected values, and (iii) the canonical threshold is strictly positive. Domain cost is the local specialization of the RS J-cost; upstream, cost_nonneg records that every recognition event has nonnegative cost via Jcost_nonneg at positive state.
Sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos discharge those three obligations pointwise.
proof idea
One-line structure instance. Field cost_at_eq is filled by domainCost_at_eq; cost_nonneg by domainCost_nonneg; threshold_pos by canonicalThreshold_pos. No further tactics or algebraic work.
why it matters
Gives an explicit inhabitant of the Middle-C frequency certificate structure, so downstream acoustics results can assume the cost axioms rather than re-prove them. Sits in the RS acoustics layer that ties audible frequencies to the φ-ladder (primer: φ forced at T6; mass/frequency rungs use φ-powers). The module doc frames the numerical match φ^14 × 0.31 Hz ≈ 261.3 Hz against concert middle C 261.63 Hz as a structural theorem. No used_by edges are recorded yet; the sibling cert_inhabited is the natural consumer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.