continuous_arith_equiv_logicNat
plain-language theorem explainer
Continuous realizations of the law of logic induce an arithmetic structure whose Peano carrier is equivalent to the natural numbers generated by the law of logic. Researchers formalizing the Recognition Science forcing chain would cite this when confirming that the continuous positive-ratio case preserves the discrete arithmetic extracted from any valid comparison operator. The implementation is a one-line wrapper delegating directly to the orbit equivalence supplied by the continuous realization.
Claim. Let $C$ be a comparison operator on positive reals satisfying the laws of logic. Then the Peano carrier of the arithmetic object extracted from the continuous realization of $C$ is equivalent to the inductive type of natural numbers forced by the law of logic.
background
ComparisonOperator is the type of functions from pairs of positive reals to reals that assign a comparison cost. SatisfiesLawsOfLogic is the structure asserting the four Aristotelian constraints (identity, non-contradiction, excluded middle, route independence) together with scale invariance and non-triviality. LogicNat is the inductive type whose constructors are identity (the zero-cost multiplicative unit) and step (one further iteration of the generator), forming the smallest subset of positive reals closed under multiplication by the generator and containing the unit.
proof idea
The definition is a one-line wrapper that returns the orbitEquivLogicNat field of the continuous realization applied to the given comparison operator and its law-satisfaction hypothesis.
why it matters
The definition shows that the continuous realization carries the universal forced arithmetic, directly supporting the arithmeticOf extraction in UniversalForcing. It closes the link between the continuous positive-ratio wrapper and the LogicNat type that appears in the forcing chain from logic to arithmetic. No downstream uses are recorded, leaving open whether this equivalence will be invoked in later steps that extract physical constants or mass ladders from the same realization.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.