HasFreeChoice
Free choice is formalized as the existence of at least two positive paths each attaining zero J-cost. Researchers in foundations of physics cite this predicate when deriving compatibilist free will from sigma conservation in the Recognition framework. The definition is a direct conjunction of a length condition and a universal zero-cost predicate on the supplied list.
claimA list of paths $p$ satisfies the free-choice property when its length is at least 2, every entry $r$ is positive, and $J(r)=0$ for each such $r$.
background
In Recognition Science the J-cost function quantifies recognition cost of a configuration or path, vanishing at equilibrium (J(1)=0) and symmetric under inversion. The module treats free will as degeneracy in this cost landscape: multiple admissible paths share the global minimum. Upstream results supply the actualization operator A that selects the argmin of J over possible configurations and the active-edge count A per fundamental tick.
proof idea
The definition is a direct conjunction of the length predicate and the universal zero-cost condition. No lemmas or tactics are invoked; it is an immediate predicate definition.
why it matters in Recognition Science
This predicate is the core building block for FreeWillCert, which certifies the five-position compatibilist structure, and for the trivial free-choice theorem on the list [1,1]. It realizes the module's structural derivation step that equates free choice with J-cost multiplicity greater than one under sigma conservation. The construction sits inside the T5-T8 forcing chain through the underlying J function and the eight-tick octave.
scope and limits
- Does not claim that free choice violates sigma conservation.
- Does not specify the physical realization of the listed paths.
- Does not compute the cardinality of zero-cost paths for concrete systems.
- Does not distinguish libertarian from compatibilist interpretations.
Lean usage
theorem has_free_choice_example : HasFreeChoice [1, 1] := trivial_free_choiceformal statement (Lean)
54def HasFreeChoice (paths : List ℝ) : Prop :=
proof body
Definition body.
55 paths.length ≥ 2 ∧ ∀ r ∈ paths, r > 0 ∧ Jcost r = 0
56
57/-- A trivial free-choice instance: {1, 1}. -/