SwadeshDecayCert
plain-language theorem explainer
SwadeshDecayCert packages four properties of the replacement rate on the phi-ladder: positivity at every rung, exact multiplication by phi on each step up, strict monotonic increase, and adjacent ratios fixed at phi. Linguists modeling Swadesh-list replacement would cite the certificate to embed Pagel et al. (2007) core-versus-peripheral ratios into the Recognition Science geometric progression. The declaration is a pure structure definition that aggregates four sibling lemmas without internal proof steps.
Claim. A Swadesh-list decay-rate certificate asserts that the replacement rate function $r(k)$ satisfies $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
The module places Swadesh-list replacement rates on the phi-ladder, with rateAtRung k defined as referenceRate times phi to the power k. Higher rungs correspond to faster replacement for less stable word classes. The module documentation states that core vocabulary occupies rung 0 at base rate r0 while peripheral vocabulary occupies rung 1 at r0·φ and rung 2 at r0·φ², reproducing the observed peripheral-to-core factor of 5-10 via φ²≈2.618 at two steps. rateAtRung supplies the explicit geometric form used by all four fields of the certificate.
proof idea
SwadeshDecayCert is a structure definition that collects four properties of rateAtRung into one object. The fields are supplied directly by the sibling lemmas rateAtRung_pos, rateAtRung_succ_ratio, rateAtRung_strictly_increasing, and rate_adjacent_ratio when the certificate is later instantiated by swadeshDecayCert. No tactics or reductions occur inside the structure itself.
why it matters
The certificate supplies the structural interface for the Swadesh decay model and is instantiated by the downstream swadeshDecayCert definition. It encodes the geometric progression with common ratio phi that the module links to Pagel et al. observations, realizing the self-similar scaling fixed by T6 in the forcing chain. The construction bridges Recognition Science constants to empirical linguistics without introducing new axioms or open hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.