gapFreq_succ_ratio
plain-language theorem explainer
Successive band-gap center frequencies on the phi-ladder obey the recurrence gapFreq(k + 1) equals gapFreq(k) times phi. Materials physicists modeling Fibonacci photonic crystals cite this to recover the golden-ratio scaling of gap positions from the ladder structure. The proof is a direct algebraic reduction that unfolds the gapFreq definition, applies the power successor identity, and simplifies via ring.
Claim. For every natural number $k$, the band-gap center frequency at rung $k+1$ equals the frequency at rung $k$ multiplied by the golden ratio: if $ω_k$ denotes the center at rung $k$ then $ω_{k+1} = ω_k · ϕ$.
background
The module develops the structural prediction for photonic metamaterials with golden-ratio lattice geometry. Gap-center frequencies form a phi-ladder whose adjacent ratios equal phi exactly, matching observations in 1D Fibonacci photonic crystals. gapFreq(k) is defined as referenceFreq multiplied by phi to the power k, placing the center frequency at rung k. This theorem supplies the immediate successor relation that generates the ladder. It rests on the explicit power form given by the gapFreq definition.
proof idea
The proof is a term-mode reduction. It unfolds gapFreq to expose the power expression, rewrites the exponent via the successor rule, and finishes with ring to equate the two sides.
why it matters
This supplies the one-step multiplicative relation used to prove the adjacent ratio equals phi in gapFreq_adjacent_ratio, the strict increase in gapFreq_strictly_increasing, and the full certificate in metamaterialBandGapCert. It realizes the self-similar scaling required by the phi fixed point in the Recognition Science framework, specifically the T6 forcing of phi as the self-similar fixed point, for the metamaterial band-gap application.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.