rateAtRung_succ_ratio
plain-language theorem explainer
rateAtRung_succ_ratio establishes that the Swadesh replacement rate at rung k+1 equals the rate at rung k multiplied by phi. Linguists modeling vocabulary decay on the phi-ladder cite it to obtain adjacent ratios and monotonicity from the base exponential. The proof is a one-line wrapper that unfolds the rate definition, rewrites the successor power, and closes by ring.
Claim. For every natural number $k$, the replacement rate at rung $k+1$ equals the replacement rate at rung $k$ multiplied by $phi$.
background
The upstream definition rateAtRung sets the replacement rate at phi-ladder rung $k$ to referenceRate times phi to the power $k$, with higher rungs corresponding to faster decay. The module places this in the Swadesh-list setting where core vocabulary occupies lower rungs and peripheral terms occupy higher rungs, so that adjacent-category ratios equal phi. This supplies the geometric progression whose square approximates the empirical peripheral-to-core factor of 5-10 reported by Pagel et al.
proof idea
One-line wrapper that unfolds rateAtRung, rewrites the successor exponent via pow_succ, and closes with ring.
why it matters
It supplies the one-step multiplication by phi required by rate_adjacent_ratio, rateAtRung_strictly_increasing, and swadeshDecayCert. The result fills the structural prediction in the module documentation that replacement rates advance geometrically with ratio phi, matching observed factors via phi squared. It anchors the phi-ladder application to linguistics within the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.