`classE_count`

proved

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Superhuman.Core on GitHub at line 154.

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

 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
 177  cases p <;> simp_all [powerClass, constraintReason]
 178
 179end IndisputableMonolith.Superhuman

papers checked against this theorem

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