preCost
plain-language theorem explainer
The preCost definition equips each pre-logical state s with the real number given by its value times one minus that value. Analysts of pre-logical stability cite this as the explicit cost landscape on the unit interval. The expression vanishes exactly at the endpoints, marking the minima. The body consists of a direct algebraic product with no auxiliary computation.
Claim. For a configuration value $v$ in the closed unit interval, the pre-logical cost is $v(1-v)$.
background
The module introduces PreState as a real number val equipped with the proof that it satisfies $0 ≤ val ≤ 1$. The module doc-comment frames this as the pre-logical configuration value constrained to the unit interval. The supplied doc-comment for preCost itself notes that the resulting landscape on [0,1] has minima at the boundary states.
proof idea
The definition is a direct one-line expression that multiplies the configuration value by its complement. No lemmas or tactics are applied; the body is the explicit formula.
why it matters
This definition supplies the cost expression used to define IsStable as the predicate that the cost equals zero. It thereby supports the downstream equivalence of stability to the boundary values 0 or 1. The construction realizes the pre-logical cost landscape whose minima occur at boundaries, consistent with the framework emphasis on cost minima for stable configurations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.