extracted_peanoSurface
plain-language theorem explainer
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.
Claim. Let $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
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.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.
papers checked against this theorem (showing 1 of 1)
-
Two-level atom dynamics run classical logic as finite-state machines
"superevolution matrix... mimics a parity checker, a class of finite-state machine (FSM)"