peano_surface
plain-language theorem explainer
Every Law-of-Logic realization forces an arithmetic object whose carrier satisfies the three Peano surface axioms. Researchers establishing the universality of forced arithmetic across realizations cite this result to confirm initiality. The proof is a direct one-line application of the extracted_peanoSurface lemma that assembles the surface fields from the realization's orbit axioms.
Claim. For any Law-of-Logic realization $R$, the forced arithmetic object arithmeticOf($R$) satisfies the Peano surface property: its zero differs from every successor, the successor map is injective, and the induction principle holds for every predicate on the carrier.
background
A LogicRealization supplies a carrier, a comparison cost, a zero element, and the structural propositions (orbit_no_confusion, orbit_step_injective, orbit_induction) that permit arithmetic extraction. The ArithmeticOf structure packages the resulting PeanoObject together with its initiality witness. PeanoSurface is the proposition that records the three surface axioms: zero_ne_step, step_injective, and induction. The module states the first form of the Universal Forcing theorem: any two realizations yield canonically equivalent forced arithmetic objects because those objects are initial Peano algebras. This theorem rests on the upstream extracted_peanoSurface result, which constructs the surface directly from the orbit properties supplied by the realization.
proof idea
The proof is a one-line term that applies the extracted_peanoSurface lemma to the input realization R. That lemma assembles the three fields of PeanoSurface from the corresponding orbit axioms of R: zero_ne_step from orbit_no_confusion, step_injective from orbit_step_injective, and induction from orbit_induction.
why it matters
This declaration supplies the Peano surface for the arithmetic object of an arbitrary realization and serves as the base case for the invariance theorems in the Universal and Strict submodules. It directly supports the module claim that forced arithmetic objects are initial Peano algebras. Downstream results such as bool_peano_surface and universal_peano_surface invoke it to verify the property for concrete realizations and invariance statements. In the Recognition Science framework it anchors the arithmetic extraction step of the Universal Forcing chain before further forcing to dimensions and constants.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.