classD_count
plain-language theorem explainer
The theorem establishes that exactly five of the twenty-seven canonical powers belong to the Speculative epistemic class. Researchers formalizing the σ-Resolution Superhero Thesis would cite this cardinality when completing the partition of the power taxonomy into five tiers. The proof is a one-line native decision procedure that evaluates the filter length on the enumerated list.
Claim. Let $P$ be the complete list of twenty-seven powers and let $κ: P → {A,B,C,D,E}$ be the classification map sending each power to its epistemic tier. Then $|{p ∈ P | κ(p) = D}| = 5$.
background
The Superhuman Core module formalizes the σ-Resolution Superhero Thesis as an explicit enumeration of twenty-seven powers partitioned into five epistemic classes by Recognition Science mechanism type. The classification map assigns each power to one of DirectMechanism, Derivable, NautilusClass, Speculative, or Constrained. Upstream results supply the concrete list of all powers and the definition of the classification function; a related construction gives the edge count of the D-cube as $D × 2^{D-1}$.
proof idea
The proof is a one-line wrapper that applies native_decide to compute the length of the filtered list whose classification equals Speculative.
why it matters
This cardinality supplies one of the five class counts required to verify the exhaustive taxonomy of twenty-seven powers. It forms part of the structural theorems derived from Recognition Science axioms and completes the partition into the five tiers. The parent result is the claim that the taxonomy contains exactly twenty-seven entries with twenty-three accessible via RS paths.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.