exists_named_logicRealization_of_distinction
plain-language theorem explainer
Any nonempty type K containing at least two distinct elements admits a LogicRealization whose carrier is exactly K and whose extracted arithmetic orbit is LogicNat. Researchers formalizing the passage from bare distinction to forced arithmetic in Recognition Science cite this result to justify applying Universal Forcing to arbitrary carriers. The proof performs classical case analysis on the witness pair and packages the output of logicRealizationOfDistinction inside the required Nonempty constructor.
Claim. Let $K$ be a nonempty type. If there exist distinct $x, y : K$, then there exist $x, y : K$ with $x ≠ y$ such that the type of LogicRealizations on carrier $K$ (with cost type in universe 0) is nonempty.
background
The module repairs the objection that a bare distinction cannot be bundled with an already-existing reality certificate. It shows that any carrier $K$ with two distinguishable points $x ≠ y$ directly instantiates the Law-of-Logic interface on itself. The comparison cost is the two-valued equality predicate, the identity element is $x$, the step map sends everything to $y$, and the internal orbit is the free LogicNat generated by repeated application of the step constructor. LogicRealization is the structure that packages a carrier, a cost type equipped with zero, a compare function, a zero element, and the propositions required for Universal Forcing to extract an arithmetic object. LogicNat is the inductive type whose constructors identity and step mirror the orbit {1, γ, γ², …} under multiplication by the golden-ratio generator.
proof idea
The proof is a term-mode one-liner. It opens classical to permit case analysis, destructures the hypothesis ∃ x y, x ≠ y via rcases into concrete witnesses x, y and inequality hxy, then returns the tuple ⟨x, y, hxy, ⟨logicRealizationOfDistinction K x y hxy⟩⟩ that witnesses the target existential.
why it matters
This supplies the named instantiation used by universalInstantiationCert, which asserts that UniversalInstantiationCert K holds. It completes the module's first universal step: every non-singleton carrier instantiates the Law-of-Logic interface, so Universal Forcing applies and yields the same forced arithmetic object LogicNat as the canonical recognition realization. The construction therefore bridges the distinction-to-arithmetic segment of the forcing chain without presupposing a smooth J-cost on K. It directly addresses the skeptical objection recorded in the module documentation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.