`classB_count`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Superhuman.Core on GitHub at line 142.

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

 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
 169  | .duplication             => some .zConservation
 170  | .realityWarping          => some .jUniqueness
 171  | .creationExNihilo        => some .costOfNothing
 172  | .absoluteInvulnerability => some .boundaryDissolution

papers checked against this theorem

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