potterySerialCert
plain-language theorem explainer
This definition constructs a certificate object asserting that popularity derived from J-cost peaks at unity for scaled time s=1, remains in [0,1], and that the adjacency gap J(φ) lies in (0.11,0.13). Archaeologists modeling Petrie sequence dating would cite it to ground empirical ceramic succession curves in the Recognition Science J-cost framework. The construction is a direct record that bundles the component theorems popularity_peak, popularity_nonneg, popularity_pos, popularity_le_one, adjacencyGap_pos and adjacencyGap_band.
Claim. Let $popularity(s) = 1/(1+J(s))$ for $s>0$ (and 0 otherwise), where $J$ is the J-cost function. There exists a certificate asserting $popularity(1)=1$, $0≤popularity(s)≤1$ for all real $s$, $popularity(s)>0$ for $s>0$, and $0.11 < J(φ) < 0.13$.
background
In the Recognition Science treatment of archaeology, style popularity follows the J-cost trajectory on a one-dimensional design graph. The function popularity(s) is defined as 1/(1 + Cost.Jcost s) for s>0 (and 0 otherwise), yielding the rise-peak-decline shape of Predynastic Egyptian pottery sequences. Neighboring style minima are separated by the adjacency gap J(φ) ≈ 0.118.
proof idea
The definition is a direct record construction that populates each field of the PotterySerialCert structure by referencing the corresponding pre-proved theorem: popularity_peak for the peak at s=1, popularity_nonneg and popularity_pos for non-negativity and positivity, popularity_le_one for the upper bound, and adjacencyGap_pos together with adjacencyGap_band for the gap interval.
why it matters
This definition packages the core properties needed to certify that ceramic style succession follows the J-cost trajectory, realizing the derivation of Petrie's sequence dating. It completes the local theorem statement for the pottery serial model. No downstream uses are recorded yet, but it supports quantitative checks against archaeological half-life data in [10,200] yr.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.