pith. machine review for the scientific record. sign in
inductive

PowerClass

definition
show as:
view math explainer →
module
IndisputableMonolith.Superhuman.Core
domain
Superhuman
line
32 · github
papers citing
none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Superhuman.Core on GitHub at line 32.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  29
  30/-- The five epistemic classes for superhuman powers.
  31    Each class has a different relationship to proved RS structure. -/
  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. -/
  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