module module high

`IndisputableMonolith.Ethics.ThermodynamicInstabilityOfExtraction`

This module defines the combined J-cost for a two-agent extraction system in Recognition Science, with one agent shifted to e^σ and the other to e^{-σ}. It would be cited when analyzing thermodynamic constraints on extraction within the ethics domain. The module assembles a sequence of lemmas on non-negativity, convexity, and equilibrium uniqueness derived from the functional equation.

claimLet $J(x) = (x + x^{-1})/2 - 1$. For extraction parameter σ the system cost is $J(e^σ) + J(e^{-σ})$, which is nonnegative, strictly convex, and minimized only at σ = 0.

background

The module sits in the Ethics domain and imports the Cost module (defining the J-cost) together with Cost.FunctionalEquation, whose doc-comment states it supplies lemmas for the T5 cost uniqueness proof. Extraction is modeled as an asymmetric shift that places the two agents at reciprocal exponential positions. The Recognition Science setting uses the J-cost as the unique solution to the Recognition Composition Law, with T5 establishing J-uniqueness and T6 forcing the self-similar fixed point phi.

proof idea

This is a definition module, no proofs. It opens with the extractionSystemCost definition, then applies algebraic identities from the FunctionalEquation module to obtain the cosh form, non-negativity, first and second derivatives, strict convexity, and the unique equilibrium at zero.

why it matters in Recognition Science

The module applies T5 J-uniqueness to an ethical setting, showing that extraction creates a positive surcharge that cannot be removed without reversing the shift. It supplies the formal substrate for downstream ethics results that link thermodynamic cost to instability, consistent with the eight-tick octave and D = 3 spatial structure of the forcing chain.

scope and limits

Does not treat extraction among more than two agents.
Does not assign numerical values to σ or to the resulting cost.
Does not derive ethical norms; only the cost function and its analytic properties.
Does not address time-dependent or stochastic extraction processes.

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