extraction_creates_surcharge
plain-language theorem explainer
Any nonzero real extraction parameter produces a strictly positive system cost in the J-cost metric. Researchers modeling log-shifts as information exchanges cite the result to establish that balanced extractions remain thermodynamically costly. The argument substitutes the closed-form cost identity and invokes the elementary strict inequality cosh(σ) > 1.
Claim. For any real number $σ ≠ 0$, the extraction system cost $J(e^σ) + J(e^{-σ})$ satisfies $0 < 2(ℝ.cosh(σ) - 1)$.
background
The J-cost is the function $J(x) = (x + x^{-1})/2 - 1$, equivalently cosh(log x) - 1. The extraction system cost for parameter σ is defined as the sum of J-costs for the pair of agents located at exp(σ) and exp(-σ). An upstream identity theorem states that this sum equals exactly 2(cosh(σ) - 1). The present declaration belongs to the module examining thermodynamic consequences of extraction within the Recognition Science framework.
proof idea
The proof is a one-line wrapper that first rewrites the system cost via the upstream identity extraction_cost_eq_cosh, then applies the standard fact that cosh(σ) > 1 whenever σ ≠ 0, and finishes with linear arithmetic.
why it matters
The result is invoked directly by the equivalence theorem characterizing when extraction cost vanishes and by the strict-minimum theorem establishing σ = 0 as the global minimum. It supplies the key positivity step in the argument that extraction introduces a net action surcharge, consistent with the Recognition Composition Law and the interpretation of J-cost as a measure of thermodynamic cost.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.