strictOrdered_arith_equiv_logicNat
plain-language theorem explainer
The definition supplies an equivalence between the Peano carrier extracted from the arithmetic of the strict ordered integer realization and the inductive LogicNat type. Researchers deriving natural-number structure from the Law of Logic in the forcing chain would cite this equivalence to confirm that the integer model reproduces the expected orbit. The proof is a one-line wrapper that invokes the orbit equivalence supplied by the lightweight realization of the same strict ordered data.
Claim. The carrier of the Peano arithmetic extracted from the strict ordered realization on integers is equivalent to the inductive type LogicNat.
background
A StrictLogicRealization consists of a carrier type, a cost type with zero, a compare function, and a compose operation; the supplied strictOrderedRealization instantiates this on carrier ℤ, cost ℕ, compare given by intCost, and compose given by addition. The arith function then extracts an ArithmeticOf structure from the lightweight version of any such realization. LogicNat is the inductive type with constructors identity (zero-cost unit) and step, whose orbit under the generator mirrors the positive reals closed under multiplication by the fixed point γ.
proof idea
One-line wrapper that applies the orbitEquivLogicNat field of the lightweight realization obtained from strictOrderedRealization.
why it matters
The equivalence confirms that every strict ordered realization canonically recovers the LogicNat structure forced by the Law of Logic, thereby closing one link in the derivation of arithmetic from the recognition functional equation. It sits inside the strict-realization layer that precedes the extraction of Peano arithmetic and the subsequent mass-ladder constructions.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.