popularity_pos
plain-language theorem explainer
For positive scaled time s the popularity function returns a strictly positive value. Archaeologists reconstructing Petrie serial curves from recognition cost would cite the result to guarantee positive style frequencies throughout the sequence. The term proof unfolds the conditional definition, negates the non-positive case, applies positivity of division, and reduces the denominator via the nonnegativity of J-cost.
Claim. If $s > 0$, then $1/(1 + J(s)) > 0$, where $J(s)$ is the J-cost at scaled time $s$.
background
The module models Predynastic pottery style succession as a J-cost trajectory on a one-dimensional design graph. Popularity at scaled time $s = t/τ$ is defined to be zero for $s ≤ 0$ and $1/(1 + J(s))$ otherwise, reproducing the observed rise-peak-decline shape with neighboring styles separated by $J(φ) ≈ 0.118$. The upstream lemma Jcost_nonneg_of_pos states that $s > 0$ implies $J(s) ≥ 0$ by the AM-GM inequality $s + s^{-1} ≥ 2$.
proof idea
Unfold the popularity definition to expose the conditional. Rewrite the if-condition via not_le.mpr on the hypothesis $0 < s$. Apply div_pos with numerator one_pos. Invoke Jcost_nonneg_of_pos to obtain $0 ≤ J(s)$, then close with linarith to obtain the strict positivity of the denominator.
why it matters
The result is packaged into the PotterySerialCert structure alongside peak value one, nonnegativity, and adjacency-gap positivity; that structure certifies the full set of properties needed for the serial-dating model. It directly supports the derivation of the Petrie curve from the J-cost minimum with gaps fixed by the phi self-similar point. The module falsifier remains quantitative half-lives outside the interval [10, 200] yr.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.