ConstraintReason
plain-language theorem explainer
ConstraintReason enumerates the four conservation-law reasons that forbid specific superhuman powers in the Recognition Science taxonomy. Authors of the σ-Resolution Superhero Thesis cite it when assigning the four constrained cases out of 27 total powers. The declaration is a plain inductive enumeration whose constructors label the physical prohibitions without further proof.
Claim. Inductive type of constraint reasons: $zConservation$ (Z conserved; patterns cannot duplicate), $jUniqueness$ (J uniquely forced; cost structure cannot be overridden), $costOfNothing$ (J(0^+) diverges; creation from vacuum forbidden), $boundaryDissolution$ (dissolution always thermodynamically available).
background
Superhuman.Core formalizes the σ-Resolution Superhero Thesis power taxonomy with 27 powers split into five epistemic classes A-E. Four powers are labeled constrained. ConstraintReason supplies the labels for those cases. It rests on cost definitions: ObserverForcing.cost states the cost of any recognition event is its J-cost, while MultiplicativeRecognizerL4.cost gives the derived cost on positive ratios. PrimitiveDistinction supplies the underlying structural conditions.
proof idea
The declaration is an inductive definition introducing four constructors. No lemmas or tactics are invoked; the type is used directly by the downstream constraintReason function to tag specific powers.
why it matters
ConstraintReason supplies the labels consumed by constraintReason, which maps duplication to zConservation, realityWarping to jUniqueness, creationExNihilo to costOfNothing, and absoluteInvulnerability to boundaryDissolution. It completes the structural count of 4 constrained powers out of 27 and ties directly to J-uniqueness in the forcing chain. No open scaffolding remains.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.