PhiHarmonicForced
plain-language theorem explainer
The structure encodes that for any positive frequency f the scaled value f phi is the unique self-similar ratio above f, where self-similar means satisfying the quadratic r squared equals r plus one. Frequency-ladder constructions in the Recognition Science cost module cite this when building the first phi-harmonic resonance. It packages the uniqueness of phi as the positive root of the self-similarity equation together with the scaling relation.
Claim. For any positive real number $f$, let $h = f phi$. Then $h = f phi$, the ratio $h/f$ equals $phi$, the ratio satisfies the self-similar equation $r^2 = r + 1$, and $phi$ is the unique positive real satisfying that equation.
background
The module establishes the phi-ladder frequency bridge as part of Gap B closure. The J-cost function evaluates the cost of a ratio r as one half times (r plus one over r) minus one. A self-similar ratio satisfies the equation r squared equals r plus one, which is the fixed-point condition for the recursion r equals one plus one over r. The golden ratio phi is the unique positive solution to this equation.
proof idea
The declaration is a structure that collects the defining properties: the harmonic equals f times phi, the ratio equals phi, the ratio satisfies IsSelfSimilarRatio, and uniqueness of such ratios. No proof steps are needed beyond the field definitions, as it serves as a record type for the forced harmonic.
why it matters
This definition supplies the structure used by phi_harmonic_forced to construct the explicit harmonic for any positive f. It fills the step in the forcing chain from T5 (J-uniqueness) and T6 (phi as self-similar fixed point) to the frequency ladder. In the Recognition framework it supports the eight-tick octave by providing the scale-invariant resonances.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.