cert
plain-language theorem explainer
Packages three structural facts about the domain cost and the canonical threshold into a single inhabited certificate for the kinetic-friction-from-J construction. Anyone citing the μ_k ≈ J(φ) derivation uses this bundle. The body is a pure structure constructor that wires three already-proved field lemmas.
Claim. There is a certificate recording that the domain cost vanishes on equal nonzero arguments ($C(r,r)=0$ for $r\neq 0$), is nonnegative for positive mass and energy, and that the canonical threshold is strictly positive.
background
The module derives a kinetic friction coefficient from the Recognition Science J-cost. In RS units the cost functional is $J(x)=(x+x^{-1})/2-1$, forced unique by the Recognition Composition Law (T5). The module claims $\mu_k\approx J(\varphi)\approx 0.118$ in the canonical boundary-lubrication regime, sitting in the empirical lubricated band $\approx 0.05$–$0.15$.
domainCost is the local cost used for the friction model; the certificate demands it vanish when the two arguments agree and stay nonnegative on the positive orthant. canonicalThreshold is the positive cutoff that marks the onset of the dissipative regime. Upstream, nonnegativity of recognition cost is already known from ObserverForcing (cost_nonneg: every recognition event has $0\le e.\mathrm{cost}$ via $J$-cost nonnegativity).
proof idea
Pure structure inhabitation. The three fields of FrictionCoeffCert are filled by the sibling lemmas domainCost_at_eq, domainCost_nonneg, and canonicalThreshold_pos. No extra algebra or tactics; the def is a one-line record constructor.
why it matters
Gives a single named witness that the structural hypotheses of the friction-from-J story hold, so downstream statements can cite one object rather than three separate lemmas. The module frames this as a structural theorem (zero sorry, zero axiom) supporting $\mu_k\approx J(\varphi)\approx 0.118$, which lands in the center of the lubricated empirical range. It sits on the J-uniqueness landmark (T5) and the forced golden ratio $\varphi$ (T6). No downstream users are recorded yet; the certificate is the local packaging step before numerical or comparative claims.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.