adoptionTimeRatio
plain-language theorem explainer
The theorem establishes that consecutive adoption times on the phi-ladder scale exactly by the golden ratio phi. Economists working in Recognition Science on innovation diffusion would cite it to obtain the predicted scaling between Rogers' adopter categories. The proof is a direct algebraic reduction that unfolds the power definition of adoptionTime and simplifies via successor exponent and ring cancellation.
Claim. For each natural number $k$, the ratio of consecutive adoption times satisfies $a(k+1)/a(k) = phi$, where the adoption time function is defined by $a(k) := phi^k$ and $phi$ is the self-similar fixed point.
background
The module interprets Rogers' five adopter categories as positions on the phi-ladder of social recognition cost, with the number of categories identified with configDim D = 5. The upstream definition states that adoptionTime(k) equals phi raised to k, supplying the explicit scaling law used here. This construction sits inside the Recognition Science forcing chain at T6, where phi is fixed as the unique self-similar point satisfying the Recognition Composition Law.
proof idea
The term proof unfolds adoptionTime to obtain phi^{k+1} over phi^k. It invokes pow_pos to obtain positivity of phi^k, rewrites via pow_succ and div_eq_iff to clear the denominator, then closes the equality by ring simplification.
why it matters
The result supplies the phi_ratio field inside the innovationDiffusionCert definition, which packages the five-category count together with the phi scaling. It directly realizes the module's stated RS prediction that adoption transition times ratio by phi, thereby connecting the economic observable to the T5 J-uniqueness and T6 phi fixed-point steps of the UnifiedForcingChain without extra hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.