love
plain-language theorem explainer
The definition instantiates the Love virtue signature with name Love, family loadings (1,0,0,0) across the four families, and sigma effect -1. Ethics researchers analyzing DREAM virtues as generators of imbalance reduction cite this when modeling how only Love alters global sigma. The construction is a direct record definition with explicit field values.
Claim. The Love virtue signature is the structure with name ``Love'', family loadings $f: Fin 4 → ℝ$ where $f(0)=1$ and $f(i)=0$ otherwise, and sigma effect $-1$.
background
The module models each DREAM virtue by a Born-profile signature: a name, a loading vector in the four families, and a real sigma effect. VirtueSignature is the record type carrying these three fields. Upstream, sigma denotes the charge from AbileneParadox: the signed gap between an agent's private preference and public vote. The module doc states that Love is the sole virtue whose sigma effect is nonzero, thereby providing the only direct mechanism for changing global imbalance.
proof idea
This is a direct definition that builds the VirtueSignature record by supplying the three fields explicitly: the string name, the piecewise family loading function, and the constant sigma effect -1. No lemmas or tactics are invoked.
why it matters
The definition supplies the concrete Love instance required by downstream results such as love_has_unique_sigma_effect (Love is the only nonzero sigma effect) and love_reduces_sigma (its effect is negative). These feed the claim that virtues act as ethical generators in the L3 scope. Within Recognition Science the sigma effect links directly to the imbalance measure that appears in the forcing chain and equilibration arguments.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.