popularity
plain-language theorem explainer
The popularity function gives per-style popularity at scaled time s = t/τ as zero for s ≤ 0 and otherwise 1/(1 + J(s)), where J is the J-cost. Archaeologists reconstructing Petrie curves or physicists deriving cultural succession from Recognition Science would cite this definition. It is introduced directly as a piecewise expression that applies the J-cost formula for positive arguments.
Claim. The popularity function at scaled time $s = t/τ$ is defined by $p(s) := 0$ if $s ≤ 0$, and $p(s) := 1/(1 + J(s))$ otherwise, where $J$ is the J-cost function satisfying $J(1) = 0$ and the Recognition Composition Law.
background
In the module on Pottery Serial Succession from J-Cost, style popularity is modeled as the reciprocal of one plus the recognition cost on a one-dimensional time-parametrized family. The J-cost is the function J(x) = (x + x^{-1})/2 - 1 for x > 0, which vanishes at the fixed point x = 1 and measures the recognition defect between neighboring styles separated by J(φ) ≈ 0.118. The Cost type is the RS-native quantity whose Jcost component supplies the explicit formula used here. The module derives Petrie's 1899 sequence dating as the resulting trajectory, with neighboring minima on the design graph overlapping during a gap-45 frustration interval.
proof idea
This is the base definition itself. It implements the formula in the doc-comment via a single conditional that returns zero on the non-positive branch and otherwise divides one by one plus Cost.Jcost s. No upstream lemmas are invoked; the expression is the direct translation of the J-cost trajectory into a real-valued function.
why it matters
This definition supplies the core function referenced by the downstream theorems popularity_peak, popularity_nonneg, popularity_pos, popularity_le_one and by the structure PotterySerialCert that assembles the certification properties. It realizes the J-cost shape stated in the module doc-comment for modeling ceramic-style succession. Within the Recognition framework it instantiates the J-uniqueness step (T5) and the phi-ladder spacing, furnishing the explicit curve whose half-life τ lies in the falsifiable interval [10, 200] yr.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.