strictPositiveRatio_arith_equiv_strictBoolean
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.
claimLet $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 in Recognition Science
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.
scope and limits
- Does not address non-strict realizations or finite Boolean images.
- Does not supply an explicit isomorphism beyond the initiality lift.
- Does not compute numerical values or concrete elements of the carriers.
- Does not extend to realizations that violate scale invariance.
formal statement (Lean)
60noncomputable def strictPositiveRatio_arith_equiv_strictBoolean
61 (C : ComparisonOperator) (h : SatisfiesLawsOfLogic C) :
62 (StrictLogicRealization.arith (PositiveRatio.strictPositiveRatioRealization C h)).peano.carrier
63 ≃ (StrictLogicRealization.arith strictBooleanRealization).peano.carrier :=
proof body
Definition body.
64 ArithmeticOf.equivOfInitial
65 (StrictLogicRealization.arith (PositiveRatio.strictPositiveRatioRealization C h))
66 (StrictLogicRealization.arith strictBooleanRealization)
67
68end DiscreteBoolean
69end Strict
70end UniversalForcing
71end Foundation
72end IndisputableMonolith