orderRealization
plain-language theorem explainer
The ordered integer realization supplies a concrete carrier for forced arithmetic on the integers with unit increments and equality cost. Workers on the universal forcing chain cite this construction to embed the logic natural numbers orbit into the integers. The definition assembles the structure by direct field assignment, with orbit properties discharged by rewriting lemmas from the arithmetic module.
Claim. Define the ordered realization as the logic realization structure with carrier the integers, cost taking values in the natural numbers, comparison given by the integer cost function, zero element 0, step map $z mapsto z+1$, orbit the logic natural numbers, interpretation the standard embedding of the orbit into the integers, and the remaining axioms (identity, non-contradiction, nontriviality) satisfied by the integer cost properties.
background
The module defines an order-theoretic realization on the integers with equality cost and unit step. This is a lightweight model: the forced arithmetic is carried by the certified internal orbit, while the carrier interpretation is the standard embedding of the logic natural numbers into the integers.
proof idea
The definition populates each field of the logic realization structure. Interpret zero and interpret step are discharged by simp and rw with the toNat successor lemma followed by norm_num. Orbit no-confusion applies the zero not successor theorem, orbit step injective uses the successor injectivity theorem, and orbit induction applies the logic natural numbers induction. Nontriviality is witnessed by exhibiting 1 and simplifying the integer cost.
why it matters
This definition is invoked by the order arithmetic invariant to establish equivalence of arithmetic carriers across any two realizations. It supplies the standard concrete model for the universal forced arithmetic in the foundation module. The construction realizes the ordered arithmetic forced by the law of logic on the integers.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.