inductive
definition
PowerClass
show as:
view math explainer →
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
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