universal_peano_surface
plain-language theorem explainer
Every Law-of-Logic realization forces an arithmetic object whose Peano surface obeys distinct zero, injective successor, and induction. Researchers establishing invariance of extracted arithmetic across realizations cite this result. The proof is a direct one-line application of the extraction theorem for the Peano surface.
Claim. For any Law-of-Logic realization $R$, let $A$ be the arithmetic object extracted from $R$. Then $A$ satisfies the Peano surface: its zero differs from the successor of every carrier element, its successor map is injective, and induction holds for every predicate on the carrier.
background
A Law-of-Logic realization supplies a carrier, comparison cost, zero element, and step action together with the structural laws needed for forcing. The arithmetic object forced by the realization is the structure ArithmeticOf R, which packages a Peano object with an initiality condition. The Peano surface of this object asserts zero distinct from all successors, injectivity of successor, and the induction schema.
proof idea
The proof is a one-line wrapper that applies the peano_surface theorem from the UniversalForcing module, which invokes the extracted_peanoSurface construction on the realization.
why it matters
This theorem confirms that the Peano surface properties hold uniformly for the arithmetic extracted from any Law-of-Logic realization, forming part of the general Universal Forcing theorem that every realization carries canonically equivalent forced arithmetic. It supports the invariance claims by ensuring the arithmetic object is well-behaved independently of the specific realization. No open questions are directly touched.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.