gapFreq_strictly_increasing
plain-language theorem explainer
The band-gap center frequency on the phi-ladder, defined as reference frequency times phi to the power k, rises strictly with each natural-number rung. Materials physicists working on Fibonacci photonic crystals cite this to confirm monotonicity of the self-similar cascade predicted by golden-ratio lattice geometry. The tactic proof rewrites the successor via the ratio lemma, invokes positivity of the current frequency, and applies the multiplication inequality after establishing phi exceeds 1.5.
Claim. For every natural number $k$, the band-gap center frequency satisfies $f_k < f_{k+1}$, where $f_k = f_0 phi^k$ and $phi$ is the golden ratio.
background
In the metamaterial band-gap module the gap frequency at rung $k$ is defined as referenceFreq times phi to the power $k$. The module documentation states that photonic metamaterials with golden-ratio lattice geometry exhibit a phi-laddered family of band gaps whose adjacent-rung ratios equal exactly phi, matching empirical observations in one-dimensional Fibonacci photonic crystals. The theorem depends on the successor-ratio result that the next gap frequency equals the current one multiplied by phi, on the positivity theorem for every rung, and on the constant lemma establishing phi greater than 1.5.
proof idea
The proof rewrites the target inequality with the successor-ratio theorem to obtain the form gap frequency at k less than gap frequency at k times phi. It obtains positivity of the current frequency from the positivity theorem. It derives one less than phi from the phi-greater-than-1.5 lemma via linarith. It then applies the multiplication inequality for positive left factors and finishes with simpa.
why it matters
The result supplies the strictly_increasing field inside the metamaterialBandGapCert definition that packages the full certificate for phi-laddered band gaps. It thereby supports the structural prediction underlying the patent and RS_PAT_018, linking the LawOfExistence constants bundle to the explicit monotonicity required for the self-similar cascade on the phi-ladder. The theorem closes one concrete link in the Recognition Science chain from the forcing steps that fix phi to the materials-level certificate.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.