freeWillStance_count
plain-language theorem explainer
The declaration establishes that the inductive type of free will stances has cardinality exactly five, matching the five-dimensional configuration space in Recognition Science. Philosophers and physicists studying determinism and agency would cite this finite enumeration when linking configDim to philosophical categories. The proof is a one-line decision procedure that exhausts the Fintype instance on the inductive type.
Claim. The cardinality of the free will stances type is five: $|FreeWillStance| = 5$, where $FreeWillStance$ enumerates hard determinism, hard incompatibilism, classical compatibilism, libertarian agent-causal, and libertarian event-causal.
background
The module identifies five canonical stances on free will with configDim D = 5. These stances are hard determinism, hard incompatibilism, classical compatibilism, libertarian agent-causal, and libertarian event-causal. Recognition Science favors compatibilism arising from recognition-symmetric J-cost degeneracy. The upstream inductive definition lists precisely these five constructors and equips the type with DecidableEq, Repr, BEq, and Fintype instances.
proof idea
The proof is a one-line wrapper that invokes the decide tactic. This tactic uses the derived Fintype instance on the finite inductive type to compute the cardinality directly.
why it matters
The count is supplied directly to freeWillCategoriesCert to certify the five stances. It anchors the philosophical module to the configDim = 5 convention, where the five positions parametrize free will categories in Recognition Science. The result closes the enumeration step without introducing new hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.