diffractionCost_nonneg
plain-language theorem explainer
The declaration establishes non-negativity of the J-cost applied to the ratio of measured to predicted Bragg peak angles, for any positive reals m and p. Workers on quasicrystal X-ray patterns would cite it to guarantee the cost remains a valid non-negative deviation measure inside the phi-ladder model. The proof is a one-line wrapper that unfolds the definition and invokes the established Jcost_nonneg lemma on the positive ratio.
Claim. Let $m,p>0$. Then $0≤J(m/p)$, where $J(x)=(x+x^{-1})/2-1$ denotes the J-cost function.
background
The module treats Bragg's law for a phi-quasicrystal whose interlayer spacings follow the phi-ladder $d_n=d_0/φ^n$. diffractionCost is the sibling definition Jcost(measured_angle/predicted_angle), with Jcost the standard cost from the Cost module. Jcost_nonneg (appearing in six upstream modules) asserts $J(x)≥0$ for $x>0$, proved either by the algebraic identity $J(x)=(x-1)^2/(2x)$ plus positivity or by the AM-GM bound $x+x^{-1}≥2$. The module doc states the structural theorem status and supplies the falsifier of peak-spacing ratios outside $(φ-0.1,φ+0.1)$.
proof idea
One-line wrapper that unfolds diffractionCost to Jcost(m/p) and applies Jcost_nonneg to the hypothesis div_pos hm hp, which yields 0<(m/p).
why it matters
The result is invoked inside the cert definition that assembles BraggAngleCert (ratio_gt_one, cost_at_prediction, cost_nonneg). It therefore closes the non-negativity leg of the structural theorem for phi-ladder diffraction peaks, consistent with the Recognition Science use of J-cost to quantify deviations from self-similar fixed points. No open scaffolding remains in this file.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.