FreeWillCert
plain-language theorem explainer
FreeWillCert packages the five properties that certify compatibilist free will under sigma conservation in Recognition Science: exactly five philosophical positions, J-cost zero at equilibrium, inversion symmetry of J-cost, strict positivity away from unity, and free choice for duplicate unit paths. RS theorists and philosophers of physics cite the structure to formalize how degeneracy at J = 0 supplies optionality while preserving the conservation law. The declaration is a pure structure definition that bundles these properties with no proof,
Claim. A structure is defined by the conjunction of: the set of free-will positions has cardinality 5; $J(1)=0$; $J(r)=J(r^{-1})$ for every $r>0$; $J(r)>0$ whenever $r>0$ and $r≠1$; and free choice holds for the list of paths $[1,1]$, where free choice means at least two positive paths each attain zero J-cost.
background
The J-cost function assigns a non-negative recognition cost to each admissible path ratio r, with the defining properties that J(1)=0 at equilibrium and J(r)=J(r^{-1}) by symmetry. FreeWillPosition is the inductive enumeration of the five stances (hard determinism, soft determinism, compatibilism, libertarianism, hard indeterminism) whose cardinality is asserted to be 5. HasFreeChoice is the predicate that a list of paths admits genuine optionality precisely when its length is at least 2 and every entry r satisfies r>0 together with J(r)=0.
proof idea
The declaration is a structure definition whose five fields are stated directly; no tactics or lemmas are invoked because the object is an axiomatic bundle rather than a derived theorem. The cardinality field refers to the Fintype instance on FreeWillPosition, the equilibrium field imports the upstream result Jcost 1 = 0, and the free-choice field instantiates HasFreeChoice on the concrete list [1,1].
why it matters
FreeWillCert supplies the formal certificate that feeds the concrete instance freeWillCert, which in turn assembles the module's claim that free will arises from tied minima in the J-cost landscape while sigma conservation remains intact. The structure realizes the five-position count as configDim D=5 and aligns with the compatibilist reading given in the module documentation, where determinism is the substrate and optionality emerges from degeneracy at J=0. It touches the broader Recognition Science chain by grounding philosophical consequences in J-uniqueness without deriving them from the T0-T8 forcing sequence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.