distinctionInterpret_zero
plain-language theorem explainer
The declaration states that the distinction interpretation of the LogicNat identity element returns the base point x of any carrier K. Researchers constructing minimal Law-of-Logic realizations from a single distinction would cite it when reducing identity cases in orbit maps. The proof is immediate reflexivity after unfolding the definition of distinctionInterpret.
Claim. For any carrier set $K$ and points $x,y$ in $K$, the map that sends the lifted identity of LogicNat to $x$ and every successor to $y$ satisfies distinctionInterpret$(x,y)$ (ULift.up LogicNat.identity) $= x$.
background
The module constructs a LogicRealization on an arbitrary non-singleton carrier $K$ equipped with two distinguishable points $x$ and $y$. distinctionInterpret is the function that sends the identity constructor of LogicNat to $x$ and every step constructor to $y$, thereby supplying the minimal endomap induced by one distinction. LogicNat itself is the inductive type whose identity element represents the zero-cost multiplicative identity and whose step constructor generates the free orbit under multiplication by the generator.
proof idea
One-line wrapper that applies reflexivity (rfl) directly to the definition of distinctionInterpret, whose identity case clause returns $x$ by construction.
why it matters
It supplies the first universal step asserted in the module: 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. The result therefore bridges a bare distinction to the Recognition Science forcing chain before the continuous J/spacetime layer is recovered via realization-invariance. No downstream uses appear yet.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.