discrete_arith_equiv_logicNat
plain-language theorem explainer
This definition supplies an equivalence between the Peano carrier of the arithmetic extracted from the discrete Boolean realization and the inductive type of natural numbers forced by the law of logic. Researchers tracing the universal forcing chain would cite it when identifying the extracted naturals with the orbit structure. The definition is realized as a direct reference to the orbit equivalence supplied by the discrete realization.
Claim. The carrier of the Peano structure in the arithmetic object induced by the discrete Boolean realization is equivalent to the inductive type of natural numbers forced by the law of logic.
background
The discrete realization is the Boolean or propositional realization of the law of logic. The arithmeticOf construction extracts the forced arithmetic object from any law-of-logic realization. LogicNat is the inductive type with identity constructor for the zero-cost multiplicative identity element and step constructor for one iteration of the generator, forming the smallest subset of positive reals closed under multiplication by the generator and containing the identity.
proof idea
The definition is a one-line wrapper that directly invokes the orbit equivalence supplied by the discrete realization.
why it matters
This definition completes the discrete case for the universal forcing of arithmetic and supports the theorem that arithmetic objects extracted from any two realizations coincide. It anchors the foundation where the law of logic forces the natural numbers via the propositional realization, consistent with the forcing chain landmarks.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.