canonical_peanoSurface
plain-language theorem explainer
The canonical arithmetic object extracted from any Law-of-Logic realization satisfies the three Peano surface axioms. Researchers tracing the initiality mechanism in forced arithmetic would cite this result to confirm that the abstract construction yields a valid Peano algebra. The proof is a direct three-part tactic application that transfers the zero-distinctness, successor injectivity, and induction principle from the underlying LogicNat inductive type.
Claim. For any Law-of-Logic realization $R$, the canonical arithmetic object associated to $R$ satisfies the Peano surface: its zero element differs from every successor, its successor map is injective, and every property holding at zero and closed under successor holds for all elements.
background
ArithmeticOf extracts a Peano algebra from a LogicRealization, which supplies a carrier, zero-cost comparison, and identity element. The structure pairs a PeanoObject (carrier with zero and step) with an IsInitial witness. canonical constructs the realization-independent instance by taking logicNatPeano as the PeanoObject and logicNat_initial as the initiality proof. PeanoSurface is the Prop asserting the three standard Peano conditions on that object: zero distinct from every successor, successor injective, and the induction schema. LogicNat is the inductive type with constructors identity and step whose orbit structure directly encodes the forced natural numbers.
proof idea
The tactic proof splits into three fields. zero_ne_step proceeds by intro x h followed by cases h, which is impossible by constructor disjointness. step_injective applies the upstream theorem LogicNat.succ_injective directly. induction rewrites the motive and hands the hypotheses to LogicNat.induction, which discharges the goal by the inductive definition of LogicNat.
why it matters
This theorem closes the verification that the canonical construction (defined via logicNatPeano and logicNat_initial) meets the PeanoSurface interface required by ArithmeticOf. It therefore supplies the concrete arithmetic content that Universal Forcing extracts from any realization, confirming that initiality alone forces the standard Peano structure. The result sits inside the foundation layer that later modules use to derive mass ladders and constants without further hypotheses on 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)
-
Hardness assumption stops PV1 proving every number has a prime divisor
"By the completeness theorem, it follows that under this assumption there is a model M of PV1 that contains a nonstandard number m which has no prime factorization."