classE_count
plain-language theorem explainer
Exactly four of the twenty-seven canonical powers fall into the Constrained epistemic class. Researchers working on the σ-Resolution Superhero Thesis cite this count when separating accessible mechanisms from the four forbidden ones. The proof evaluates the filtered length of the enumerated list via a native decision procedure.
Claim. Let $P$ be the set of 27 canonical powers and let $κ: P → {DirectMechanism, Derivable, NautilusClass, Speculative, Constrained}$ be the classification map. Then $|{p ∈ P | κ(p) = Constrained}| = 4$.
background
The Superhuman.Core module formalizes the σ-Resolution Superhero Thesis power taxonomy, partitioning 27 powers into five epistemic classes A–E by RS mechanism type. PowerClass is the inductive type with constructors DirectMechanism, Derivable, NautilusClass, Speculative, and Constrained. The function powerClass assigns each Power to its class. Sibling results include powerCount_eq_27 establishing the total at 27 and accessible_count_eq_23 showing 23 powers admit an RS path while the remaining 4 are constrained.
proof idea
The declaration is a one-line wrapper that applies native_decide to compute the length of the filter selecting powers where powerClass p equals Constrained on the concrete allPowers list.
why it matters
This theorem supplies the precise count for class E, completing the partition that underlies accessible_count_eq_23. It anchors the claim hygiene separating structural theorems from empirical hypotheses in the module. The result sits within the Recognition Science taxonomy effort but does not invoke the forcing chain T0–T8 or the Recognition Composition Law.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.