adjacencyGap_band
plain-language theorem explainer
The J-cost gap between successive pottery styles is shown to lie strictly between 0.11 and 0.13. Archaeologists reconstructing Petrie sequence dating from recognition costs would cite this bound to calibrate model predictions against serial data. The proof reduces the gap to phi minus three halves via its defining equality and closes the interval with linear arithmetic on the golden-ratio bounds.
Claim. $0.11 < J(φ) < 0.13$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost function and $φ$ is the golden ratio.
background
The module models style popularity as popularity(s) = 1 / (1 + Jcost(s)), where s is scaled time. The adjacency gap is the J-cost evaluated at phi, defined as Cost.Jcost phi and shown equal to phi - 3/2 by the equality theorem. This gap measures the separation between neighboring J-cost minima on the one-dimensional design graph.
proof idea
The proof rewrites adjacencyGap using the equality theorem to obtain phi - 3/2. It then introduces the two phi-bound lemmas. Linear arithmetic is applied to both resulting inequalities to establish the open interval (0.11, 0.13).
why it matters
This result supplies the required numerical band for the master certificate potterySerialCert and is invoked directly in the one-statement theorem pottery_serial_one_statement. It quantifies the universal spacing J(phi) ≈ 0.118 that emerges from the self-similar fixed point phi in the Recognition framework, thereby linking the forcing chain to observable ceramic succession patterns.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.