pith. sign in
module module high

IndisputableMonolith.Crystallography.BraggAngleFromPhiLadder

show as:
view Lean formalization →

This module defines the peak-angle spacing ratio for Bragg diffraction peaks as the self-similar fixed point φ from the Recognition Science phi-ladder. It supplies supporting definitions including braggPeakRatio, diffractionCost, and BraggAngleCert that connect crystallographic observables to RS cost structures. The module imports Constants and Cost to anchor all quantities in RS-native units with τ₀ = 1 tick. Its structure consists of a sequence of definitions and basic properties rather than a single theorem.

claimThe Bragg peak spacing ratio satisfies $\frac{\theta_{n+1}}{\theta_n} = \phi$, where $\phi$ is the fixed point of the J-cost map and the peak angles derive from the phi-ladder in the diffractionCost function.

background

The module sits in the Crystallography domain and imports IndisputableMonolith.Constants, which fixes the fundamental RS time quantum as τ₀ = 1 tick, together with IndisputableMonolith.Cost, which supplies the J-cost function J(x) = (x + x^{-1})/2 - 1. These imports allow the module to express diffraction quantities directly on the phi-ladder whose self-similar fixed point is φ. The sibling declarations braggPeakRatio, diffractionCost, and BraggAngleCert then encode the angle spacing and its certification.

proof idea

This is a definition module, no proofs.

why it matters in Recognition Science

The module supplies the explicit link between the phi-ladder (T6) and observable Bragg angles, feeding any downstream crystallography results that require the spacing ratio to equal φ. It closes one concrete application of the Recognition Composition Law and the eight-tick octave structure to a measurable physical ratio.

scope and limits

depends on (2)

Lean names referenced from this declaration's body.

declarations in this module (8)