natOrderedRealization
plain-language theorem explainer
The natural-number realization equips the carrier set of natural numbers with the natCost comparison function and the inductive orbit generated by identity and step constructors. Researchers verifying invariance of arithmetic across realizations in the Universal Forcing framework cite this construction as the base model. The definition assembles the structure by direct field assignment, delegating successor, interpretation, and induction proofs to the upstream LogicNat inductive type and its lemmas.
Claim. The ordered natural-number realization is the structure whose carrier is the set of natural numbers, whose cost function is the natural cost map, whose zero element is 0, whose step operation is the standard successor, whose orbit is the inductive type generated by an identity element and a successor constructor, whose interpretation map counts the number of successor applications, and which satisfies the axioms of zero preservation, successor injectivity, induction, and non-triviality.
background
In the module establishing ordered faithful realizations for Universal Forcing, this definition supplies the canonical model using natural numbers. The upstream LogicNat inductive type consists of an identity constructor and a step constructor; it represents the smallest orbit closed under the generator and containing the multiplicative identity. Its associated lemmas include successor injectivity (forced by constructor disjointness), the toNat map that sends identity to 0 and step n to the successor of toNat n, and the induction principle.
proof idea
The definition populates the LogicRealization structure by assigning Nat as carrier and natCost as compare. Orbit fields and proofs are delegated to LogicNat: orbitZero and orbitStep use its constructors, interpret applies toNat, interpret_step invokes toNat_succ, orbit_step_injective uses succ_injective, orbit_induction applies the induction principle, and nontriviality is witnessed by exhibiting 1 with a simplified natCost computation. Remaining fields are set to True or reflexivity.
why it matters
This definition supplies the base realization that feeds the equivOfInitial construction establishing invariance of ordered arithmetic across all realizations, and the injectivity argument proving faithful arithmetic interpretation. It anchors the concrete natural-number model in the ordered logic realization module, closing the arithmetic component of the forcing chain. No open scaffolding remains at this site.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.