orderRealization
plain-language theorem explainer
The orderRealization supplies a concrete LogicRealization on the integers that carries the forced arithmetic orbit from LogicNat with unit successor and equality cost. Researchers on the universal forcing chain cite it as the base model establishing arithmetic invariance across realizations. The definition populates the structure by direct field assignment, delegating orbit axioms to lemmas from ArithmeticFromLogic.
Claim. Define the ordered realization with carrier set the integers, costs in the naturals, comparison via the integer cost function, zero element at 0, successor map sending each integer to its successor, orbit given by the forced naturals, and interpretation embedding the orbit into the carrier while preserving zero and successor.
background
The module constructs an order-theoretic realization on the integers. LogicNat is the inductive type whose constructors identity and step generate the orbit forced by the Law of Logic, the smallest subset of positive reals closed under multiplication by the generator and containing the identity. Upstream, toNat counts iterations along this orbit, toNat_succ records that successor on the orbit corresponds to adding one, succ_injective records constructor disjointness, and zero_ne_succ records that the identity is never a successor.
proof idea
The definition assembles the LogicRealization structure by assigning Carrier to integers, Cost to Nat, compare to intCost, step to integer successor, Orbit to LogicNat, and interpret to intOrbitInterpret. interpret_step rewrites via toNat_succ then normalizes; orbit_no_confusion applies zero_ne_succ; orbit_step_injective invokes succ_injective; orbit_induction invokes LogicNat.induction; nontrivial exhibits the element 1 with positive cost via intCost.
why it matters
orderRealization supplies the concrete ordered model that order_arithmetic_invariant invokes to prove that the Peano carrier is equivalent for any realization. It realizes the forced arithmetic inside the UniversalForcing layer, anchoring the T5 J-uniqueness and T6 self-similar fixed point through the certified orbit. The construction closes the arithmetic-invariant scaffolding for the foundation.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.