phi_harmonic_forced
plain-language theorem explainer
Researchers modeling minimal-cost resonances cite this definition to obtain the first φ-harmonic above any positive frequency f as the product f φ. It supplies the explicit value together with the verification that the ratio equals φ and is the unique self-similar ratio. The definition is assembled by direct field assignment, reflexivity for the equality, and direct application of the self-similarity and uniqueness lemmas for φ.
Claim. For every positive real number $f$, the first φ-harmonic is the real $h = f φ$ satisfying $h = f φ$, the ratio $h/f = φ$, the ratio satisfies the self-similarity equation $r^2 = r + 1$, and φ is the unique positive solution to that equation.
background
The module treats the φ-ladder as the minimal-cost bridge between frequencies. The J-cost function J(r) = ½(r + r⁻¹) − 1 evaluates the cost of any positive ratio r. The golden ratio φ is the unique positive fixed point of the self-similar recursion r = 1 + 1/r, i.e., r² = r + 1. This module proves that φ is the minimal-cost non-trivial ratio among all r > 1 satisfying the self-similarity equation. Therefore, for any oscillating system at frequency f, the first φ-harmonic f × φ is the minimal-cost resonance above f.
proof idea
The definition constructs an instance of the required structure by setting the harmonic field directly to f multiplied by phi. The equality field is discharged by reflexivity. The ratio-equals-phi field follows from left cancellation of f in the division. The self-similarity field applies the same cancellation then invokes the theorem that phi is self-similar. The uniqueness field delegates immediately to the theorem establishing that phi is the unique positive self-similar ratio.
why it matters
This definition closes the gap-B step in the φ-ladder frequency bridge. It supplies the concrete first harmonic needed to define f_phi_rung1 in BodyCosmosResonance. Within the Recognition framework it realizes the T6 forcing of phi as the unique self-similar fixed point, ensuring that the first resonance above any base frequency carries the minimal J-cost among scale-invariant ratios.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.