peano_surface
Any strict logic realization forces an arithmetic object whose carrier obeys the Peano surface axioms. Researchers on discrete foundations cite the result to confirm that induction and successor properties hold once the orbit is derived uniformly from LogicNat. The proof is a one-line term that applies the general UniversalForcing.peano_surface theorem to the lightweight conversion of the strict realization.
claimLet $R$ be a strict logic realization. Then the arithmetic object extracted from $R$ satisfies the Peano surface: its zero differs from every successor, the successor map is injective, and the induction schema holds for every predicate on the carrier.
background
A StrictLogicRealization is a structure supplying only native data: a carrier type, a cost type with zero, a compare function, a compose operation, distinguished elements one and generator, plus laws that compare(x,x)=0 and compare(x,y)=compare(y,x). The arith definition extracts ArithmeticOf from the lightweight LogicRealization produced by toLightweight, which derives all orbit fields from LogicNat rather than accepting them from the caller.
proof idea
The proof is a direct term that invokes UniversalForcing.peano_surface on the result of toLightweight R. This converts the strict interface into a standard LogicRealization whose forced arithmetic is already known to carry the Peano surface.
why it matters in Recognition Science
The theorem closes the strict interface to the universal forcing path, ensuring every strict realization inherits the Peano surface without an explicit orbit field. It is invoked by strict_peano_surface in Strict.Invariance and by bool_peano_surface for concrete models. The result sits inside the chain that derives arithmetic axioms from the law-of-logic data alone.
scope and limits
- Does not construct an explicit carrier or cost model.
- Does not verify the surface for realizations that supply their own orbit.
- Does not address continuous or non-discrete realizations.
- Does not prove uniqueness of the forced arithmetic object.
Lean usage
theorem example (R : StrictLogicRealization) : ArithmeticOf.PeanoSurface (arith R) := peano_surface Rformal statement (Lean)
110theorem peano_surface (R : StrictLogicRealization) :
111 ArithmeticOf.PeanoSurface (arith R) :=
proof body
Term-mode proof.
112 UniversalForcing.peano_surface (toLightweight R)
113
114end StrictLogicRealization
115
116end Strict
117end UniversalForcing
118end Foundation
119end IndisputableMonolith