distinctionStep
plain-language theorem explainer
distinctionStep supplies the constant successor map for any LogicRealization built from a bare distinction on carrier K. Researchers deriving logic from minimal carriers cite it when constructing the total endomap that advances every state to the distinguished point y. The definition is implemented directly as the constant function returning y.
Claim. For any carrier set $K$ and points $x, y$ in $K$, the step map induced by the distinction is the constant function $f: K to K$ satisfying $f(z) = y$ for all $z$ in $K$.
background
The module shows that a single distinction $x neq y$ on an arbitrary carrier $K$ instantiates the full LogicRealization interface on that carrier. The cost is the natural-number equality cost, the identity point is $x$, and the step map is the constant function to $y$ supplied here. This minimal construction proves that every non-singleton carrier carries a LogicRealization, so Universal Forcing applies and yields the same forced arithmetic object as the canonical case.
proof idea
The definition is a one-line constant function that discards its argument and returns the distinguished point $y$.
why it matters
It supplies the step component of logicRealizationOfDistinction, the universal instantiation theorem that any carrier with a named distinction is a LogicRealization. This fills the first universal step in the Recognition Science framework: every non-singleton carrier instantiates the Law-of-Logic interface, allowing the T0-T8 forcing chain and the same phi-ladder arithmetic to apply without assuming a native real-valued J-cost on the carrier.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.