pith. machine review for the scientific record. sign in
inductive definition def or abbrev

PowerClass

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  32inductive PowerClass where
  33  | DirectMechanism   -- Class A: Lean module with formalization exists
  34  | Derivable         -- Class B: follows from existing RS results
  35  | NautilusClass     -- Class C: requires localized J-cost minimization technology
  36  | Speculative       -- Class D: consistent with RS but needs theoretical extension
  37  | Constrained       -- Class E: forbidden or constrained by conservation laws
  38  deriving DecidableEq, Repr
  39
  40/-- Whether a power class represents an accessible (not forbidden) capability. -/
  41def PowerClass.accessible : PowerClass → Bool
  42  | .DirectMechanism => true
  43  | .Derivable       => true
  44  | .NautilusClass   => true
  45  | .Speculative     => true
  46  | .Constrained     => false
  47
  48/-! ## Power Enumeration -/
  49
  50/-- The 27 canonical superhuman powers from cross-cultural mythology, comics, and folklore. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (16)

Lean names referenced from this declaration's body.