love_achieves_ground_state
plain-language theorem explainer
The theorem establishes that the Love operator applied to any balanced extraction pair (σ, −σ) drives the system cost exactly to zero. Recognition Science researchers working on thermodynamic ethics cite this when showing how love resolves extraction waste. The proof is a one-line wrapper that unfolds the pair cost definition and simplifies via the identity cosh(0) = 1.
Claim. For any real number $σ$, the post-Love cost of the balanced extraction pair $(σ, -σ)$ is zero: $2(ℝ.cosh((σ + (-σ))/2) - 1) = 0$.
background
In the Ethics.ThermodynamicInstabilityOfExtraction module the pairCostAfterLove definition computes post-averaging system cost as 2*(cosh((σ₁ + σ₂)/2) - 1). This rests on the J-cost from MultiplicativeRecognizerL4.cost and ObserverForcing.cost, both of which return non-negative values tied to the Recognition Composition Law. The balanced predicate from LedgerForcing.balanced requires that the underlying ledger events form a balanced list, ensuring the pair (σ, -σ) is admissible for the extraction model.
proof idea
The proof unfolds pairCostAfterLove, substitutes the zero average of σ and -σ into the cosh argument, and applies simp with Real.cosh_zero to obtain the identity 2*(1 - 1) = 0.
why it matters
This theorem is invoked directly by love_eliminates_all_waste to separate the strictly positive pre-Love pairSystemCost (for σ ≠ 0) from the zero post-Love cost, completing the claim that love eliminates all thermodynamic waste. It supplies the ground-state step in the ethics chain, aligning with the forcing chain's T5 J-uniqueness and the minimal-cost fixed point at zero.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.