logicRealizationOfDistinction
plain-language theorem explainer
Any type K equipped with distinct elements x and y carries a LogicRealization whose carrier is exactly K, with equality cost, constant step to y, and free LogicNat orbit. Researchers deriving arithmetic from logic or applying universal forcing cite this construction to show every non-singleton carrier instantiates the required interface. The definition supplies concrete values for all fields and delegates axiom checks to sibling lemmas on cost symmetry and interpretation steps.
Claim. Let $K$ be a type with decidable equality. For distinct $x,y:K$, there is a LogicRealization structure on carrier $K$ whose cost function is the two-valued equality cost, whose zero element is $x$, whose step map is constantly $y$, whose orbit is the free LogicNat orbit, and whose interpretation map satisfies the zero and step axioms by direct construction.
background
The module UniversalInstantiationFromDistinction shows that a bare distinction suffices to instantiate the Law-of-Logic interface on its own carrier. LogicRealization is the structure imported from LogicRealization that packages a carrier, a cost function to Nat, a step map, an orbit isomorphic to LogicNat, and interpretation and invariance axioms. The local construction uses the two-valued equality cost (eqCost) for compare, the constant map distinctionStep x y for step, and distinctionInterpret for the interpretation map. Upstream, UniversalForcing supplies the arithmeticOf operation that later extracts the forced Peano structure from any such realization.
proof idea
The definition constructs the LogicRealization record by direct field assignment: Carrier to K, Cost to Nat, compare to eqCost, zero to x, step to distinctionStep x y, Orbit to ULift LogicNat, interpret to distinctionInterpret x y. Axioms are discharged by one-line references: eqCost_self for identity, eqCost_symm for nonContradiction, distinctionInterpret_step for interpret_step, LogicNat.zero_ne_succ and succ_injective for orbit axioms, and rfl for the orbit equivalence maps.
why it matters
This definition supplies the concrete object used by exists_logicRealization_of_distinction, distinction_arithmetic_equiv_logicNat, and distinction_realizations_have_same_arithmetic. It completes the universal instantiation step that lets Universal Forcing apply to any distinguished carrier and yields the same forced arithmetic object as the canonical recognition realization. The construction addresses the objection that a bare distinction must be bundled beside an existing certificate rather than generating its own LogicRealization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.