arith_universal_initial
plain-language theorem explainer
Every Law-of-Logic realization supplies a Peano arithmetic object canonically equivalent to the reference LogicNat. Researchers establishing that forced arithmetic is an initial algebra would cite this equivalence as the base case of the Universal Forcing theorem. The definition is a one-line wrapper that applies the orbit equivalence supplied by the realization.
Claim. For any Law-of-Logic realization $R$, the Peano carrier extracted from the arithmetic of $R$ is canonically equivalent to the reference natural numbers $LogicNat$.
background
LogicRealization is a structure with a carrier type, a cost type equipped with zero, a comparison map, a zero element, and the structural laws required by the Universal Forcing program. LogicNat is the inductive type generated by the constructors identity (zero-cost element) and step (iteration of the generator), representing the smallest orbit closed under the multiplicative action in the positive reals. The module states the first formal version of the theorem that any two Law-of-Logic realizations have canonically equivalent forced arithmetic objects because those objects are initial Peano algebras.
proof idea
The definition is a one-line wrapper that applies the orbitEquivLogicNat field of the supplied realization.
why it matters
This declaration supplies the simplest form of the Universal Forcing theorem, showing that the forced arithmetic of every realization is canonically equivalent to LogicNat. It supports the meta-claim that any two realizations yield equivalent arithmetic objects as initial Peano algebras. In the Recognition Science framework it anchors the independence of the extracted arithmetic from the concrete realization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.