interpret
plain-language theorem explainer
The interpret definition recursively embeds the free orbit LogicNat into the carrier of any StrictLogicRealization by sending the base identity to the realization's one element and each successor to the composition of the generator with the prior image. Workers constructing concrete Law-of-Logic realizations cite it to obtain the arithmetic orbit without an internal field. The definition proceeds by direct pattern matching on the two constructors of LogicNat.
Claim. For a strict logic realization $R$, the map $interpret_R : LogicNat → R.Carrier$ is defined by $interpret_R(identity) = R.one$ and $interpret_R(step n) = R.compose(R.generator, interpret_R n)$.
background
StrictLogicRealization is the structure that supplies only native data: a carrier type, cost type with zero, compare function, compose operation, one element, generator, and the two laws that identity has zero cost and comparison is symmetric. FreeOrbit R is the abbrev that uniformly sets the orbit to LogicNat, the inductive type whose identity constructor stands for the zero-cost element and whose step constructor iterates the generator. The module implements the strict Universal Forcing interface so that the orbit is derived rather than supplied internally, removing the escape hatch present in the earlier LogicRealization interface.
proof idea
The definition is given directly by pattern matching on the constructors of LogicNat: the identity case returns the one element supplied by the realization, and the step case applies the compose operation to the generator and the recursive call on the predecessor.
why it matters
This supplies the uniform embedding of the free orbit into the carrier for every strict realization, allowing the main Universal Forcing theorem to proceed from native generator and composition data alone. It is invoked by downstream realizations including boolRealization, natOrderedRealization, and canonicalCategoricalRealization to obtain their interpretations, and it appears in the definition of FaithfulArithmeticInterpretation. It closes the strict path in the Universal Forcing chain by deriving the arithmetic object from the native data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.