Jcost_nonneg_of_pos
plain-language theorem explainer
J-cost is non-negative for every positive real argument, providing the lower bound that keeps derived popularity functions in [0,1] for models of ceramic-style succession. Archaeologists reconstructing Petrie curves or Recognition Science researchers verifying J-function properties would cite the result when bounding recognition costs. The proof unfolds the definition then reduces the claim to the AM-GM inequality s + s inverse at least 2 via expansion of (s-1) squared and nlinarith.
Claim. For every real number $s > 0$, the J-cost satisfies $J(s) := (s + s^{-1})/2 - 1$ and $J(s) >= 0$.
background
The module derives pottery style popularity from J-cost trajectories on a one-dimensional design graph. J-cost is the recognition cost J(s) = (s + s^{-1})/2 - 1, zero at s=1 and positive elsewhere, while popularity is defined as 1/(1 + Jcost(s/tau)) for style half-life tau. Neighboring styles are separated by J(phi) approx 0.118, reproducing the empirical Petrie curve shape. This non-negativity result is the prerequisite inequality for all subsequent popularity bounds in the file.
proof idea
The tactic proof unfolds Cost.Jcost, obtains 0 < s inverse from inv_pos, proves s + s inverse >= 2 by expanding (s-1)^2 >=0 with ring and invoking nlinarith on positivity facts, then closes with linarith.
why it matters
The theorem is invoked directly by popularity_nonneg, popularity_pos, and popularity_le_one in the same module. It supplies the elementary inequality step required to derive Petrie curves as J-cost trajectories, consistent with J-uniqueness in the forcing chain. The result confirms that J-cost functions as a valid non-negative defect measure on the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.