continuous_positive_ratio_arithmetic_invariant
plain-language theorem explainer
Any two realizations of the laws of logic induce canonically equivalent forced arithmetic on their Peano carriers. Researchers working on the universal forcing theorem cite this to establish that arithmetic is independent of the choice of realization. The definition is a direct one-line application of the equivalence between any two initial Peano objects.
Claim. Let $C$ be a comparison operator satisfying the laws of logic and let $S$ be any logic realization. The carrier of the Peano algebra forced by the arithmetic object of the positive-ratio realization induced by $C$ is equivalent to the carrier of the Peano algebra forced by $S$.
background
A logic realization supplies a model of the laws of logic through a comparison operator. The arithmetic object attached to each realization consists of a Peano algebra together with a proof that the algebra is initial among all Peano algebras. The universal forcing theorem asserts that any two such realizations therefore yield equivalent arithmetic objects, because initial objects are unique up to unique isomorphism.
proof idea
This definition is a one-line wrapper that applies the equivalence of initial Peano objects to the arithmetic structures induced by the positive-ratio realization and by the arbitrary realization $S$.
why it matters
The declaration supplies the invariance statement at the heart of the universal forcing theorem in the Foundation module. It shows that forced arithmetic is the same for every realization because each Peano carrier is initial, thereby closing the gap between distinct logic models and confirming that arithmetic is uniquely determined by the laws of logic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.