pottery_serial_one_statement
plain-language theorem explainer
The declaration states that style popularity reaches exactly 1 at scaled time s=1, stays in [0,1] for every s, and that the J-cost gap between successive styles lies in (0.11,0.13). Archaeologists reconstructing Petrie curves from recognition cost would cite this as the compact summary of the one-dimensional style succession model. The proof is a direct term-mode conjunction of the peak theorem, the two bounding lemmas, and the gap-band theorem.
Claim. Let $J(s)$ denote the J-cost function and define popularity$(s) = 1/(1+J(s))$ for $s>0$ (and 0 otherwise). Then popularity$(1)=1$, $0≤$ popularity$(s)≤1$ for all real $s$, and $0.11 < J(φ) < 0.13$ where $φ$ is the golden ratio.
background
The module derives Petrie’s 1899 sequence-dating curve as the J-cost trajectory of style popularity on a one-dimensional design graph. Each style is a local J-cost minimum parametrised by scaled time $s=t/τ$; neighbouring minima are separated by the fixed gap $J(φ)=φ-3/2$. Popularity is defined by the recognition cost shape popularity$(s)=1/(1+J(s))$ for $s>0$. The upstream adjacencyGap definition supplies the concrete gap value, while adjacencyGap_band, popularity_peak, popularity_nonneg and popularity_le_one supply the three numerical claims that are conjoined here.
proof idea
The proof is a one-line term wrapper that assembles the four upstream results: popularity_peak supplies the equality at $s=1$; the anonymous function packages popularity_nonneg and popularity_le_one into the universal bound; adjacencyGap_band.1 and .2 supply the two strict inequalities on the gap.
why it matters
This is the single-statement encapsulation of Track I2 in the Recognition Science archaeology module. It shows that the canonical J-cost shape plus the forced value $J(φ)≈0.118$ already reproduces the rise-peak-decline form observed in Predynastic pottery. The result sits downstream of the J-uniqueness and phi-forcing steps (T5–T6) and supplies the quantitative falsifier stated in the module doc-comment: half-lives outside [10,200] yr would refute the model.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.