exists_logicRealization_of_distinction
plain-language theorem explainer
Any nonempty type K that contains at least one pair of distinct elements admits a LogicRealization whose carrier is exactly K. Researchers building the universal forcing chain cite the result to obtain the Law-of-Logic interface from bare distinguishability alone. The proof is a one-line wrapper that extracts the distinguishing pair classically and feeds it to the named distinction-based construction.
Claim. Let $K$ be a nonempty type containing distinct elements $x,y$. Then there exists a LogicRealization on carrier $K$ whose cost type is the natural numbers, whose comparison is decidable equality, whose identity element is $x$, and whose step map is the constant function with value $y$.
background
A LogicRealization is a carrier equipped with a cost type (here the naturals), a zero-cost element, a comparison map, an identity point, and a step generator, together with the structural propositions required by the Universal Forcing program. The module shows that any non-singleton carrier can serve as such a realization without presupposing a smooth J-cost or a canonical model. The key upstream construction (logicRealizationOfDistinction) builds the structure explicitly: it sets the carrier to K, the cost to Nat, the identity to one distinguished point, and the step map to the constant function returning the other point, with the internal orbit being the free LogicNat orbit.
proof idea
The proof is a one-line wrapper. Classical logic extracts concrete witnesses x and y from the existential hypothesis that two elements differ; the named distinction-based construction is then applied directly to those witnesses to produce the required LogicRealization instance.
why it matters
The theorem supplies the universal instantiation step required by the master forcing chain (reality_from_one_distinction). It shows that every non-singleton carrier can serve as a LogicRealization, so that Universal Forcing applies uniformly and extracts the same arithmetic object as the canonical case. The result therefore closes the first universal step before the continuous J-cost and spacetime layers are reached via realization invariance. It touches the open question of how arbitrary carriers later acquire smooth structure without additional hypotheses.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.