interpret_step
plain-language theorem explainer
The recursive step for the interpretation map from the free orbit LogicNat into the carrier of a strict logic realization equates the successor case to composing the generator onto the prior interpretation. Researchers constructing concrete realizations or proving universal forcing properties cite this when inducting over the orbit. The equality holds immediately by reflexivity because interpret is defined by primitive recursion whose step clause matches the right-hand side exactly.
Claim. Let $R$ be a strict logic realization. For any $n$ in the free orbit of $R$, the interpretation of the successor of $n$ equals the composition of the generator of $R$ with the interpretation of $n$.
background
A strict logic realization supplies a carrier type, cost type with zero, a comparison map, a binary composition, an identity element, and a generator, together with laws that the identity has zero cost and comparison is symmetric. The free orbit is the inductive type LogicNat whose constructors are identity (the zero-cost element) and step (one further iteration of the generator), exactly the smallest subset of positive reals closed under multiplication by the generator and containing the identity. The interpretation function maps this orbit into the carrier by primitive recursion: identity goes to the realization's identity element and each step applies composition with the generator.
proof idea
The proof is a one-line term proof by reflexivity. Because interpret is defined by primitive recursion on LogicNat whose step clause is literally the right-hand side of the claimed equality, the two sides are definitionally identical.
why it matters
This step case is invoked by every concrete realization that builds on the strict interface, including the canonical categorical realization from the natural-numbers object, the boolean realization, the modular cyclic realization, the ordered natural-number realization, and the physics and biology realizations. It closes the gap between the strict interface (native data only) and the lightweight LogicRealization interface used by the universal forcing theorem, ensuring the derived LogicNat orbit behaves as required without an internal orbit field.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.