constrained_choice
plain-language theorem explainer
Off-equilibrium ratios carry strictly positive J-cost. Recognition Science philosophers cite the result when separating cost-free equilibrium degeneracy from determined decisions. The proof is a one-line term that invokes the upstream positivity lemma for J-cost.
Claim. For every real number $r > 0$ with $r ≠ 1$, the recognition cost satisfies $0 < J(r)$.
background
The J-cost function quantifies recognition cost of a ratio, vanishing only at equilibrium. The upstream lemma Jcost_pos_of_ne_one rewrites Jcost via its squared form and shows strict positivity for $r > 0$, $r ≠ 1$ by positivity of squares and division. The module treats decisions as selections among J-cost minimizing paths under sigma-conservation, with free choice arising precisely when multiple paths attain the zero-cost minimum.
proof idea
Term-mode proof consisting of a direct application of the lemma Jcost_pos_of_ne_one from the Cost module.
why it matters
The theorem supplies the constraint field inside the freeWillCert definition, which assembles the five compatibilist positions. It supports the module claim that free will is compatible with sigma-conservation via J-cost degeneracy at equilibrium. The result aligns with J-uniqueness in the forcing chain and the interpretation of configDim D = 5.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.