UniversalInstantiationCert
plain-language theorem explainer
Any nonempty carrier K admitting at least one distinction x ≠ y carries a LogicRealization whose carrier is exactly K, using two-valued equality cost. Foundation researchers cite the certificate when establishing that Universal Forcing applies uniformly to arbitrary non-singleton sets before extracting arithmetic. The structure packages the two existence statements directly from the distinction data.
Claim. Let $K$ be a nonempty type. The certificate asserts that if there exist distinct $x,y$ in $K$, then a logic realization (carrier $K$, two-valued equality cost, identity $x$, constant step to $y$) exists; moreover there exist explicit witnesses $x,y$ with $x≠y$ such that the logic realization is nonempty.
background
The module shows that a bare distinction on any carrier instantiates the Law-of-Logic interface on its own carrier. A LogicRealization supplies a carrier, cost type with zero, compare map, zero element, and the structural laws required by the Universal Forcing program; the invariant target is the arithmetic object extracted from the identity and step data. Given $K$ with $x≠y$, the construction uses the two-valued equality cost, identity point $x$, and constant step map to $y$, with internal orbit the free LogicNat orbit. This is the minimal first universal step: every non-singleton carrier instantiates the interface, so Universal Forcing applies and yields the same forced arithmetic as the canonical recognition realization.
proof idea
The declaration is a structure definition with no proof body. It directly asserts the two fields: the instantiate field records existence of a LogicRealization from any distinction on $K$, while the named field records existence of explicit witnesses $x,y$ together with the inequality and the realization.
why it matters
The certificate is invoked by the theorem universalInstantiationCert to conclude that any nonempty $K$ satisfies the instantiation property. It completes the first universal step in the foundation: every non-singleton carrier instantiates the Law-of-Logic interface, therefore Universal Forcing applies and produces the same forced arithmetic object as the canonical recognition realization. The module notes that the continuous J/spacetime layer is reached through canonical realization-invariance rather than by identifying an arbitrary $K$ with the positive reals.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.