FreeOrbit
plain-language theorem explainer
FreeOrbit(R) for any strict logic realization R is defined to be the LogicNat inductive type. Researchers on the strict Universal Forcing path cite it to guarantee a uniform orbit without an internal field supplied by the caller. The declaration is a one-line abbreviation that directly names the iteration object forced by the Law of Logic.
Claim. For a strict logic realization $R$, the free orbit is the inductive type LogicNat generated by an identity constructor and a step constructor.
background
StrictLogicRealization is the structure whose fields are only native comparison, composition, identity, generator, and the two symmetry laws; it deliberately omits any supplied orbit field. The module StrictRealization therefore derives the free orbit uniformly from the earlier LogicNat construction. LogicNat is the inductive type whose constructors identity and step generate the smallest subset of positive reals closed under multiplication by the generator and containing the multiplicative identity.
proof idea
One-line abbreviation that directly returns the LogicNat inductive type.
why it matters
FreeOrbit supplies the orbit object required by interpret, interpret_step, toLightweight, and boolean_freeOrbit_isNNO. The last of these shows that the derived orbit remains a natural-number object even after carrier collapse, completing the strict path of the Universal Forcing theorem. It therefore removes the escape hatch present in the earlier LogicRealization interface while preserving the same iteration structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.