module module moderate

`IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction`

This module defines the combined J-cost for an extraction system in which one agent extracts quantity σ from another, placing the agents at scale factors e^σ and e^{-σ}. It proves the resulting cost is nonnegative, strictly convex, and minimized only at σ = 0, establishing thermodynamic instability. Researchers working on Recognition Science ethics would cite these lemmas when arguing that extraction necessarily creates a positive surcharge. The module consists of direct definitions plus short algebraic derivations that invoke the J-functional,

claimThe extraction system cost is $J(e^σ) + J(e^{-σ})$, where $J(x) = (x + x^{-1})/2 - 1$. This quantity equals $2J(φ^σ) + 2J(φ^{-σ})$ for the self-similar fixed point φ and is strictly positive for all σ ≠ 0.

background

The module imports the J-cost definition and the Recognition Composition Law from IndisputableMonolith.Cost together with the T5 functional-equation lemmas from Cost.FunctionalEquation. In the Recognition Science setting the J-cost quantifies the recognition defect associated with a scale factor x on the phi-ladder; the combined cost for two agents at reciprocal positions therefore measures the total instability created by any nonzero extraction σ. The local theoretical context is the ethical application of these costs to show that extraction is thermodynamically forbidden.

proof idea

This is a definition module. It introduces extractionSystemCost as the sum of the two J-values, then applies the functional equation to obtain the cosh identity, non-negativity, strict convexity, and the unique minimum at zero extraction. All steps are one-line wrappers or direct algebraic reductions that cite the upstream T5 lemmas.

why it matters in Recognition Science

The module supplies the concrete cost model that supports the thermodynamic-instability claim in the ethics domain. It rests on T5 J-uniqueness and the eight-tick octave structure; its results feed the broader Recognition Science argument that any extraction process necessarily increases total defect and therefore violates the minimum-cost principle.

scope and limits

Does not treat extraction among three or more agents.
Does not incorporate time-dependent or stochastic extraction.
Does not derive numerical bounds on σ in physical units.
Does not address quantum or gravitational corrections to the cost.

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Cost module_import
IndisputableMonolith.Cost.FunctionalEquation module_import

declarations in this module (22)

def extractionSystemCost L70
theorem extraction_cost_eq_cosh L75
theorem extraction_cost_nonneg L89
theorem extraction_creates_surcharge L102
theorem extraction_cost_eq_zero_iff L108
theorem deriv_extraction_cost L118
theorem second_deriv_extraction_cost L127
theorem extraction_cost_strictly_convex L136
theorem extraction_unique_equilibrium L144
theorem extraction_cost_minimum_at_zero L154
theorem extraction_cost_strict_minimum L161
theorem dAlembert_cosh_sum L180
theorem cosh_sum_via_dAlembert L192
def pairSystemCost L211
def pairCostAfterLove L215
theorem love_jensen_inequality L220
theorem love_jensen_strict L234
theorem love_achieves_ground_state L246
theorem love_eliminates_all_waste L252
theorem restoring_force_positive L270
theorem restoring_force_negative L277
theorem force_always_toward_balance L286