cert_inhabited
plain-language theorem explainer
cert_inhabited establishes that the BraggAngleCert structure is inhabited by exhibiting the explicit witness cert. Crystallographers modeling quasicrystal diffraction via the φ-ladder would cite this existence result to anchor their peak-ratio and cost conditions. The proof is a direct term construction that applies the structure constructor to the sibling cert definition.
Claim. The set of Bragg angle certificates is non-empty, where each certificate requires the ratio of successive peak angles to exceed 1, the diffraction cost function to vanish whenever measured and predicted values coincide (for nonzero arguments), and the cost to be nonnegative for all positive measured and predicted values.
background
The module treats Bragg's law 2d sin(θ) = nλ for a φ-quasicrystal whose interlayer spacings follow d_n = d_0 / φ^n, yielding sin(θ_n) = λ φ^n / (2d_0) and successive peak-angle ratios approaching φ in the small-angle limit. BraggAngleCert is the structure whose three fields encode exactly these requirements: the ratio exceeds unity, the cost vanishes on the diagonal, and the cost remains nonnegative. This structure sits inside the Recognition Science derivation of diffraction from the φ-ladder fixed point (T6) and the Recognition Composition Law.
proof idea
The proof is a one-line term wrapper that constructs an element of Nonempty BraggAngleCert by feeding the sibling definition cert into the structure constructor.
why it matters
This existence result closes the structural definition of BraggAngleCert inside the crystallography module, confirming that the φ-ladder model satisfies the peak-ratio and cost axioms required by the module's structural theorem. It supplies the concrete witness needed before any downstream application of the certificate to experimental peak data or to the broader forcing chain (T5–T8). The module falsifier remains any quasicrystal diffraction dataset whose successive peak spacing ratio lies outside (φ − 0.1, φ + 0.1).
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.