constraintReason
plain-language theorem explainer
constraintReason maps each of the four constrained powers to its specific conservation-law reason. Researchers classifying superhuman capabilities under the σ-Resolution thesis cite this mapping to identify forbidden powers by mechanism type. The definition is given by exhaustive pattern matching on the Power inductive type, returning the matching ConstraintReason variant or none.
Claim. Let $P$ be the inductive type of the 27 canonical superhuman powers and $R$ the inductive type of conservation reasons. The function $f : P → Option(R)$ satisfies $f(duplication) = some(zConservation)$, $f(realityWarping) = some(jUniqueness)$, $f(creationExNihilo) = some(costOfNothing)$, $f(absoluteInvulnerability) = some(boundaryDissolution)$, and returns none for all other powers in $P$.
background
The module Superhuman.Core formalizes the σ-Resolution Superhero Thesis power taxonomy, classifying 27 powers into five epistemic classes A–E by RS mechanism type. Power enumerates the 27 canonical superhuman powers drawn from mythology, comics, and folklore. ConstraintReason enumerates the four reasons why certain powers are constrained: zConservation (Z is conserved; cannot duplicate patterns), jUniqueness (J is uniquely forced; cannot override cost structure), costOfNothing (J(0⁺) → ∞; cannot create from nothing), and boundaryDissolution (Dissolution always thermodynamically available).
proof idea
The definition is implemented by exhaustive pattern matching on the Power constructors. It returns the appropriate ConstraintReason for the four constrained powers and none for the remaining cases. No lemmas are applied; it is a direct case definition.
why it matters
This definition supports the theorem constrained_has_reason, which proves that every power classified as Constrained has a non-none reason. It fills in the structural part of the power taxonomy in the Superhuman.Core module, linking to the Recognition Science framework through the conservation laws tied to J-uniqueness and Z conservation. It touches on the classification of the four constrained powers out of 27.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.