PeanoEquiv
plain-language theorem explainer
A Peano-algebra isomorphism: a carrier equivalence that fixes zero and intertwines successor. Anyone working the Universal Forcing arithmetic-extraction layer cites this as the bundled type of a structure-preserving map between Peano objects. It is a plain structure definition (three fields), not a proved theorem.
Claim. Given Peano algebras $A$ and $B$ (each a carrier type with a distinguished zero and a successor map), a Peano equivalence is a type equivalence $f : |A| \simeq |B|$ such that $f(0_A) = 0_B$ and $f(S_A(x)) = S_B(f(x))$ for every $x \in |A|$.
background
This module is Universal Forcing, Part II (arithmetic-extraction). The spine already yields a bare carrier bijection between the forced arithmetics of any two Law-of-Logic realizations. A bare bijection need not respect zero or successor; the module upgrades that invariant to a unique Peano-algebra isomorphism.
A Peano object is a type equipped with a zero element and a unary step (successor) map. Homomorphisms are functions preserving zero and commuting with step. The present structure packages an equivalence of carriers together with those two preservation laws, so the map is an isomorphism of Peano algebras rather than a mere set bijection.
Everything is stated at the monomorphic {0,0} realization universe used throughout the Universal Forcing program, so carriers live in Type 0.
proof idea
No proof body: this is a structure definition. It bundles three data: an equivalence of carriers, a zero-preservation equation, and a pointwise step-commutation equation. Downstream code projects out the underlying Peano homomorphism via the companion toHom constructor (same zero and step fields, forgetting invertibility).
why it matters
This is the type-level upgrade from bare carrier bijection to Peano-algebra isomorphism in the Universal Forcing extraction layer. It is the return type of the canonical map between forced arithmetics of any two realizations, and the domain type of the uniqueness theorem: any two such structure-preserving isomorphisms between the same forced pair have the same underlying function.
It feeds the Universal Forcing isomorphism certificate (existence plus uniqueness, quantified over all realizations) and the parallel strict-realization certificate and uniqueness theorem. The module doc is explicit that this closes the gap only at the Peano-algebra layer: ring operations and order are not yet in the Peano object, so ordered-semiring isomorphism remains open Part II work.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.