universalInstantiationCert
plain-language theorem explainer
Any nonempty carrier K with at least one distinction admits a LogicRealization on exactly that carrier, using two-valued equality cost and a constant step map. Foundation researchers cite this to justify applying Universal Forcing to arbitrary non-singleton types before reaching the continuous J layer. The proof is a direct term assignment that packages two existence lemmas into the required structure.
Claim. For any nonempty type $K$, if there exist distinct $x,y$ in $K$, then there is a nonempty LogicRealization whose carrier is $K$, whose comparison is the two-valued equality cost, whose identity point is $x$, and whose step map is the constant map to $y$; moreover a named version exists that retains the explicit choice of $x,y$ and the inequality witness.
background
The module constructs a minimal LogicRealization on any carrier that is not a singleton. The realization uses the two-valued equality cost as comparison function, picks one point as identity, and maps every step to the other point; its internal orbit is the free LogicNat orbit. This supplies the Law-of-Logic interface without assuming a native smooth real-valued J-cost on the carrier.
proof idea
The proof is a one-line term-mode wrapper. It supplies the instantiate field of the structure by direct reference to the existence theorem that builds a LogicRealization from any distinction, and supplies the named field by reference to the version that retains the chosen points and witness.
why it matters
This declaration removes the skeptical objection that a bare distinction cannot instantiate the Law-of-Logic interface on its own carrier. It therefore lets Universal Forcing apply to every non-singleton type, yielding the same forced arithmetic object as the canonical recognition realization. The result is the first universal step before realization-invariance reaches the continuous J/spacetime layer.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.