FreeOrbit
plain-language theorem explainer
FreeOrbit uniformly sets the iteration object of any strict logic realization to the inductive type LogicNat generated by identity and step. Researchers formalizing the universal forcing theorem cite this to guarantee that the orbit derives solely from native carrier operations without an internal field. The declaration is a direct abbreviation to LogicNat.
Claim. For any strict logic realization $R$, the free orbit is the inductive type generated by an identity element and a successor step, written $LogicNat$.
background
A strict logic realization is a structure supplying only a carrier type, a cost type with zero, a comparison map, a composition operation, a unit element, a generator, and two laws: comparison of any element to itself yields zero cost, and comparison is symmetric. The module removes the internal orbit field present in the earlier lightweight interface, forcing the orbit to be derived uniformly. LogicNat is the inductive type with constructors identity (the zero-cost unit) and step (iteration of the generator), representing the smallest set closed under multiplication by the generator and containing the unit.
proof idea
This is a one-line abbreviation that directly aliases the free orbit of a strict realization to the LogicNat inductive type.
why it matters
The definition supplies the orbit required by the strict interface, enabling the interpretation map that recurses over the native generator and composition, the conversion to the lightweight LogicRealization, and the proof that the orbit forms a natural-number object. It closes the supplied-orbit escape hatch in the universal forcing path, ensuring the theorem rests only on native law data.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.