orderRealization
The ordered integer realization supplies a concrete model of the forced arithmetic on the integers, using unit step and equality cost on the carrier. Researchers working on the universal forcing chain cite it as the base ordered model that embeds the logic natural numbers into the integers. The definition assembles the structure record by wiring integer operations to the inductive orbit and verifying invariants through direct rewriting and normalization.
claimThe ordered realization is the structure with carrier the integers $Z$, cost the natural numbers, zero element $0$, step function $z mapsto z+1$, orbit the inductive logic natural numbers, and interpretation the embedding that sends the orbit identity to $0$ and each successor to an increment by one.
background
The module introduces order-theoretic realizations that carry the arithmetic forced by logic. The logic natural numbers form an inductive type with an identity constructor and a successor constructor; this encodes the smallest orbit closed under the generator and containing the identity, as described in the upstream ArithmeticFromLogic development. The integer realization is lightweight: the certified internal orbit carries the forced arithmetic while the carrier uses the standard embedding of the orbit into the integers.
proof idea
The definition constructs the realization structure field by field, assigning the integer carrier, natural-number cost, integer successor step, logic natural orbit, and embedding interpretation. The interpret_step field is discharged by rewriting with the toNat successor lemma followed by normalization; orbit_no_confusion applies the zero-not-successor property; orbit_step_injective and orbit_induction are transferred directly from the corresponding logic natural theorems.
why it matters in Recognition Science
This definition supplies the ordered base case for the arithmetic equivalence result in the same module, which establishes that the Peano carrier of this realization is equivalent to the carrier of any other realization. It realizes the forced arithmetic on the ordered integers, connecting the logic-derived naturals to the integer line and supporting the universal forcing chain. It touches the question of how the abstract orbit embeds into concrete ordered structures.
scope and limits
- Does not claim uniqueness of this realization among all possible carriers.
- Does not derive the forcing steps T5 through T8 or the Recognition Composition Law.
- Does not extend the construction to non-ordered or continuous carriers.
- Does not compute explicit costs for elements outside the integer line.
formal statement (Lean)
37def orderRealization : LogicRealization where
38 Carrier := ℤ
proof body
Definition body.
39 Cost := Nat
40 zeroCost := inferInstance
41 compare := intCost
42 zero := 0
43 step := fun z => z + 1
44 Orbit := LogicNat
45 orbitZero := LogicNat.zero
46 orbitStep := LogicNat.succ
47 interpret := intOrbitInterpret
48 interpret_zero := by simp [intOrbitInterpret]
49 interpret_step := by
50 intro n
51 show ((LogicNat.toNat (LogicNat.succ n) : ℤ) = (LogicNat.toNat n : ℤ) + 1)
52 rw [LogicNat.toNat_succ]
53 norm_num
54 orbit_no_confusion := by
55 intro n h
56 exact LogicNat.zero_ne_succ n h
57 orbit_step_injective := LogicNat.succ_injective
58 orbit_induction := by
59 intro P h0 hs n
60 exact LogicNat.induction (motive := P) h0 hs n
61 orbitEquivLogicNat := Equiv.refl LogicNat
62 orbitEquiv_zero := rfl
63 orbitEquiv_step := by intro n; rfl
64 identity := intCost_self
65 nonContradiction := intCost_symm
66 excludedMiddle := True
67 composition := True
68 actionInvariant := True
69 nontrivial := by
70 refine ⟨1, ?_⟩
71 simp [intCost]
72
73/-- Ordered realization carries the universal forced arithmetic. -/