constrained_count_eq_4
plain-language theorem explainer
The RS power taxonomy contains exactly four constrained powers. Workers on the σ-Resolution Superhero Thesis cite this when bounding forbidden capabilities. Native decision on the explicit enumeration of allPowers yields the equality after filtering out accessible entries.
Claim. Let $P$ be the complete list of 27 canonical superhuman powers. Then the cardinality of the sublist consisting of those $p$ for which $p$ is not accessible equals 4.
background
The Superhuman.Core module defines the Power inductive type enumerating 27 canonical powers drawn from mythology, comics, and folklore. It partitions them into five epistemic classes A-E via the powerClass function, with Class A containing direct RS mechanisms such as telepathy and healing. The predicate Power.accessible identifies powers possessing an RS path, and allPowers supplies the complete list used for counting.
proof idea
The proof is a one-line wrapper applying native_decide to evaluate the length of the filtered list on the concrete definition of allPowers.
why it matters
This theorem closes the count of constrained powers in the taxonomy, complementing accessible_count_eq_23 and powerCount_eq_27. It aligns with the Recognition Science framework by distinguishing direct mechanisms from constrained ones, consistent with the eight-tick octave and phi-ladder structures elsewhere in the monolith.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.