extraction_cost_strict_minimum
plain-language theorem explainer
The extraction system cost function attains its strict global minimum at zero extraction. Researchers modeling thermodynamic bounds on recognition processes would cite this to establish that any nonzero extraction produces a positive surcharge. The proof is a term-mode one-liner that rewrites the zero case via the equivalence lemma and applies the surcharge creation result directly.
Claim. Let $C$ denote the extraction system cost function. Then $C(0) < C(σ)$ for every real number $σ ≠ 0$.
background
In Recognition Science the J-cost satisfies the Recognition Composition Law J(xy) + J(x/y) = 2J(x)J(y) + 2J(x) + 2J(y), which is equivalent to the cosh-add identity CoshAddIdentity on the cost function. The extraction system cost is the cosh-based measure of deviation from equilibrium extraction, so that C(σ) = cosh(σ) - 1 in native units. This places the theorem inside the Ethics module on thermodynamic instability of extraction, which builds directly on the Cost.FunctionalEquation module.
proof idea
The proof is a term-mode one-liner. It rewrites C(0) = 0 by the mpr direction of extraction_cost_eq_zero_iff, then applies extraction_creates_surcharge σ h to obtain the strict inequality.
why it matters
The result confirms zero as the unique global minimum, completing the local argument that extraction is thermodynamically unstable. It sits downstream of the surcharge theorem and the zero-equivalence lemma, both of which rest on the RCL-derived cosh identity. The surrounding module section links the same identity to the d'Alembert sum, showing that the forcing chain (T5 J-uniqueness through T8 D=3) supplies the tools for the optimality claim. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.