bandFrequency
plain-language theorem explainer
The definition assigns to each natural number k the value of the golden ratio raised to k, providing the relative frequency scaling for the k-th electromagnetic band. Modelers of spectral structure or biological carrier frequencies would reference it when deriving consecutive-band ratios or populating spectrum certificates. The declaration is introduced as a direct noncomputable equational assignment with no reduction steps or lemmas.
Claim. The scaling factor for the frequency of the k-th band is defined by the expression $phi^k$, where $phi$ is the golden ratio.
background
The module builds the electromagnetic spectrum on the phi-ladder in which each successive band is scaled by one phi-decade. Five canonical bands are identified (radio through UV+X+gamma), corresponding to a configuration dimension of 5, with the visible bandwidth ratio lying between phi and phi squared. The golden ratio itself enters as the self-similar fixed point forced by the Recognition Science chain (T6).
proof idea
The declaration is a direct definition that sets the value equal to phi raised to the power k. No lemmas or tactics are applied; it functions as the base assignment that later ratio statements unfold.
why it matters
This supplies the frequency scaling on which the bandRatio theorem rests to establish that consecutive bands differ by exactly phi, and on which the EMSpectrumCert structure depends to certify the five-band count, the universal phi-ratio property, and the cortical carrier bounds between 8 and 9. It realizes the phi-ladder construction for the electromagnetic spectrum, consistent with the eight-tick octave and the prediction of 5 phi Hz biological resonances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.