BraggAngleCert
plain-language theorem explainer
BraggAngleCert packages the phi peak-ratio inequality, the zero value of diffraction cost at the predicted angle, and nonnegativity of that cost for positive inputs. Quasicrystal diffraction modelers cite it when checking consistency between observed peak spacings and the phi-ladder prediction. The structure is assembled by direct reference to the three upstream lemmas on ratio and J-cost.
Claim. A Bragg-angle certificate consists of the inequality $1 < r$ where $r$ is the successive-peak ratio, the identity $C(a,a)=0$ for all $a≠0$, and the nonnegativity $C(m,p)≥0$ whenever $m>0$ and $p>0$, with $C$ the J-cost of the measured-to-predicted angle ratio.
background
The module treats Bragg's law for a phi-quasicrystal whose interlayer spacings are $d_n = d_0/φ^n$. Successive diffraction peaks then satisfy sin(θ_{n+1})/sin(θ_n) ≈ φ in the small-angle limit, so the ratio braggPeakRatio is defined as phi. The cost function diffractionCost(measured, predicted) is Jcost(measured/predicted). The nonnegativity property is imported from the theorem that every recognition event has nonnegative cost.
proof idea
The declaration is a structure definition whose three fields are filled by the sibling results braggPeakRatio_gt_one, diffractionCost_at_prediction, and diffractionCost_nonneg. No tactics or reductions are required; the structure simply records the three properties.
why it matters
The certificate supplies the structural theorem of the Bragg-angle module and is used to prove cert_inhabited. It applies the phi fixed point (T6) to quasicrystal diffraction and supplies the falsifier that any dataset whose peak-spacing ratio lies outside (φ−0.1, φ+0.1) would refute the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.