peano_surface
plain-language theorem explainer
Any strict logic realization yields forced arithmetic obeying the Peano surface axioms. Modelers of discrete logic realizations cite this when confirming arithmetic structure without caller-supplied orbits. The proof is a one-line wrapper that invokes the lightweight peano_surface after the canonical conversion to the standard interface.
Claim. Let $R$ be a strict logic realization. Then the arithmetic object extracted from the lightweight realization derived from $R$ satisfies the Peano surface: its zero differs from every successor, the successor map is injective, and the induction principle holds for every predicate on the carrier.
background
StrictLogicRealization is a structure supplying only native Carrier, Cost, compare, compose, one, generator, identity_law, and non_contradiction_law; the free orbit is derived uniformly as LogicNat rather than supplied. The arith definition produces ArithmeticOf by applying arithmeticOf to toLightweight R, which maps the strict data to the LogicRealization interface. PeanoSurface is the Prop requiring zero_ne_step, step_injective, and induction on the peano carrier of that ArithmeticOf object.
proof idea
One-line wrapper that applies UniversalForcing.peano_surface to the result of toLightweight R.
why it matters
This result feeds strict_peano_surface and universal_peano_surface, which in turn support bool_peano_surface. It closes the verification path for the derived orbit in StrictLogicRealization, confirming that removal of the supplied-orbit escape hatch still yields the standard Peano axioms on the forced arithmetic. The declaration sits inside the chain that extracts ArithmeticOf from every Law-of-Logic realization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.