frequency_pos
plain-language theorem explainer
The theorem shows that the frequency at the k-th rung of the phi-ladder is strictly positive for every natural number k. Workers certifying plasmonic modes in the Recognition Science framework cite it to confirm that all five canonical modes have positive frequencies. The proof is a one-line application of the general positivity of powers with positive base.
Claim. For every natural number $k$, the frequency defined by $omega_k = phi^k$ satisfies $omega_k > 0$.
background
The module treats plasmonic modes derived from the phi-ladder, with five canonical types (surface plasmon polariton, localized surface plasmon, propagating, bulk, gap plasmon) each assigned a frequency one rung up the ladder. The upstream definition sets the plasmon frequency at rung k to exactly phi raised to k. The local setting is a module with zero sorrys or axioms, placing frequencies on the self-similar fixed point phi.
proof idea
The proof is a one-line wrapper that applies pow_pos to the positivity of phi and the natural exponent k.
why it matters
This result supplies the frequency_always_pos field inside the plasmonicModeCert definition, completing the certification that all five modes have positive frequencies. It anchors the phi-ladder construction used for mode frequencies and constants in the Recognition framework, consistent with the phi fixed point and the Recognition Composition Law. No open questions are addressed.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.