extraction_unique_equilibrium
plain-language theorem explainer
The theorem establishes that the derivative of the extraction system cost vanishes only at zero extraction level. Researchers modeling thermodynamic costs in recognition systems would cite this to confirm equilibrium uniqueness. The proof reduces the derivative to twice the hyperbolic sine via the cost identity and invokes the strict monotonicity of sinh.
Claim. Let $C(σ)$ denote the extraction system cost. Then $C'(σ) = 0$ if and only if $σ = 0$.
background
In the Recognition Science framework the J-cost measures recognition cost on positive ratios via the multiplicative functional equation. The extractionSystemCost is defined as the sum of J-costs for states at scales exp(σ) and exp(-σ), which equals 2(cosh(σ) − 1) by the extraction cost identity. This construction models the combined thermodynamic cost when one agent extracts from another in a two-agent multiplicative recognizer system.
proof idea
The proof first rewrites the derivative via the marginal cost theorem as 2 sinh(σ). It splits the biconditional with constructor. One direction assumes 2 sinh(σ) = 0, reduces to sinh(σ) = 0, and applies the strict monotonicity of sinh to obtain σ = 0. The converse substitutes σ = 0 and uses sinh(0) = 0.
why it matters
This theorem confirms the unique critical point of the extraction cost, which is required to show that nonzero extraction creates a positive surcharge and is thermodynamically unstable. It belongs to the Ethics module on instability of extraction and aligns with the J-uniqueness fixed point at unity in the forcing chain. No downstream uses are recorded yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.