`accessible_count_eq_23`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Superhuman.Core on GitHub at line 131.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

 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. -/
 160inductive ConstraintReason where
 161  | zConservation       -- Z is conserved; cannot duplicate patterns

papers checked against this theorem

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