arith_continuous_equiv_arith_discrete
plain-language theorem explainer
Continuous positive-ratio arithmetic is canonically equivalent to discrete Boolean arithmetic via a natural isomorphism of their Peano carriers. Researchers verifying invariance properties in Recognition Science would cite this when showing that distinct realizations of the laws of logic induce isomorphic arithmetic. The construction is a one-line wrapper invoking the general equivalence between any two initial Peano objects.
Claim. Let $C$ be a comparison operator satisfying the laws of logic. The carrier set of the Peano object induced by the continuous realization of $C$ is canonically equivalent to the carrier set of the Peano object induced by the discrete realization.
background
ComparisonOperator is a map from pairs of positive reals to reals that assigns a comparison cost, subject to the four Aristotelian constraints plus scale invariance. SatisfiesLawsOfLogic is the structure asserting that a given operator obeys identity, non-contradiction, excluded middle, scale invariance, and route independence. ArithmeticOf is the structure that packages a PeanoObject together with a proof that the object is initial among all Peano objects. The module TwoCases records the first invariance kernel between continuous positive-ratio realizations and the discrete Boolean realization, showing that their forced arithmetic objects are equivalent.
proof idea
The definition is a one-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic object coming from the continuous realization of C and the arithmetic object coming from the discrete realization.
why it matters
This supplies the canonical equivalence at the core of the invariance kernel between continuous and discrete realizations. It fills the first non-trivial step recorded in the module documentation for UniversalForcing.Invariance.TwoCases. Within the Recognition Science framework it supports the independence of the forced arithmetic from the choice of realization, consistent with the uniqueness of J and the phi-ladder construction. No open questions are closed here.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.