cert
plain-language theorem explainer
The cert assembles a BraggAngleCert record certifying phi-ladder diffraction peaks by supplying the ratio exceeding one, zero cost on the prediction diagonal, and nonnegative cost. A crystallographer working with quasicrystal X-ray data would cite it to confirm that successive peak ratios satisfy the Recognition Science cost minimum. The definition is a direct structure constructor delegating each field to an established lemma on the J-cost and the phi inequality.
Claim. Let BraggAngleCert be the structure requiring that the ratio of successive Bragg peak angles exceeds 1, that the diffraction cost vanishes for any nonzero argument on the diagonal, and that the diffraction cost remains nonnegative for all positive measured and predicted values. The cert instance is the record satisfying these three properties by direct substitution of the phi-ladder ratio theorem, the J-cost identity lemma, and the general nonnegativity result.
background
In the Bragg angle module, interlayer spacings follow the phi-ladder d_n = d_0 / phi^n, so that Bragg's law 2 d_n sin(theta_n) = n lambda yields peak angles whose successive ratios approach phi in the small-angle limit. The BraggAngleCert structure packages three properties that certify this model: ratio greater than one, cost at prediction zero for nonzero a, and cost nonnegative for positive m and p. These rest on the upstream results that reduce the ratio inequality to one_lt_phi, unfold the zero-cost identity to Jcost_unit0, and apply the general cost nonnegativity theorem to the ratio.
proof idea
The definition constructs the BraggAngleCert record by supplying the three fields directly from prior theorems: the ratio field from braggPeakRatio_gt_one, the zero-cost field from diffractionCost_at_prediction, and the nonnegativity field from diffractionCost_nonneg. No further tactics are required; it is a pure record literal that assembles the certificate from the established lemmas.
why it matters
This definition supplies the concrete certificate required by the structural theorem in the crystallography module, confirming that the phi-ladder reproduces the observed five-fold symmetry in quasicrystal diffraction. It closes the local scaffolding for the Bragg angle predictions and aligns with the Recognition Science forcing chain by embedding the phi fixed point into the cost function for diffraction events. The module falsifier states that any dataset with peak ratios outside the interval (phi - 0.1, phi + 0.1) would refute the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.