extraction_cost_minimum_at_zero
plain-language theorem explainer
The result shows that the extraction system cost for two agents reaches its global minimum of zero exactly when the extraction parameter σ is zero. Researchers modeling thermodynamic penalties in recognition-based agent systems would cite this to confirm baseline stability. The proof is a direct term-mode reduction that rewrites the zero case via the equivalence lemma and applies nonnegativity.
Claim. Let $C(σ)$ denote the extraction system cost of two agents with extraction parameter $σ$, defined as $J(e^σ) + J(e^{-σ})$ where $J$ is the J-cost function. Then $C(0) ≤ C(σ)$ for all real $σ$.
background
The module examines thermodynamic instability of extraction between two agents in a recognition framework. The extraction system cost is defined as the sum of J-costs for agents positioned at $e^σ$ and $e^{-σ}$, which equals $2( cosh(σ) - 1 )$ by the cost identity. The J-cost satisfies $J(x) = (x + x^{-1})/2 - 1$, equivalent to $cosh(log x) - 1$ from the Recognition Composition Law.
proof idea
One-line wrapper that applies the zero-equivalence lemma to rewrite the base case as zero, then invokes the nonnegativity theorem to conclude the inequality.
why it matters
This anchors the module's instability claim by establishing zero extraction as the global minimum cost point. It builds directly on the cost-equivalence and nonnegativity results, which rest on the hyperbolic-cosine identity. In the broader framework it illustrates how J-uniqueness and the self-similar fixed point force positive costs for any deviation, consistent with the eight-tick octave structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.