`classA_count`

proved

show as: view math explainer →

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

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Superhuman.Core on GitHub at line 138.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 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
 162  | jUniqueness         -- J is uniquely forced; cannot override cost structure
 163  | costOfNothing       -- J(0⁺) → ∞; cannot create from nothing
 164  | boundaryDissolution -- Dissolution always thermodynamically available
 165  deriving DecidableEq, Repr
 166
 167/-- Each constrained power has a specific conservation-law reason. -/
 168def constraintReason : Power → Option ConstraintReason

papers checked against this theorem

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