rateAtRung_pos
plain-language theorem explainer
rateAtRung_pos asserts that the replacement rate at every phi-ladder rung k is strictly positive. Linguists modeling Swadesh-list decay via the Recognition Science phi-ladder cite it to guarantee positivity before ratio or monotonicity arguments. The proof unfolds the definition rateAtRung k = phi^k and applies pow_pos together with linarith on the known positivity of phi.
Claim. For every natural number $k$, the replacement rate $r_k$ at rung $k$ on the phi-ladder satisfies $0 < r_k$, where $r_k = 1 · phi^k$.
background
The module places Swadesh-list replacement rates on the phi-ladder: core vocabulary occupies rung 0 with reference rate 1 (RS-native units), while rung k carries rate phi^k. rateAtRung is defined directly as referenceRate * phi^k with referenceRate fixed at 1. Constants supplies the golden-ratio value phi together with its positivity and phi > 1.5 facts from the LawOfExistence bundle. The positivity statement is invoked immediately by the adjacent-ratio and strictly-increasing theorems that build the SwadeshDecayCert certificate.
proof idea
The term-mode proof first unfolds rateAtRung and referenceRate, reducing the goal to 0 < phi^k. It then invokes pow_pos Constants.phi_pos k to obtain the strict inequality, after which linarith closes the goal.
why it matters
rateAtRung_pos supplies the positivity hypothesis required by rate_adjacent_ratio and rateAtRung_strictly_increasing, which together populate the SwadeshDecayCert structure. The certificate encodes the structural claim that rates increase by exactly phi at each rung step, reproducing the observed peripheral-to-core factor of roughly 5-10 reported by Pagel et al. (2007). It therefore anchors the entire decay-rate model inside the Recognition Science framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.