parisLawExponent_pos
plain-language theorem explainer
The theorem establishes that the Paris law exponent in the Recognition Science fracture model is strictly positive. Materials scientists applying fatigue crack growth models would cite it when using da/dN = C (ΔK)^m with the predicted m value. The proof is a one-line wrapper that rewrites the definition to the constant 4 and applies numeric normalization to confirm positivity.
Claim. $0 < m$ where $m$ is the Paris law exponent in the crack growth law $da/dN = C (ΔK)^m$.
background
The Fracture Mechanics from J-Cost module derives Griffith crack propagation from the J-cost functional. It predicts the critical strain energy release rate as G_c = 2 J(φ) E a_0, where E is Young's modulus and a_0 is interatomic spacing, yielding values around 14 J/m² for typical metals. The Paris law exponent is defined as m = configDim + 1 with configDim = 3, giving m = 4 from the four-point symmetry of the stress intensity field.
proof idea
This is a one-line wrapper proof. It applies the rewrite tactic using the equality theorem that substitutes the definition of the exponent, then invokes norm_num to verify that the resulting constant 4 is positive.
why it matters
The result confirms positivity of the exponent in the Paris law within the Recognition Science fracture framework, supporting the structural theorem on Griffith criterion and G_c predictions. It aligns with the eight-tick octave and D = 3 spatial dimensions by setting m = 4 = 3 + 1. The module supplies a falsifier for any fracture toughness data falling outside the J(φ) E a_0 band by more than 50%.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.