realizationPeano
plain-language theorem explainer
This definition assembles a Peano algebra directly from the orbit data of any logic realization by setting the carrier to the orbit, the zero element to the orbit zero, and the successor to the orbit step. Researchers extracting arithmetic from law-of-logic models in the Recognition Science framework cite it as the concrete initial object supplied by each realization. The construction is a direct record definition that populates the three PeanoObject fields from the realization's supplied identity-step data.
Claim. Given a logic realization $R$, the Peano algebra $P_R$ has underlying set equal to the orbit of $R$, zero element equal to the orbit zero of $R$, and successor map equal to the orbit step of $R$.
background
A PeanoObject is a structure consisting of a carrier type together with a distinguished zero element and a successor map. A LogicRealization supplies a carrier, a zero-cost element, a comparison cost, and a generator action whose orbit yields the arithmetic data. The module extracts arithmetic from any abstract law-of-logic realization; the key mechanism is that the identity-step data forces an initial Peano algebra unique up to unique isomorphism, which underpins Universal Forcing.
proof idea
One-line record definition that directly populates the PeanoObject fields using the orbit, orbitZero, and orbitStep components already present in the realization.
why it matters
This supplies the concrete Peano algebra that feeds realization_initial (which proves initiality) and extracted (which packages the full arithmetic). It realizes the initial object generated by the identity-step data, the central mechanism behind Universal Forcing. The construction closes the extraction step in the arithmetic-of-logic pipeline.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.