extracted_peanoSurface
The theorem shows that arithmetic extracted from any LogicRealization satisfies the three Peano surface axioms. Workers on the universal forcing chain cite it to confirm every realization produces a valid initial Peano algebra. The proof is a direct term-mode construction that assembles the structure fields from the realization's orbit properties.
claimLet $R$ be a LogicRealization. Let $A$ be the arithmetic object extracted from $R$. Then $A$ satisfies: zero is not equal to any successor, the successor map is injective, and the induction schema holds for every predicate on the carrier.
background
A LogicRealization supplies a carrier, comparison cost, zero element, and identity-step orbit data together with the structural propositions needed for forcing. The extracted definition builds an ArithmeticOf R by pairing the realization's Peano object with its initiality witness. PeanoSurface is the structure that packages the three Peano axioms on this arithmetic object: zero distinct from every successor, injective successor, and the full induction principle. The module extracts arithmetic from abstract realizations precisely to realize the initiality mechanism of universal forcing.
proof idea
The proof is a term-mode construction of the PeanoSurface structure. It directly supplies zero_ne_step from the realization's orbit_no_confusion field, step_injective from orbit_step_injective, and induction from orbit_induction. No further lemmas or tactics are required.
why it matters in Recognition Science
This result is invoked by the peano_surface theorem in UniversalForcing, which states that the Peano surface holds for the forced arithmetic of every realization. It supplies the concrete verification that the extracted object is initial, thereby supporting the uniqueness-up-to-isomorphism step in the forcing program. The construction rests on the initiality property already present in the realization.
scope and limits
- Does not construct an explicit carrier or cost function for any realization.
- Does not prove uniqueness of the extracted Peano object up to isomorphism.
- Does not address topology, order, or category structure supplied by the realization.
- Does not connect the arithmetic object to physical constants or dimensions.
Lean usage
theorem peano_surface (R : LogicRealization) : ArithmeticOf.PeanoSurface (arithmeticOf R) := ArithmeticOf.extracted_peanoSurface Rformal statement (Lean)
202theorem extracted_peanoSurface (R : LogicRealization) :
203 PeanoSurface (extracted R) where
204 zero_ne_step := R.orbit_no_confusion
proof body
Term-mode proof.
205 step_injective := R.orbit_step_injective
206 induction := R.orbit_induction
207
208/-- The natural equivalence between two initial Peano objects. -/