PhiHarmonicForced
For any positive frequency f the structure packages the first harmonic h = f phi together with the identities showing that the ratio equals phi, obeys the self-similar equation r squared equals r plus one, and that phi is the unique positive solution. Frequency-ladder arguments in the Recognition framework cite the construction to justify the minimal-cost resonance step above any given mode. The definition simply assembles the algebraic verifications of the ratio properties and the uniqueness clause already established for self-similar ratios.
claimFor any positive real frequency $f$, let $h = f phi$. Then $h = f phi$, the ratio $h/f = phi$ satisfies the self-similarity equation $r^2 = r + 1$, and $phi$ is the unique positive real number obeying that equation.
background
The J-cost function evaluates the cost of any positive ratio r by the formula one-half times (r plus one over r) minus one. A self-similar ratio is defined by the equation r squared equals r plus one, which is the fixed-point relation whose unique positive root is the golden ratio phi. The module establishes that phi is the minimal-cost non-trivial ratio among all such self-similar values, so that for any oscillating system at frequency f the product f times phi supplies the first minimal-cost resonance above f. This step closes the gap-B argument that feeds the definition of the first phi-ladder rung as Mode1 times phi.
proof idea
The structure is introduced by direct packaging of the candidate harmonic value f times phi together with the three algebraic identities that follow immediately from field arithmetic and the already-proved uniqueness of phi among positive self-similar ratios.
why it matters in Recognition Science
The declaration supplies the typed interface used by the downstream definition phi_harmonic_forced that constructs the explicit instance for any positive f. It thereby records the T6 forcing step in which phi is singled out as the unique self-similar fixed point, allowing the phi-ladder to be erected rung by rung from the J-cost minimality property. The construction is cited in BodyCosmosResonance when the first phi-harmonic is required.
scope and limits
- Does not compute explicit numerical harmonics for concrete frequency values.
- Does not extend the construction to higher rungs or multiple harmonics.
- Does not incorporate dissipation, damping, or non-linear corrections.
- Does not address the case of zero or negative frequencies.
formal statement (Lean)
84structure PhiHarmonicForced (f : ℝ) where
85 harmonic : ℝ
86 harmonic_eq : harmonic = f * phi
87 ratio_is_phi : harmonic / f = phi
88 ratio_self_similar : IsSelfSimilarRatio (harmonic / f)
89 ratio_unique : ∀ r > 0, IsSelfSimilarRatio r → r = phi
90
91/-- The φ-harmonic is forced for any positive frequency. -/