diffractionCost_nonneg
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not compute numerical peak angles for concrete phi rungs.
- Does not invoke the small-angle approximation stated in the module doc.
- Does not address the five-fold symmetry of the original Shechtman patterns.
- Does not link to the T0-T8 forcing chain or the Recognition Composition Law.
formal statement (Lean)
48theorem diffractionCost_nonneg (m p : ℝ) (hm : 0 < m) (hp : 0 < p) :
49 0 ≤ diffractionCost m p := by
proof body
One-line wrapper that applies unfold.
50 unfold diffractionCost; exact Jcost_nonneg (div_pos hm hp)
51