inductive
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 160.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
157/-! ## Constraint Type -/
158
159/-- Why a power is constrained or forbidden. -/
160inductive ConstraintReason where
161 | zConservation -- Z is conserved; cannot duplicate patterns
162 | jUniqueness -- J is uniquely forced; cannot override cost structure
163 | costOfNothing -- J(0⁺) → ∞; cannot create from nothing
164 | boundaryDissolution -- Dissolution always thermodynamically available
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