positiveRatio_strict_equiv_existing
plain-language theorem explainer
This definition shows that the arithmetic carrier forced by the strict positive-ratio realization coincides with that from the existing positive-ratio wrapper through an equivalence of their initial Peano objects. Workers unifying strict and lightweight logic realizations in the Recognition framework cite it for consistency checks. The proof applies the natural equivalence between initial Peano objects supplied by ArithmeticOf.
Claim. Let $C$ be a comparison operator on positive reals and $h$ a proof that it satisfies the laws of logic. Then the carrier of the Peano object in the arithmetic forced by the strict positive-ratio realization of $C$ is equivalent to the carrier in the arithmetic of the logic realization obtained from the positive-ratio comparison of $C$.
background
ComparisonOperator is a map from pairs of positive reals to reals that returns the cost of comparing them. SatisfiesLawsOfLogic requires the operator to obey identity, non-contradiction, excluded middle, scale invariance, and route independence. ArithmeticOf packages a Peano object with a proof that it is initial. The upstream lemma equivOfInitial supplies the canonical isomorphism between any two initial Peano objects. This declaration lives in the Strict.PositiveRatio module, which builds a strict continuous positive-ratio realization directly from a SatisfiesLawsOfLogic instance.
proof idea
The definition is a one-line wrapper that invokes ArithmeticOf.equivOfInitial on the arithmetic object extracted from the strict realization and the arithmetic object extracted from the universal forcing of the positive-ratio logic realization.
why it matters
The equivalence confirms that the strict-derived lightweight realization produces the same forced arithmetic as the existing positive-ratio wrapper. It closes a consistency gap between strict and non-strict construction paths in the foundation layer. The result supports deriving arithmetic from functional equations without introducing discrepancies between alternative realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.