cert
plain-language theorem explainer
The cert definition constructs a FractureCert record bundling four properties of the J-cost-derived fracture cost function: vanishing exactly at the equal-parameter threshold, non-negativity for positive inputs, positivity of the surface energy factor, and the Paris exponent fixed at 4. Materials modelers would cite it to verify that Recognition Science fracture predictions satisfy Griffith and Paris laws in closed form. It is assembled as a direct record constructor from four sibling theorems in the same module.
Claim. Let FractureCert be the structure requiring: for all real $e$ with $e$ nonzero the fracture cost satisfies fractureCost$(e,e)=0$; for all positive $s$, sur the fracture cost is nonnegative; the surface energy factor is positive; and the Paris law exponent equals 4. Then cert is the explicit instance of this structure.
background
The module derives fracture mechanics from the J-cost of recognition events. Upstream, cost_nonneg states that the cost of any recognition event is non-negative, obtained by applying Jcost_nonneg to a positive state. The fractureCost function is the ratio-based cost (unfolded to Jcost of the ratio), surfaceEnergyFactor is the RS surface energy J(φ) scaled by modulus and spacing, and parisLawExponent is fixed at 4 by four-point symmetry of the stress field. The module states the Griffith criterion G ≥ 2γ with RS prediction G_c = 2 J(φ) E a0 and the Paris law da/dN = C (ΔK)^m with m=4.
proof idea
The definition is a one-line record constructor that directly supplies the four fields of FractureCert by referencing the sibling theorems fractureCost_at_threshold, fractureCost_nonneg, surfaceEnergyFactor_pos, and parisLawExponent_eq.
why it matters
This definition closes the structural theorem of the module by packaging the J-cost properties into a single certificate usable for materials predictions. It links the non-negativity of recognition cost to the Griffith energy release rate and to the Paris exponent 4 arising from configDim + 1 with D=3. The module falsifier is any G_c measurement lying systematically outside the J(φ) E a0 band by more than 50 percent.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.