strictPositiveRatio_arith_equiv_strictBoolean
plain-language theorem explainer
Positive ratios and Boolean propositions induce equivalent arithmetic carriers when both realizations satisfy the laws of logic. Researchers tracing cross-realization invariance in the Recognition framework cite this as the first strict invariance result. The definition is obtained by direct application of the natural equivalence between any two initial Peano objects.
Claim. Let $C$ be a comparison operator satisfying the laws of logic. Then the carrier of the Peano object in the arithmetic induced by the strict positive-ratio realization of $C$ is equivalent to the carrier of the Peano object in the arithmetic induced by the strict Boolean realization.
background
ComparisonOperator denotes a map from pairs of positive reals to reals that records the cost of comparing them; SatisfiesLawsOfLogic packages the four Aristotelian constraints together with scale invariance and route independence. ArithmeticOf R packages the Peano object that is forced to be initial by any logic realization R. The module works in the strict setting, where the carrier orbit is periodic yet the forced arithmetic remains the free iteration object generated by the native step, not the finite image inside Bool. Upstream, equivOfInitial supplies the canonical equivalence between the carriers of any two initial Peano objects.
proof idea
One-line wrapper that applies ArithmeticOf.equivOfInitial to the two ArithmeticOf instances obtained from the positive-ratio realization and the strict Boolean realization.
why it matters
This definition supplies the first strict cross-realization invariance theorem, establishing that positive-ratio and Boolean realizations force identical arithmetic. It rests on the ArithmeticOf construction and the uniqueness of initial Peano objects. In the Recognition framework it closes the loop between the functional-equation treatment of logic and the forced arithmetic that appears in the T0-T8 chain, providing a concrete bridge between ratio-based and propositional realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.