applyCourage
plain-language theorem explainer
The predicate for courage application holds precisely when a lattice state's spectral gap exceeds a supplied positive gradient. Researchers modeling ethical effects on recognition lattices cite this to connect virtues to field gradients in the phi-ladder. The definition is a direct one-line inequality between the state's spectral gap and the input gradient value.
Claim. Let $s$ be a lattice state with positive spectral gap and let $g > 0$ be a gradient magnitude. Courage applies if the spectral gap of $s$ is strictly greater than $g$.
background
The Virtue Lattice Effect module studies how each of the 14 DREAM virtues alters average J-cost (jbar) and spectral gap on the recognition lattice. LatticeState is the structure recording jbar (average recognition cost), spectral_gap (minimum cost separation from vacuum), and energy, each required positive by construction. The gradient collects directional derivatives of a scalar field. The upstream spectral gap theorem states that for all nonzero integers n, J of the nth phi-ladder rung is at least the mass gap Delta.
proof idea
This is a one-line definition that equates the courage predicate directly to the inequality between the lattice state's spectral gap and the supplied gradient.
why it matters
This supplies the predicate used by the downstream theorem courage_enables_high_gradient_action, which concludes the predicate from the inequality. It links the Yang-Mills mass gap result to ethical modeling by permitting high-gradient actions only when the gap is large enough. In the Recognition Science setting the definition ties virtues to spectral properties of the phi-ladder and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.