canonical
plain-language theorem explainer
The canonical definition supplies the initial Peano arithmetic object extracted from any Law-of-Logic realization. Researchers on the Recognition Science forcing program cite it when they require the unique-up-to-isomorphism arithmetic structure that follows from identity and step data alone. The definition is a direct structure constructor that wires the pre-proved initiality of LogicNat into the ArithmeticOf record.
Claim. For any Law-of-Logic realization $R$, the canonical arithmetic object is the structure whose Peano object is the natural-numbers object carried by LogicNat (with its zero and successor) together with the proof that this object is initial among all Peano objects.
background
ArithmeticOf packages a PeanoObject with a proof of its initiality. A LogicRealization supplies a carrier, comparison cost, zero element, and step action; the arithmetic content is then extracted via initiality. The module states that once identity and step data are supplied, the forced arithmetic object is the initial Peano algebra generated by that data, with initial objects unique up to unique isomorphism. Upstream, logicNatPeano builds the Peano object on LogicNat while logicNat_initial supplies the lift and uniqueness maps that establish initiality.
proof idea
This is a definition that constructs an ArithmeticOf instance by setting the peano field to logicNatPeano and the initial field to logicNat_initial.
why it matters
The definition supplies the canonical arithmetic object used by downstream constructions such as canonicalCostAlgebra and canonicalRecognitionCostSystem. It realizes the initiality mechanism of Universal Forcing, ensuring arithmetic content remains invariant across realizations. It anchors the extraction step that precedes the J-cost and phi-ladder structures in the T0-T8 chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 2 of 2)
-
Trained encoder transplant cuts grokking delay by 2.75 times
"Numeral base acts as an inductive bias that controls how much local digit structure the decoder can exploit"
-
Fraction is a category of concepts, not one math idea
"We introduce a way of specifying number systems, and compare the analytical concepts with those of structuralism."