logicRealizationOfDistinction_actionInvariant
plain-language theorem explainer
On any carrier with two distinct points, the Law-of-Logic realization built from that distinction has an action-invariant step: the generator sends every state to the same marked second point. Anyone citing the minimal LogicRealization-from-distinction construction needs this field discharged. The proof is a one-line reflexivity after unfolding the constant step map.
Claim. Let $K$ be a type with decidable equality and let $x,y\in K$ with $x\neq y$. In the Law-of-Logic realization of $K$ induced by the distinction $(x,y)$, the step map is action-invariant: for all $a,b\in K$, the step applied to $a$ equals the step applied to $b$ (both equal $y$).
background
The module answers a skeptical gap in Reality-from-Distinction: a bare pair of unequal points should itself instantiate the Law-of-Logic interface, not merely sit beside a pre-built canonical certificate. Given $x\neq y$ on a carrier $K$, one builds a LogicRealization whose carrier is $K$, whose comparison is two-valued equality cost, whose identity is $x$, and whose step is the constant endomap sending every state to $y$.
A Law-of-Logic realization packages a carrier, a cost type, a comparison, an identity element, and a step/generator, together with the structural laws Universal Forcing needs. The arithmetic object extracted from identity/step data is the invariant target, not the ambient carrier itself.
The step map here is the distinction step: every input advances to the distinguished second point. Action-invariance is the proposition that this step is independent of its input, i.e. constant on $K$.
proof idea
Unfold action-invariance to the statement that the distinction step agrees on every pair of inputs. Introduce two dummy states and close by reflexivity: both sides reduce definitionally to the fixed second point $y$, since the step is fun _ => y. No external lemmas are required.
why it matters
This discharges one structural field of the minimal LogicRealization built from a single distinction. With comparison, identity, step, and the remaining interface laws in place, every non-singleton carrier instantiates the Law-of-Logic interface, so Universal Forcing applies and yields the same forced arithmetic object as the canonical recognition realization.
That is the first universal step the module claims is actually true. Continuous J-cost and spacetime structure are reached later by realization-invariance, not by pretending an arbitrary $K$ is $\mathbb{R}_{>0}$. The construction sits upstream of the forcing chain (T5 J-uniqueness through T8 dimension) once the interface is live on the carrier. No downstream dependents are recorded yet; the theorem closes a required field of the sibling realization constructor.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.