strict_peano_surface
plain-language theorem explainer
Every strict logic realization R induces an arithmetic object whose Peano surface satisfies zero distinct from successors, injectivity of successor, and the induction principle. Researchers verifying invariance of forced arithmetic under the strict Universal Forcing construction cite this result. The proof is a direct one-line application of the peano_surface theorem already established for StrictLogicRealization.
Claim. For every strict logic realization $R$, let $A$ be the arithmetic object extracted from $R$. Then $A$ satisfies: $A.peano.zero ≠ A.peano.step(x)$ for all carriers $x$, the successor map is injective, and the induction axiom holds for every predicate on the carrier.
background
The module Strict.Invariance records that native Law-of-Logic data determines a derived free orbit and that all such orbits are canonically equivalent. A StrictLogicRealization supplies only a carrier, a cost type with zero, a comparison, and a composition map, without any pre-given orbit. ArithmeticOf is the structure forced by any LogicRealization; it packages a PeanoObject together with the fact that the object is initial. PeanoSurface is the proposition that this object obeys the three classical Peano axioms: zero is not a successor, successor is injective, and induction holds. The upstream theorem UniversalForcing.peano_surface asserts that every realization carries a Peano surface on its forced arithmetic; the strict counterpart in StrictRealization inherits the surface from the lightweight realization obtained by toLightweight.
proof idea
The proof is a one-line term wrapper that applies StrictLogicRealization.peano_surface R. That lemma in turn reduces the claim to UniversalForcing.peano_surface applied to the lightweight realization derived from R.
why it matters
The declaration closes the invariance step for the Peano surface under strict realizations, confirming that the arithmetic forced by native law data obeys the standard Peano axioms. It directly supports the Strict Universal Forcing theorem stated in the module documentation. No downstream uses are recorded yet, and the result touches no open scaffolding questions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.