PeanoSurface
plain-language theorem explainer
PeanoSurface packages the three Peano axioms as a Prop on the carrier of any arithmetic object forced by a logic realization: zero is never a successor, successor is injective, and induction holds for every predicate. Category theorists and logicians studying initial algebras cite it when confirming that a realization yields the standard naturals up to unique isomorphism. The declaration is a bare structure definition with three fields and no proof body.
Claim. Let $R$ be a logic realization and let $A$ be the arithmetic object it forces. Then $A$ satisfies the Peano surface when its carrier obeys: the zero element differs from every successor, the successor map is injective, and every predicate on the carrier that holds at zero and is preserved by successor holds everywhere.
background
ArithmeticOf R is the structure that pairs a PeanoObject (carrier set with zero and step) with a proof that the object is initial. PeanoSurface is the Prop asserting the three standard Peano axioms on that object. The module extracts arithmetic from any LogicRealization; upstream LogicNat supplies the canonical initial object via its identity and step constructors, which mirror the orbit generated by repeated multiplication by the logic generator.
proof idea
Direct structure definition. The three fields zero_ne_step, step_injective, and induction are declared verbatim with no lemmas, tactics, or reductions applied.
why it matters
This supplies the target property proved by extracted_peanoSurface and canonical_peanoSurface, which feed directly into UniversalForcing.peano_surface and the invariance theorems that follow. It realizes the initiality mechanism stated in the module documentation, guaranteeing that every realization produces isomorphic arithmetic. The definition therefore anchors the arithmetic layer of the forcing construction.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Language models fail at extended rule following
"Stable Counting Capacity (SCC), a purely mechanical assay that utilizes a minimal probe based on homogeneous sequence counting"