bool_arithmetic_invariant
plain-language theorem explainer
The Boolean realization of the Law of Logic forces an arithmetic whose Peano carrier is equivalent to that of any other realization. Researchers working on discrete models of logic cite this to confirm the Boolean case sits inside the universal forcing framework without new arithmetic structure. The definition is a one-line wrapper that applies the equivalence of initial Peano objects.
Claim. Let $R$ be any Law-of-Logic realization. The Peano carrier of the arithmetic object forced by the Boolean realization is equivalent to the Peano carrier of the arithmetic object forced by $R$.
background
LogicRealization supplies a carrier set, cost function, and zero element that together realize the Law of Logic. ArithmeticOf packages the Peano object forced by any such realization together with a proof that the object is initial. boolRealization is the concrete discrete case whose carrier is Bool and whose cost is Nat, serving as the first non-continuous test case for Universal Forcing. equivOfInitial constructs the canonical equivalence between the carriers of any two initial Peano objects by lifting each through the other's initiality map.
proof idea
One-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic objects of boolRealization and R.
why it matters
This definition shows that the discrete Boolean realization induces the same Peano carrier as every other realization under Universal Forcing. It supports the claim that the Boolean case is a valid test for the forcing chain without deviating in arithmetic structure. It connects to the broader framework in which all realizations share an initial Peano object up to equivalence.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.