fractureCost_nonneg
plain-language theorem explainer
The non-negativity of fracture cost for positive strain energy s and surface energy sur follows from the corresponding property of the J-cost function. Materials scientists modeling Griffith crack propagation in the Recognition Science framework would cite this to confirm physical consistency of the energy ratio. The proof is a one-line wrapper that unfolds the fractureCost definition and applies the Jcost_nonneg lemma to the positive quotient.
Claim. If $s > 0$ and $sur > 0$, then $0 ≤ J(s / sur)$, where $J(x) = (x + x^{-1})/2 - 1$ is the J-cost function.
background
The J-cost function is defined as $J(x) = (x + x^{-1})/2 - 1$ and satisfies $J(x) ≥ 0$ for all $x > 0$ by the AM-GM inequality, as established in the upstream Jcost_nonneg lemmas across Cost, Gravity, and Navier-Stokes modules. The fractureCost is the specialization of J-cost to the ratio of strain energy to surface energy. This module develops the Recognition Science account of fracture mechanics, where the Griffith criterion states that a crack propagates when the strain energy release rate meets or exceeds twice the surface energy factor $J(φ) × E × a_0$.
proof idea
The proof unfolds the definition of fractureCost to obtain Jcost applied to the ratio s/sur, then invokes the Jcost_nonneg lemma on the positive real produced by div_pos hs hsur.
why it matters
This result supplies the cost_nonneg component of the FractureCert structure that collects the core properties of the RS fracture model. It supports the structural theorem in the module that derives the Griffith critical release rate and the Paris law exponent m = 4 from four-point symmetry. The non-negativity ensures the energy ratio remains physically admissible and aligns with the J-uniqueness step in the forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.