diffractionCost
plain-language theorem explainer
diffractionCost assigns to each pair of measured and predicted diffraction angles the J-cost of their ratio. Quasicrystal diffraction analysts cite it when testing whether observed peak positions align with phi-ladder predictions from Recognition Science. The definition is a direct one-line application of Jcost to the ratio, which propagates the zero-at-unity and nonnegativity properties established for Jcost.
Claim. Let $m$ be a measured diffraction angle and $p$ its predicted value from the phi-ladder. The diffraction cost is defined by diffractionCost$(m,p) := J(m/p)$, where $J$ is the J-cost function.
background
The module develops structural results for diffraction peaks in phi-quasicrystals, where interlayer spacings follow $d_n = d_0 / phi^n$. Bragg's law then implies successive peak angles satisfy a ratio approaching phi in the small-angle limit. The original 5-fold symmetry in Shechtman quasicrystals is recovered from the phi-lattice structure.
proof idea
The declaration is a one-line wrapper that applies Jcost to the ratio of the measured angle over the predicted angle.
why it matters
diffractionCost supplies the cost metric inside the BraggAngleCert structure, which records that the bragg peak ratio exceeds one, the cost vanishes at equality, and the cost remains nonnegative. It supports the module's structural theorem linking diffraction patterns to the phi self-similar fixed point. The falsifier for the surrounding results is any quasicrystal X-ray dataset whose peak spacing ratios fall outside the interval (phi - 0.1, phi + 0.1).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.