FreeWillStance
plain-language theorem explainer
FreeWillStance enumerates five canonical positions on free will corresponding to configDim equal to 5. Researchers classifying deterministic interpretations in the Recognition Science J-cost setting would cite this enumeration when mapping stances to compatibilism versus libertarianism. The definition is a direct inductive construction with automatic derivation of Fintype and decidability instances.
Claim. Let $S$ be the inductive type whose constructors are hard determinism, hard incompatibilism, classical compatibilism, libertarian agent-causal, and libertarian event-causal. The type $S$ carries decidable equality and forms a finite type.
background
The module defines five canonical stances on free will as the content of configDim D = 5. These stances are hard determinism, hard incompatibilism, classical compatibilism, libertarian agent-causal, and libertarian event-causal. Recognition Science locates compatibilism in recognition-symmetric J-cost degeneracy. The local theoretical setting is the philosophy depth of the framework, with zero axioms and zero sorrys.
proof idea
The declaration is a direct inductive definition of the five constructors. The instances for DecidableEq, Repr, BEq, and Fintype are obtained by automatic derivation.
why it matters
This enumeration supplies the type whose cardinality is certified equal to 5 by the downstream FreeWillCategoriesCert structure and the freeWillStance_count theorem. It occupies the configDim = 5 slot and supports the framework claim that compatibilism follows from J-cost symmetry. The stances sit at the interpretive level relative to the T0-T8 forcing chain and the eight-tick octave.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.