extraction_cost_nonneg
plain-language theorem explainer
The extraction system cost, defined as the sum of J-costs for agents at states e^σ and e^{-σ}, is nonnegative for every real σ. Researchers modeling recognition events through thermodynamic costs would cite this to bound extraction penalties. The proof rewrites via the cosh identity and reduces the inequality 1 ≤ cosh σ to case analysis plus linear arithmetic.
Claim. For every real number $σ$, $0 ≤ J(e^σ) + J(e^{-σ})$, where $J(x) = (x + x^{-1})/2 - 1$ is the recognition cost function.
background
In this module the extractionSystemCost σ is the total J-cost of a two-agent system in which one agent has extracted parameter σ from the other, placing the agents at states e^σ and e^{-σ}. The J-cost itself is the Recognition Science cost function J(x) = cosh(log x) - 1, which is nonnegative by construction from the multiplicative recognizer. The local setting is the thermodynamic analysis of extraction, showing that any nonzero extraction produces a positive action surcharge.
proof idea
The tactic proof first rewrites the goal with the extraction_cost_eq_cosh lemma, converting the claim into 0 ≤ 2(cosh σ - 1). It then proves the auxiliary inequality 1 ≤ cosh σ by case split on σ = 0 (using cosh_zero) versus σ ≠ 0 (using one_lt_cosh). Linear arithmetic finishes the argument.
why it matters
This result is invoked directly by extraction_cost_minimum_at_zero to establish that cost zero is achieved only at σ = 0. It supplies the nonnegativity step in the larger claim that zero-sum log-exchanges are strictly negative-sum in J-cost. The theorem therefore anchors the thermodynamic instability argument and aligns with the J-uniqueness property (T5) and the nonnegativity of all recognition costs.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.