`classC_count`

proved

show as: view math explainer →

module: IndisputableMonolith.Superhuman.Core
domain: Superhuman
line: 146 · 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 146.

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

 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
 173  | _                        => none
 174
 175theorem constrained_has_reason (p : Power) (h : powerClass p = .Constrained) :
 176    (constraintReason p).isSome = true := by

papers checked against this theorem

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