fractureCost_at_threshold
plain-language theorem explainer
The fracture cost vanishes exactly when strain energy equals surface energy for nonzero values. Materials modelers applying the Recognition Science J-cost to Griffith crack propagation would cite this to fix the zero-cost threshold. The proof is a one-line wrapper that unfolds fractureCost, reduces the ratio to 1, and invokes the Jcost unit lemma.
Claim. Let $J$ be the J-cost function. For any nonzero real $e$, $J(e/e)=0$, where fracture cost is defined as $J$ applied to the ratio of strain energy to surface energy.
background
In this module the J-cost is $J(x)=(x-1)^2/(2x)$. fractureCost applies it to the ratio of strain energy to surface energy, so that the quantity measures excess energy available for crack advance relative to the surface-energy barrier. The module states the Griffith criterion as crack propagation when strain-energy release rate $G$ meets or exceeds twice the surface energy, with the RS prediction $G_c=2J(φ)Ea_0$ yielding roughly 14 J/m² for typical metals.
proof idea
One-line wrapper. Unfold fractureCost to obtain Jcost(e/e), rewrite the ratio to 1 via div_self under the nonzero hypothesis, then apply the upstream lemma Jcost_unit0 which states Jcost 1 = 0.
why it matters
The result supplies the zero-cost threshold inside FractureCert, the structural certificate for the fracture-mechanics model. It directly supports the module's claim that the critical release rate lies inside the observed 10-100 J/m² band for metals and links the J-cost functional equation to material failure. The parent cert aggregates this with non-negativity, surface-factor positivity, and the Paris exponent m=4 derived from four-point symmetry.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.