intOrbitInterpret
plain-language theorem explainer
The definition embeds each element of the logic-natural numbers into the integers by converting it to its iteration count. Researchers constructing order realizations in the universal forcing module cite this when defining the carrier for integer arithmetic. It supplies the nonnegative integer values needed for the unit-step realization on the integers. The implementation directly applies the iteration count map and casts the result to an integer.
Claim. The map sending each logic-natural number $n$ to the nonnegative integer given by its iteration count, where the identity element maps to zero and each successive step increments the count by one.
background
The logic-natural numbers form an inductive type with constructors identity (the zero-cost element, the multiplicative identity in the orbit) and step (one more iteration of the generator). Its documentation states: 'The natural numbers as forced by the Law of Logic. identity represents the zero-cost element (the multiplicative identity in the orbit). step represents one more iteration of the generator. The two-constructor structure mirrors the orbit {1, γ, γ², γ³, ...} as the smallest subset of ℝ₊ closed under multiplication by γ and containing 1.' The forward map extracts the iteration count by recursion, sending identity to 0 and step n to the successor of the count for n. The module supplies an order-theoretic realization on the integers with equality cost and unit step. This is a lightweight construction: the forced arithmetic is carried by the certified internal orbit while the carrier uses the standard embedding of the logic-natural numbers into the integers.
proof idea
The definition is a one-line wrapper that applies the iteration count map to the input logic-natural number and casts the resulting natural number to an integer.
why it matters
This definition supplies the integer interpretation used by orderRealization to build the LogicRealization with carrier the integers. It completes the ordered integer realization with unit step in the universal forcing module. In the Recognition framework it bridges the logic-forced naturals to the arithmetic needed for higher structures such as the phi-ladder.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.