courage_enables_high_gradient_action
plain-language theorem explainer
The theorem asserts that a lattice state whose spectral gap exceeds a positive gradient satisfies the courage application predicate by definition. Recognition Science modelers of virtue effects on recognition lattices cite this when linking courage to high-gradient regimes. The proof is a direct one-line reduction to the supplied hypothesis via the definition of applyCourage.
Claim. Let $s$ be a lattice state with spectral gap $Δ_s > 0$ and let $g > 0$ be a gradient. If $Δ_s > g$, then the courage-enabled high-gradient action condition holds, which is exactly $Δ_s > g$.
background
The Virtue Lattice Effect module studies how each virtue alters average J-cost (J̄) and spectral gap on the recognition lattice. LatticeState records jbar, spectral_gap and energy with positivity axioms. applyCourage is the predicate that holds precisely when the state's spectral gap exceeds the supplied positive gradient. This rests on the spectral gap theorem establishing that every non-vacuum φ-ladder rung satisfies J(φⁿ) ≥ J(φ) > 0.
proof idea
The proof is a one-line wrapper. It matches the hypothesis h directly to the body of applyCourage, which is defined as s.spectral_gap > gradient under the assumption gradient > 0.
why it matters
The result supplies the courage clause in the Virtue Lattice Effect description, showing how courage permits action in regions where gradient is positive yet remains below the spectral gap. It draws on the Yang-Mills spectral gap theorem and supports later modeling of J-bar transformations under the full set of virtues. No downstream theorems yet reference it, leaving integration with the broader lattice open.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.