swadeshDecayCert
plain-language theorem explainer
The Swadesh decay certificate packages four properties of the rung-indexed replacement rate: positivity for every rung, exact multiplication by phi on each step, strict monotonic increase, and adjacent ratio identically phi. Historical linguists working with Swadesh lists would cite the certificate to embed Pagel et al. (2007) replacement estimates inside the Recognition Science phi-ladder. The declaration is a structure instance that directly references the four supporting theorems without additional proof steps.
Claim. Let $r : ℕ → ℝ$ denote the replacement rate at rung $k$. The Swadesh decay certificate asserts that $r(k) > 0$, $r(k+1) = r(k) · ϕ$, $r(k) < r(k+1)$, and $r(k+1)/r(k) = ϕ$ for every natural number $k$.
background
SwadeshDecayCert is the structure recording the four required properties of the decay rate on the phi-ladder. The rate function is defined via referenceRate scaled by phi to the power k. Upstream theorems establish positivity via pow_pos on phi, the successor ratio via pow_succ and ring, strict increase via the ratio greater than one, and the exact phi ratio by simplification. In the local setting of Swadesh-list decay, core vocabulary occupies rung 0 with rate r0, and each higher rung multiplies the rate by phi, matching observed peripheral-to-core ratios of 5-10 over two steps.
proof idea
The definition is a one-line wrapper that supplies the four fields of SwadeshDecayCert by direct reference to rateAtRung_pos, rateAtRung_succ_ratio, rateAtRung_strictly_increasing, and rate_adjacent_ratio.
why it matters
This definition certifies the structural prediction of the phi-ladder for linguistic replacement rates. It closes the module by assembling the component theorems into the certificate structure referenced in the module documentation. The result supports the Recognition Science claim that vocabulary decay follows the same self-similar scaling as other physical quantities, with phi as the fixed point.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.