FreeWillCategoriesCert
plain-language theorem explainer
The structure FreeWillCategoriesCert records that the inductive type FreeWillStance has cardinality exactly 5, matching the five canonical positions on free will that Recognition Science associates with configDim D = 5. Philosophers of physics working inside the Recognition framework cite it when mapping J-cost degeneracy to compatibilism. The definition is a direct structure whose single field packages the Fintype cardinality fact already derived from the five-constructor inductive type.
Claim. Let $S$ be the inductive type whose five constructors are hard determinism, hard incompatibilism, classical compatibilism, libertarian agent-causal, and libertarian event-causal. The structure FreeWillCategoriesCert consists of the single field asserting that the cardinality of $S$ equals 5.
background
The module FreeWillCategoriesFromConfigDim identifies five canonical stances on free will with configDim D = 5: hard determinism, hard incompatibilism, classical compatibilism, libertarian (agent-causal), and libertarian (event-causal). Recognition Science adopts the compatibilist stance on the grounds of recognition-symmetric J-cost degeneracy. The upstream FreeWillStance inductive type enumerates exactly these five positions and carries derived instances of DecidableEq, Repr, BEq and Fintype.
proof idea
This is a structure definition. Its single field directly records the already-established fact Fintype.card FreeWillStance = 5 that follows from the five-constructor inductive definition of FreeWillStance together with its derived Fintype instance.
why it matters
The definition supplies the certificate consumed by the downstream freeWillCategoriesCert witness. It occupies the D = 5 slot in the philosophy depth of Recognition Science, anchoring the framework's compatibilist position in J-cost symmetry. No new axioms are introduced; the cardinality is inherited from the inductive enumeration.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.