MetamaterialBandGapCert
plain-language theorem explainer
The MetamaterialBandGapCert structure packages four properties of the gap-frequency sequence on the phi-ladder: positivity at every rung, exact multiplicative scaling by phi per step, strict increase, and adjacent ratios identically equal to phi. Materials physicists modeling Fibonacci-lattice photonic crystals cite the certificate when confirming that computed band-gap centers match the Recognition Science structural prediction. The declaration is a bare structure definition that collects these universally quantified statements with no proof.
Claim. Let $f(k)$ be the gap-center frequency at rung $k$ on the phi-ladder. The certificate asserts $f(k)>0$, $f(k+1)=f(k)·ϕ$, $f(k)<f(k+1)$, and $f(k+1)/f(k)=ϕ$ for every natural number $k$, where $ϕ$ is the golden ratio.
background
In the Recognition Science treatment of photonic metamaterials the gap-center frequencies sit on the phi-ladder by the definition gapFreq k := referenceFreq * phi ^ k. This places the dimensionless frequencies ω_n / ω_0 at successive rungs with exact scaling factor phi, matching the self-similar geometry of Fibonacci photonic crystals noted in the module documentation.
proof idea
The declaration is a structure definition with an empty proof body. It simply declares four fields, each a universally quantified statement over the gapFreq sequence. The actual verification of those statements is supplied downstream by the lemmas gapFreq_pos, gapFreq_succ_ratio, gapFreq_strictly_increasing and gapFreq_adjacent_ratio when an instance is constructed.
why it matters
This structure is the type of the concrete witness metamaterialBandGapCert, which formalizes the phi-ladder prediction underlying RS_PAT_018. It encodes the self-similar scaling forced by the fixed-point phi (T6) and supplies the structural link between the Recognition framework and the observed golden-ratio cascades in 1D Fibonacci photonic crystals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.