PotterySerialCert
plain-language theorem explainer
The PotterySerialCert structure bundles the verified properties of the popularity function derived from J-cost together with the numerical band on the adjacency gap between successive styles. Archaeologists reconstructing Predynastic ceramic sequences would cite it to anchor Petrie curves in the Recognition framework. It is assembled as a record whose fields are supplied directly by six sibling lemmas on peak value, bounds, and the gap interval (0.11, 0.13).
Claim. A record type whose instances certify that the popularity function $p(s) = 1/(1+J(s))$ for $s>0$ satisfies $p(1)=1$, $p(s)≥0$ for all real $s$, $p(s)>0$ whenever $s>0$, and $p(s)≤1$ for all $s$, together with the statements $0<Δ$ and $0.11<Δ<0.13$ where $Δ=J(φ)$ is the J-cost gap between neighboring styles.
background
In the Recognition Science model of archaeological serialisation, style popularity at scaled time $s=t/τ$ is given by $p(s)=1/(1+J(s))$ for $s>0$, where $J$ is the J-cost function. The adjacency gap $Δ$ between successive styles is defined as $Δ:=J(φ)=φ-3/2≈0.118$. The module derives the canonical Petrie curve shape from the Recognition Composition Law and the uniqueness of the J-function, with the gap fixed by the self-similar fixed point $φ$. Upstream results establish that $p(1)=1$ because $J(1)=0$, that $p(s)≥0$ and $p(s)≤1$ by direct computation from the definition of $J$, and that $p(s)>0$ for $s>0$ using the non-negativity of J-cost.
proof idea
The structure is a plain record definition whose six fields are populated directly by the already-proved theorems popularity_peak, popularity_nonneg, popularity_pos, popularity_le_one, adjacencyGap_pos, and adjacencyGap_band. No additional reasoning is required inside the structure itself; it simply aggregates the results of the preceding lemmas on the popularity function and the gap.
why it matters
This certificate supplies the master data structure for the pottery serial succession theorem, which reconstructs Petrie's sequence-dating method as a direct consequence of J-cost minimisation on a one-dimensional design graph. It closes the derivation by confirming that the inter-style gap lies inside the narrow interval (0.11, 0.13) predicted by the eight-tick octave and the value of $φ$. The construction feeds the downstream potterySerialCert definition that packages the full empirical match.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.