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

Power

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)

  51inductive Power where
  52  -- Class A: Direct RS Mechanism
  53  | telepathy
  54  | precognition
  55  | empathy
  56  | healing
  57  | immortality
  58  | astralProjection
  59  -- Class B: Derivable from RS
  60  | superIntelligence
  61  | enhancedSenses
  62  | soundControl
  63  | animalCommunication
  64  | mindInfluence
  65  | collectivePower
  66  -- Class C: Nautilus-Class Technology
  67  | flight
  68  | invulnerability
  69  | superStrength
  70  | forceFields
  71  | energyProjection
  72  | transmutation
  73  -- Class D: Speculative but Consistent
  74  | timePerception
  75  | superSpeed
  76  | invisibility
  77  | elementalControl
  78  | sizeManipulation
  79  -- Class E: Constrained or Forbidden
  80  | duplication
  81  | realityWarping
  82  | creationExNihilo
  83  | absoluteInvulnerability
  84  deriving DecidableEq, Repr
  85
  86/-- Classification function: assigns each power to its epistemic class. -/

used by (31)

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

… and 1 more

depends on (17)

Lean names referenced from this declaration's body.