rate_adjacent_ratio
plain-language theorem explainer
The theorem shows that replacement rates for Swadesh-list vocabulary increase by exactly the golden ratio phi when moving one rung up the phi-ladder. Modelers of language evolution citing Pagel et al. would use this to derive the predicted factor of phi squared between core and peripheral word classes. The proof applies the successor ratio identity and cancels the common positive factor via field simplification.
Claim. For each natural number $k$, let $r(k)$ denote the replacement rate at phi-ladder rung $k$, defined by $r(k) = r_0 phi^k$ where $r_0$ is the reference rate. Then $r(k+1)/r(k) = phi$.
background
The module models Swadesh-list decay rates on the phi-ladder. The replacement rate at rung $k$ is defined as referenceRate times phi to the power $k$, with higher rungs corresponding to faster replacement for less stable word classes. The positivity of these rates follows from the positivity of phi and the reference rate. The successor ratio lemma establishes that the rate at rung $k+1$ equals the rate at rung $k$ multiplied by phi.
proof idea
The proof rewrites the left-hand side using the successor ratio lemma rateAtRung_succ_ratio. It then invokes field_simp, supplying the non-equality to zero from the positivity theorem rateAtRung_pos at $k$, to simplify the division to phi.
why it matters
This result supplies the adjacent ratio equality required by the SwadeshDecayCert definition, which certifies the full set of decay-rate properties including positivity, one-step ratios, strict increase, and the phi equality. It directly implements the module's claim that adjacent-category ratios equal phi, consistent with the Recognition Science phi-ladder structure where phi arises as the self-similar fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.