popularity_le_one
plain-language theorem explainer
The popularity function, defined piecewise as zero for non-positive scaled time and as the reciprocal of one plus J-cost otherwise, is bounded above by unity. Archaeologists reconstructing Petrie sequence curves from ceramic data would cite this inequality to constrain fitted half-lives. The term proof cases on the sign of s, applies non-negativity of J-cost for the positive branch, and closes via a division inequality plus linear arithmetic.
Claim. For every real number $s$, the popularity function satisfies popularity$(s) = 0$ when $s ≤ 0$ and popularity$(s) = 1/(1 + J(s))$ when $s > 0$, where $J(s)$ is the J-cost, and in all cases popularity$(s) ≤ 1$.
background
The module models Predynastic pottery style succession as the J-cost trajectory of successive minima on a one-dimensional design graph. Popularity at scaled time $s = t/τ$ is defined to be zero for $s ≤ 0$ and $1/(1 + Cost.Jcost s)$ for $s > 0$, with the J-cost itself obtained from the multiplicative recognizer comparator. This construction rests on the upstream theorem that J-cost is non-negative for positive arguments, proved by AM-GM on $s + s^{-1} ≥ 2$. The local theoretical setting derives the empirical Petrie curve shape directly from recognition cost minima separated by the gap $J(φ) = φ - 3/2$.
proof idea
The term proof first unfolds the definition of popularity and splits on whether $s ≤ 0$. The non-positive case reduces immediately to $0 ≤ 1$ by numeric normalization. The positive case invokes Jcost_nonneg_of_pos to obtain $0 ≤ J(s)$, rewrites the target as a division inequality via div_le_one, and finishes with linear arithmetic.
why it matters
This bound is packaged into the PotterySerialCert structure together with the peak-at-unity, non-negativity, positivity, and adjacency-gap-positivity properties; that structure is then used verbatim by the one-statement theorem pottery_serial_one_statement. The result therefore supplies one of the four certified properties needed to derive the full Petrie serial curve from the J-cost model, consistent with the Recognition Composition Law and the forced eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.