stable_iff_boundary
plain-language theorem explainer
Pre-logical states achieve zero cost exactly when their value is zero or one. Researchers building the foundation layer cite this equivalence to locate cost minima before deriving logical structures. The argument unfolds the product definition of pre-cost and splits cases with the zero-product lemma from the integers layer.
Claim. For a pre-state $s$ whose value lies in the unit interval, the configuration is stable if and only if its value equals $0$ or $1$.
background
The module treats pre-logical configurations as real numbers in $[0,1]$. PreState packages such a value with the explicit interval bounds. Pre-cost is the quadratic $s.val * (1 - s.val)$, whose zeros mark the boundary minima. IsStable is defined simply as pre-cost equal to zero. This pre-logical layer precedes the extraction of logical integers and sits upstream of the full J-cost stability notion imported from DiscretenessForcing.
proof idea
The term proof first unfolds both IsStable and preCost to obtain the equation $s.val * (1 - s.val) = 0$. It invokes mul_eq_zero to factor the product into the two cases $s.val = 0$ or $s.val = 1$. The converse direction applies simp on each case to recover the zero product.
why it matters
The result fixes the arithmetic minima of the pre-cost landscape at the endpoints, supplying the concrete content for the stable-state predicate used in the foundation. It bridges the pre-logical cost to the later logical layer without invoking the full defect function from DiscretenessForcing. No downstream theorems are listed, leaving open how this boundary characterization lifts to the eight-tick octave and spatial dimensions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.