SoundSpeedCert
plain-language theorem explainer
Certificate structure bundling three analytic properties of the domain cost used for the φ-derived transverse/longitudinal sound-speed ratio: diagonal vanishing, nonnegativity for positive arguments, and positivity of the canonical threshold. Downstream code builds a concrete inhabited instance from sibling lemmas. Pure structure definition; no proof body.
Claim. A sound-speed certificate is a triple of properties: (i) the domain cost vanishes on the diagonal, $\mathrm{cost}(r,r)=0$ for every nonzero real $r$; (ii) the domain cost is nonnegative for positive arguments, $0\le\mathrm{cost}(m,e)$ whenever $m>0$ and $e>0$; (iii) the canonical threshold is strictly positive.
background
The module treats the isotropic-solid ratio $v_T/v_L=\sqrt{(1-2\nu)/(2-2\nu)}$. Recognition Science fixes Poisson's ratio at $\nu=1/\varphi^2\approx0.382$, yielding $v_T/v_L\approx0.437\approx\varphi^{-2.7}$, compared with empirical metal values near $0.5$–$0.6$.
The domain cost is the local cost functional on a pair of positive reals (mass-like and energy-like coordinates). Upstream, recognition-event cost is already known to be nonnegative via the J-cost nonnegativity lemma. The canonical threshold is the positive scale against which that cost is compared when extracting the sound-speed ratio.
This structure packages exactly the three properties the ratio argument needs: equilibrium vanishing, positivity off equilibrium, and a positive threshold.
proof idea
No proof: this is a structure declaration. Its three fields are Prop-valued hypotheses (diagonal vanishing of domain cost, nonnegativity of domain cost on positive reals, and positivity of the canonical threshold). The concrete inhabitant is assembled later by assigning the sibling lemmas domainCost_at_equilibrium, domainCost_nonneg, and canonicalThreshold_pos.
why it matters
Gives a single named bundle for the cost hypotheses that the φ-sound-speed story depends on. Downstream, cert fills the three fields from the sibling lemmas, and cert_inhabited records that the type is nonempty. That closes the structural side of the Plan v7 pass on $v_T/v_L$ from $\varphi$, tying the continuum elasticity ratio to the same J-cost nonnegativity used elsewhere in the forcing chain. It does not itself derive $\nu=1/\varphi^2$; it only certifies the cost scaffolding those later steps assume.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.