distinctionInterpret_step
plain-language theorem explainer
The theorem shows that distinction interpretation commutes with the successor on lifted LogicNat: the image of step n equals the distinction step applied to the image of n. Researchers building LogicRealization from a single named distinction cite this compatibility to justify the inductive orbit construction. The proof is a direct case split on the ULift wrapper and the two constructors of LogicNat, collapsing to reflexivity.
Claim. For any type $K$, elements $x,y$ in $K$, and lifted logic natural number $n$, the interpretation of the successor of $n$ equals the one-step distinction map applied to the interpretation of $n$.
background
The module constructs a LogicRealization on an arbitrary carrier $K$ once two distinguishable points $x,y$ are given. LogicNat is the inductive type with constructors identity (zero-cost base) and step (generator), mirroring the free orbit under multiplication by the forced ratio. distinctionInterpret maps each lifted LogicNat element to an element of $K$ by iterated application of distinctionStep, which advances from the identity point $x$ toward $y$ along the orbit. The module doc states that this yields the first universal step that is actually true: every non-singleton carrier instantiates the Law-of-Logic interface, after which Universal Forcing applies directly.
proof idea
The term proof opens with cases on the ULift wrapper, exposing the underlying LogicNat value, then performs exhaustive case analysis on the two constructors of LogicNat. Each branch reduces immediately to reflexivity by the definitional unfolding of distinctionInterpret and distinctionStep.
why it matters
The result is invoked inside logicRealizationOfDistinction, the definition that packages any carrier with a named distinction $x ≠ y$ as a LogicRealization whose carrier is exactly $K$, Cost is Nat, and step map is constant to $y$. It thereby supplies the minimal instantiation required before canonical realization-invariance can reach the continuous J/spacetime layer. The construction stays within the eight-tick octave and phi-ladder structure already forced by the upstream LogicNat inductive definition.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.