theorem
proved
powerCount_eq_27
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Superhuman.Core on GitHub at line 129.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
126 .timePerception, .superSpeed, .invisibility, .elementalControl, .sizeManipulation,
127 .duplication, .realityWarping, .creationExNihilo, .absoluteInvulnerability]
128
129theorem powerCount_eq_27 : allPowers.length = 27 := by native_decide
130
131theorem accessible_count_eq_23 :
132 (allPowers.filter Power.accessible).length = 23 := by native_decide
133
134theorem constrained_count_eq_4 :
135 (allPowers.filter (fun p => !(Power.accessible p))).length = 4 := by native_decide
136
137/-- Class A has exactly 6 powers. -/
138theorem classA_count :
139 (allPowers.filter (fun p => powerClass p == .DirectMechanism)).length = 6 := by native_decide
140
141/-- Class B has exactly 6 powers. -/
142theorem classB_count :
143 (allPowers.filter (fun p => powerClass p == .Derivable)).length = 6 := by native_decide
144
145/-- Class C has exactly 6 powers. -/
146theorem classC_count :
147 (allPowers.filter (fun p => powerClass p == .NautilusClass)).length = 6 := by native_decide
148
149/-- Class D has exactly 5 powers. -/
150theorem classD_count :
151 (allPowers.filter (fun p => powerClass p == .Speculative)).length = 5 := by native_decide
152
153/-- Class E has exactly 4 powers. -/
154theorem classE_count :
155 (allPowers.filter (fun p => powerClass p == .Constrained)).length = 4 := by native_decide
156
157/-! ## Constraint Type -/
158
159/-- Why a power is constrained or forbidden. -/