braggPeakRatio
plain-language theorem explainer
The definition assigns the golden ratio φ to the peak-angle spacing ratio of successive Bragg peaks in a φ-quasicrystal. Crystallographers modeling diffraction patterns from interlayer spacings d_n = d_0 / φ^n cite it to obtain the scaling θ_{n+1}/θ_n ≈ φ under Bragg's law in the small-angle limit. The declaration is a direct one-line abbreviation that equates the ratio to the constant phi.
Claim. Define the peak-angle spacing ratio $r$ by $r := φ$, where $φ$ is the golden ratio.
background
The module applies Bragg's law $2d sin(θ) = nλ$ to a φ-quasicrystal whose interlayer spacings satisfy $d_n = d_0 / φ^n$. This produces $sin(θ_n) = λ φ^n / (2d_0)$, so successive peak angles scale by φ in the small-angle regime. The construction accounts for the five-fold symmetry first observed in quasicrystals. No upstream lemmas are invoked.
proof idea
The declaration is a one-line definition that sets the ratio equal to the constant phi.
why it matters
It supplies the ratio value required by BraggAngleCert to certify that the ratio exceeds one and that diffractionCost vanishes at the predicted point. The definition realizes the self-similar scaling forced by the φ fixed point. The module falsifier requires experimental peak ratios to lie within 0.1 of φ.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.