FreeWillPosition
The inductive type enumerates the five standard positions on free will as a configuration space of dimension five inside the Recognition Science sigma-conservation model. A researcher deriving free choice from J-cost degeneracy would cite the enumeration to fix the discrete options available under equilibrium multiplicity. The definition proceeds by direct listing of the five constructors followed by automatic derivation of Fintype for cardinality proofs.
claimLet $P$ be the finite set of free-will positions. Then $P = $ {hard determinism, soft determinism, compatibilism, libertarianism, hard indeterminism} with $|P| = 5$.
background
Recognition Science treats free will as arising from genuine degeneracy in the J-cost landscape under sigma conservation. A decision is free precisely when two or more admissible paths achieve the minimal cost J = 0; it is determined when exactly one path meets that threshold. The module therefore introduces five interpretive positions that differ only in how they read the existence or uniqueness of such zero-cost paths.
proof idea
The declaration is the direct inductive definition of the five constructors with automatic derivation of DecidableEq, Repr, BEq and Fintype; no lemmas are applied.
why it matters in Recognition Science
This supplies the configuration space whose cardinality is asserted by the downstream structure FreeWillCert (five_positions : Fintype.card FreeWillPosition = 5 together with the equilibrium Jcost 1 = 0 and symmetry Jcost r = Jcost r^{-1}). It is also used by the theorem freeWillPositionCount. In the framework it realizes the D = 5 dimension for the five compatibilist readings of J-cost degeneracy, closing the structural derivation of free choice from sigma conservation.
scope and limits
- Does not assert which of the five positions is physically correct.
- Does not derive the J-cost equalities or the sigma-conservation law.
- Does not connect the positions to specific values of phi or other constants.
- Does not address measurement or collapse mechanisms outside the J-cost model.
Lean usage
theorem freeWillPositionCount : Fintype.card FreeWillPosition = 5 := by decideformal statement (Lean)
36inductive FreeWillPosition where
37 | hardDeterminism | softDeterminism | compatibilism | libertarianism | hardIndeterminism
38 deriving DecidableEq, Repr, BEq, Fintype
39