rateAtRung_strictly_increasing
plain-language theorem explainer
The theorem establishes that replacement rates for Swadesh-list vocabulary increase strictly with each step up the phi-ladder. Linguists modeling core versus peripheral word decay would cite it to confirm that higher-rung terms replace faster by the exact factor phi. The proof is a short algebraic reduction that rewrites the successor step, invokes positivity of the rate, and applies the bound phi greater than 1.5 to obtain the strict inequality via left-multiplication.
Claim. For every natural number $k$, the replacement rate at rung $k$ is strictly less than the replacement rate at rung $k+1$, where the rate equals the base reference rate times the golden ratio to the power $k$.
background
The module models Swadesh-list decay rates on the phi-ladder, with core vocabulary at lower rungs and peripheral terms at higher rungs. Replacement rate at rung $k$ is defined as the base reference rate multiplied by phi to the power $k$, where phi is the golden ratio. Upstream results supply the successor identity that the rate at rung $k+1$ equals the rate at rung $k$ times phi, the positivity of every rate, and the bound phi greater than 1.5.
proof idea
The proof rewrites the target inequality using the successor ratio lemma to obtain rate at $k$ times phi greater than rate at $k$. It then applies the positivity theorem to obtain a positive left factor, invokes the phi greater than 1.5 lemma to obtain the strict multiplier inequality, and finishes with mul_lt_mul_of_pos_left followed by simpa.
why it matters
The result supplies the strictly increasing property required by the Swadesh decay certificate, which bundles positivity, one-step ratio, strict increase, and adjacent ratio equal to phi. It completes the structural prediction that peripheral-to-core replacement ratios match observed factors of 5-10 after two rung steps, consistent with the forced self-similar value of phi.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.