courage
plain-language theorem explainer
Courage is defined as the virtue signature carrying the name Courage, unit loading on family index 2 and zero elsewhere, together with zero sigma effect. Researchers working on the ethical layer of Recognition Science cite this definition when they verify that the fourteen DREAM virtues form a basis of distinct signatures. The definition is a direct structure instantiation with no computational content.
Claim. Let $V$ be the type whose elements are triples consisting of a string name, a function from the four families (indexed by Fin 4) to real numbers, and a real number measuring the sigma effect. The courage signature is the element $c$ of $V$ whose name is ``Courage'', whose family-loading function equals 1 at index 2 and 0 at all other indices, and whose sigma effect equals 0.
background
The module defines Born-profile signatures for the DREAM virtues inside Recognition Science. Each virtue receives a characteristic pattern of loadings across four families together with a sigma effect that records its net contribution to global imbalance. The VirtueSignature structure packages exactly these three fields: a String name, a Fin 4 → ℝ loading map, and an ℝ sigma effect. The upstream structure definition supplies the type that courage must inhabit.
proof idea
The declaration is a direct structure constructor that supplies literal values for the three fields of VirtueSignature.
why it matters
This definition supplies one of the fourteen concrete base elements required by the downstream theorems each_virtue_distinct_signature and love_has_unique_sigma_effect. Those results establish that the DREAM virtues are pairwise distinct in their loading patterns and that only love carries a nonzero sigma effect. The construction therefore closes the concrete data needed for the ethical extension of the Recognition framework.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.