cert
plain-language theorem explainer
Packages three domain-cost facts (vanishes on the equal-ratio diagonal, is nonnegative for positive arguments, and the canonical threshold is positive) into one SoundSpeedCert instance. Anyone working the φ-derived transverse/longitudinal sound-speed ratio cites this bundle. Construction is a pure structure instance wiring three already-proved sibling lemmas.
Claim. There is a certificate asserting: (i) the domain cost of equal positive ratios vanishes, $\mathrm{domainCost}(r,r)=0$ for all $r\neq 0$; (ii) $\mathrm{domainCost}(m,e)\ge 0$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module derives the isotropic-solid ratio $v_T/v_L=\sqrt{(1-2\nu)/(2-2\nu)}$ under the RS choice $\nu=1/\varphi^2\approx 0.382$, which yields $v_T/v_L\approx 0.437\approx\varphi^{-2.7}$. Empirically metals sit near $0.5$–$0.6$. Status is structural: zero sorry, zero axiom.
SoundSpeedCert is the local certificate structure. Its three fields demand that the module's domain cost vanish on the equal-ratio diagonal, stay nonnegative for positive mass/energy arguments, and that the canonical threshold be positive. Upstream, cost_nonneg from ObserverForcing records that every recognition-event cost is nonnegative via $J$-cost nonnegativity; the present fields are the domain-cost analogues used here.
proof idea
Pure structure instance. The three fields are filled by the sibling lemmas domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos respectively. No extra tactics or algebraic work; the def is the certificate object itself.
why it matters
Gives a single named inhabitant of the sound-speed certificate so downstream physics lemmas can assume the three cost axioms by projecting fields rather than re-proving them. The module frames this as part of the structural theorem linking Poisson ratio $\nu=1/\varphi^2$ to $v_T/v_L$ on the $\varphi$-ladder (T6 fixed point). No used_by edges are recorded yet; the sibling cert_inhabited is the natural next consumer. Does not itself compute the numerical ratio or force $\nu$.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.