IndisputableMonolith.Archaeology.PotterySerialFromJCost
This module defines per-style popularity at scaled time s = t/τ as popularity(s) = 1/(1 + J(s)) for s > 0, together with nonnegativity lemmas and the PotterySerialCert structure. Archaeologists applying Recognition Science to serial dating would cite these objects when modeling production curves from J-cost. The module is definitional, importing τ from Constants and J from Cost, then adding basic bounds and a certificate type.
claimDefine popularity by $popularity(s) = 1/(1 + J(s))$ for $s > 0$, where $s = t/τ$ and $J$ is the J-cost function. The module also supplies $PotterySerialCert$ together with lemmas establishing $Jcost_nonneg_of_pos$, $popularity_nonneg$, $popularity_pos$, $popularity_le_one$, and $adjacencyGap$ properties.
background
The module sits in the archaeology domain of Recognition Science and imports the fundamental time quantum τ₀ = 1 tick from Constants together with the Cost module that supplies the J-cost function. J arises from the T5 uniqueness statement in the forcing chain and satisfies the Recognition Composition Law. Scaled time s = t/τ converts physical time into the dimensionless variable used for popularity curves.
proof idea
This is a definition module, no proofs. The main content consists of the popularity definition drawn directly from the supplied doc-comment, followed by elementary lemmas on nonnegativity and bounds that follow from J properties imported from Cost.
why it matters in Recognition Science
The module supplies the popularity function and PotterySerialCert that connect J-cost to observable serial ordering in archaeological data. It populates the archaeology slot in the framework and feeds any later theorems that apply the phi-ladder or eight-tick octave to artifact chronologies. No used_by edges are recorded, so its role is foundational rather than a direct parent for a named downstream theorem.
scope and limits
- Does not fit the popularity function to any concrete pottery dataset.
- Does not derive or reprove the J-cost function itself.
- Does not extend the model beyond one-dimensional serial ordering.
- Does not address uncertainty quantification or measurement error.
depends on (2)
declarations in this module (13)
-
def
popularity -
theorem
popularity_peak -
theorem
Jcost_nonneg_of_pos -
theorem
popularity_nonneg -
theorem
popularity_pos -
theorem
popularity_le_one -
def
adjacencyGap -
theorem
adjacencyGap_eq -
theorem
adjacencyGap_pos -
theorem
adjacencyGap_band -
structure
PotterySerialCert -
def
potterySerialCert -
theorem
pottery_serial_one_statement