adjacencyGap_pos
plain-language theorem explainer
The J-cost gap between successive pottery styles equals phi minus 3/2 and is therefore positive. Researchers deriving Petrie sequence dating from recognition cost trajectories would cite this to guarantee separation of style minima on the design graph. The proof rewrites the gap via its defining equality and closes with the lower bound phi greater than 1.5 together with linear arithmetic.
Claim. $0 < J(phi)$ where $J(x) = (x + x^{-1})/2 - 1$, $phi = (1 + sqrt(5))/2$, and the gap is defined as the J-cost evaluated at $phi$.
background
In the Pottery Serial from J-Cost module, style popularity is modeled as $popularity(t) = 1 / (1 + Cost.Jcost(t/tau))$ with neighboring minima on the design graph separated by the adjacency gap. The gap is introduced as the definition Cost.Jcost phi, which the upstream equality reduces to phi - 3/2. The module situates this construction inside Petrie's 1899 sequence dating, treating each ceramic style as a J-cost minimum with a gap-45 frustration interval between peaks.
proof idea
The proof is a one-line wrapper. It rewrites adjacencyGap using the equality adjacencyGap_eq to obtain the expression phi - 3/2, then invokes the lemma phi_gt_onePointFive and finishes with linarith.
why it matters
This supplies the positivity field adjacency_gap_pos required by the downstream definition potterySerialCert, which assembles the full certificate for the Petrie curve shape. It closes the positivity step in the J-cost derivation of serial succession, consistent with the phi-ladder and the recognition composition law. The result sits inside Track I2 of the plan and inherits the lower bound on phi established in Constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.