love_reduces_collective_jbar
plain-language theorem explainer
love_reduces_collective_jbar establishes that the love operator strictly lowers the average recognition cost J-bar of any lattice state when the strength parameter satisfies 0 < strength ≤ 1. Modelers of virtue effects in recognition lattices cite this to quantify cost reduction under love. The proof substitutes the explicit update rule from applyLove and reduces the resulting inequality via linear arithmetic using the positivity of the original J-bar.
Claim. Let $s$ be a lattice state with average cost $J(s) > 0$. For strength parameter $0 < σ ≤ 1$, the state $s'$ obtained by the love operator satisfies $J(s') < J(s)$.
background
The module VirtueLatticeEffect examines how each of the 14 DREAM virtues modifies the recognition lattice's average cost J-bar and spectral gap. Love is defined to reduce collective J-bar while increasing the spectral gap. LatticeState is the structure recording jbar, spectral_gap, energy together with their positivity proofs. The applyLove function updates jbar to s.jbar * (1 - strength/2) and spectral_gap to s.spectral_gap * (1 + strength), leaving energy unchanged. This result sits inside the broader Recognition Science framework where J-cost derives from the functional equation and the forcing chain.
proof idea
The proof first unfolds the definition of applyLove to expose the new J-bar value s.jbar multiplied by (1 - strength/2). It then applies nlinarith to the hypothesis that the original jbar is positive, which immediately yields the strict inequality for the scaled value when strength lies in (0,1].
why it matters
This theorem supplies the quantitative statement that love lowers collective J-bar, as announced in the module documentation on virtue effects. It forms part of the lattice transformation rules that connect ethical virtues to recognition costs in the Recognition Science model. No downstream uses are recorded yet; the result closes the local claim for the love operator within the ethics module.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.