love_widens_gap
plain-language theorem explainer
Applying love with positive strength at most 1 strictly increases the spectral gap of a lattice state. Researchers modeling virtue transformations in recognition lattices cite this to quantify how love enhances gap size. The proof is a one-line wrapper that unfolds the applyLove definition and invokes linear arithmetic on the original gap positivity.
Claim. Let $s$ be a lattice state with positive spectral gap. For strength parameter $0 < r ≤ 1$, the spectral gap of the state obtained by applying love with strength $r$ is strictly larger than the spectral gap of $s$.
background
LatticeState is the structure recording a recognition lattice configuration via its average J-cost (jbar), spectral gap, and energy, each equipped with a positivity proof. The VirtueLatticeEffect module examines how each of the 14 DREAM virtues alters these quantities on the lattice. Love is defined to reduce jbar by the factor (1 - strength/2) while multiplying the spectral gap by (1 + strength) and leaving energy unchanged. The upstream spectral_gap result from YangMillsMassGap states that for every nonzero rung on the phi-ladder, Jcost is at least the mass gap, supplying the positivity used here.
proof idea
The proof is a one-line wrapper. It unfolds the definition of applyLove, which replaces the spectral gap field by its original value multiplied by (1 + strength), then applies nlinarith to the positivity hypothesis on the input state's gap to obtain the strict inequality.
why it matters
This result belongs to the VirtueLatticeEffect module that maps each virtue to a concrete transformation of J-bar and spectral gap. It directly instantiates the module's claim that love widens the gap, feeding the broader Recognition Science picture in which positive spectral gap (from the Yang-Mills unification) is a prerequisite for stable non-vacuum configurations. No downstream theorems yet consume it, leaving open the question of how the widened gap propagates through the forcing chain to observable constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.