diffractionCost_at_prediction
plain-language theorem explainer
The result shows that the J-cost between a measured diffraction angle and its phi-ladder prediction is exactly zero when the two angles coincide. Crystallographers verifying quasicrystal peak sequences would cite it to confirm that exact matches incur no mismatch penalty. The proof is a one-line wrapper that unfolds the cost definition, reduces the ratio to one, and invokes the J-cost unit lemma.
Claim. For any nonzero real number $a$, the J-cost of the ratio of a measured diffraction angle to its predicted value equals zero when the angles are identical: $J(a/a)=0$.
background
The module treats Bragg peaks for a phi-quasicrystal whose interlayer spacings scale as $d_n = d_0 / phi^n$. DiffractionCost is the J-cost applied to the ratio of measured to predicted angle. Upstream, Jcost is the function $(x-1)^2/(2x)$ and satisfies Jcost(1)=0 by direct simplification. The local setting is the structural theorem that successive peak angles stand in ratio approximately phi, with the falsifier any observed spacing ratio lying outside the interval (phi-0.1, phi+0.1).
proof idea
The proof is a one-line wrapper. It unfolds diffractionCost to expose Jcost(a/a), rewrites the ratio to 1 via division by the nonzero hypothesis, and applies the lemma Jcost_unit0.
why it matters
The declaration supplies the zero-cost clause inside the BraggAngleCert record, which also carries the ratio-greater-than-one fact and nonnegativity. It thereby certifies that phi-ladder predictions are cost-free at exact match, supporting the Recognition Science account of quasicrystal diffraction via the phi fixed point and eight-tick octave. No open scaffolding remains at this step.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.