IsStable
plain-language theorem explainer
A pre-state s with value v in the unit interval is stable exactly when its pre-cost vanishes. Researchers tracing the forcing chain from pre-logical costs to discrete logic cite this definition to locate boundary minima. The definition is a direct equality that expands the quadratic preCost expression to zero.
Claim. A pre-state $s$ with real value $v$ in $[0,1]$ is stable when $v(1-v)=0$.
background
PreState is the structure of a real number val together with the proof that it lies in the closed unit interval. The sibling definition preCost maps each such state to the quadratic val*(1-val), whose only zeros on the interval are the endpoints 0 and 1. The module sets the local theoretical setting as the pre-logical cost landscape on [0,1], where minima occur at the boundary states. Upstream definitions in LogicFromCost and DiscretenessForcing introduce the same zero-cost pattern for stability in their respective domains.
proof idea
This is the direct definition that sets IsStable s to the proposition preCost s = 0. No lemmas or tactics are applied; the body is the literal equality to the zero-cost condition.
why it matters
The definition supplies the base stability predicate that is unfolded in the downstream theorem stable_iff_boundary and referenced by the IsStable declarations in DiscretenessForcing and LogicFromCost. It anchors the pre-logical layer of the forcing chain by equating stability with cost minima at the unit-interval boundaries.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.