def
definition
constraintReason
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.Superhuman.Core on GitHub at line 168.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
165 deriving DecidableEq, Repr
166
167/-- Each constrained power has a specific conservation-law reason. -/
168def constraintReason : Power → Option ConstraintReason
169 | .duplication => some .zConservation
170 | .realityWarping => some .jUniqueness
171 | .creationExNihilo => some .costOfNothing
172 | .absoluteInvulnerability => some .boundaryDissolution
173 | _ => none
174
175theorem constrained_has_reason (p : Power) (h : powerClass p = .Constrained) :
176 (constraintReason p).isSome = true := by
177 cases p <;> simp_all [powerClass, constraintReason]
178
179end IndisputableMonolith.Superhuman