cert
plain-language theorem explainer
Packs the three structural properties of the acoustics domain cost for phi-ladder rung spacing into one certificate: diagonal vanishing, non-negativity on positive reals, and a strictly positive canonical threshold. Anyone citing RS Acoustics Certificate 9 uses this bundle as the inhabited witness. The definition is a pure field-assembly of three already-proved sibling lemmas.
Claim. There is an acoustics domain certificate whose cost functional $C$ satisfies $C(r,r)=0$ for every nonzero real $r$, $C(m,e)\ge 0$ whenever $m>0$ and $e>0$, and whose canonical threshold $\tau$ obeys $\tau>0$.
background
Module setting is Acoustics RS Domain Certificate 9: structural facts about phi-ladder rung spacing, where adjacent rungs differ by the golden ratio $\phi\approx 1.618$. Status is a structural theorem (zero sorry, zero axiom).
The certificate structure demands three properties of the local domain cost: it vanishes on the diagonal away from zero, it is nonnegative for positive measurement and expectation arguments, and the canonical threshold is positive. Non-negativity is the domain-level echo of the foundation fact that every recognition-event cost is nonnegative (via the J-cost minimum at identity).
Sibling lemmas already establish each field: diagonal identity of the domain cost, its non-negativity, and positivity of the canonical threshold. This declaration only packages them.
proof idea
One-line structure inhabitant. Each field is filled by the matching sibling lemma: diagonal vanishing by the domain-cost-at-equality lemma, non-negativity by the domain-cost non-negativity lemma, and threshold positivity by the canonical-threshold positivity lemma. No extra rewriting or case analysis.
why it matters
Supplies the inhabited witness for Acoustics Certificate 9 on phi-ladder rung spacing. In the Recognition framework the ladder is forced by T6 ($\phi$ as the self-similar fixed point of the J-cost), and adjacent-rung factor $\phi$ is the discrete spacing used by the mass formula and the eight-tick octave (T7). The certificate records that the acoustics-domain cost inherits the standard J-cost axioms (zero on match, nonnegative, positive threshold), so downstream acoustics arguments can treat rung steps as certified recognition events. No further used-by edges are recorded yet; the object is the terminal bundle for this cert module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.