freeWillPositionCount
The theorem establishes that the inductive type enumerating five compatibilist positions on free will has cardinality exactly five. A researcher working on sigma-conservation mechanisms in Recognition Science cites this when counting admissible decision degeneracies at J = 0. The proof is a one-line decision procedure that inspects the finite type derived from the five explicit constructors.
claimLet $P$ be the set of five compatibilist positions on free will (hard determinism, soft determinism, compatibilism, libertarianism, hard indeterminism). Then $|P| = 5$.
background
The module derives free will as degeneracy in the J-cost landscape under sigma conservation. A free decision occurs when multiple paths achieve J-cost zero; determinism occurs when exactly one path does. The five positions correspond to the possible configurations of this degeneracy, matching configDim D = 5. The upstream result is the inductive definition FreeWillPosition whose five constructors are hardDeterminism, softDeterminism, compatibilism, libertarianism, and hardIndeterminism, each deriving DecidableEq, Repr, BEq, and Fintype.
proof idea
The proof is a one-line term that applies the decide tactic to the goal Fintype.card FreeWillPosition = 5. Because FreeWillPosition derives Fintype and lists exactly five constructors, the tactic computes the cardinality by enumeration and closes the equality.
why it matters in Recognition Science
This supplies the five_positions component of the FreeWillCert definition, completing the structural derivation of free will from J-cost degeneracy. It realizes the module claim that five compatibilist positions equal configDim D = 5 inside the D8 sigma-conservation mechanism. The result sits between the FreeWillPosition inductive and the FreeWillCert record that packages equilibrium, symmetry, constraint, and free-choice existence.
scope and limits
- Does not derive the five positions from the Recognition Composition Law.
- Does not select which position is realized for a given physical system.
- Does not address measurement or observer selection in the underlying physics.
- Does not prove existence of free will; only counts the enumerated positions.
Lean usage
def cert : FreeWillCert := { five_positions := freeWillPositionCount, equilibrium := equilibrium_is_zero, symmetry := choice_symmetric, constraint := constrained_choice, free_choice_exists := trivial_free_choice }formal statement (Lean)
40theorem freeWillPositionCount : Fintype.card FreeWillPosition = 5 := by decide
proof body
Term-mode proof.
41
42/-- Free choice: degeneracy at J = 0. -/