`powerClass`

definition

show as: view math explainer →

module: IndisputableMonolith.Superhuman.Core
domain: Superhuman
line: 87 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Superhuman.Core on GitHub at line 87.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  84  deriving DecidableEq, Repr
  85
  86/-- Classification function: assigns each power to its epistemic class. -/
  87def powerClass : Power → PowerClass
  88  | .telepathy             => .DirectMechanism
  89  | .precognition          => .DirectMechanism
  90  | .empathy               => .DirectMechanism
  91  | .healing               => .DirectMechanism
  92  | .immortality           => .DirectMechanism
  93  | .astralProjection      => .DirectMechanism
  94  | .superIntelligence     => .Derivable
  95  | .enhancedSenses        => .Derivable
  96  | .soundControl          => .Derivable
  97  | .animalCommunication   => .Derivable
  98  | .mindInfluence         => .Derivable
  99  | .collectivePower       => .Derivable
 100  | .flight                => .NautilusClass
 101  | .invulnerability       => .NautilusClass
 102  | .superStrength         => .NautilusClass
 103  | .forceFields           => .NautilusClass
 104  | .energyProjection      => .NautilusClass
 105  | .transmutation         => .NautilusClass
 106  | .timePerception        => .Speculative
 107  | .superSpeed            => .Speculative
 108  | .invisibility          => .Speculative
 109  | .elementalControl      => .Speculative
 110  | .sizeManipulation      => .Speculative
 111  | .duplication           => .Constrained
 112  | .realityWarping        => .Constrained
 113  | .creationExNihilo      => .Constrained
 114  | .absoluteInvulnerability => .Constrained
 115
 116/-- A power is accessible if its class is not Constrained. -/
 117def Power.accessible (p : Power) : Bool := (powerClass p).accessible

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.