physics_arithmetic_invariant
plain-language theorem explainer
The physics realization extracts an arithmetic object whose Peano carrier is equivalent to the Peano carrier of any other logic realization. Workers on the universal forcing chain cite this to confirm that extracted tick arithmetic is independent of the choice of realization. The definition is a one-line wrapper invoking the equivalence of initial Peano objects.
Claim. Let $R$ be any logic realization. The carrier of the Peano object extracted from the physics realization is equivalent to the carrier of the Peano object extracted from $R$.
background
LogicRealization supplies a carrier type, a cost type equipped with zero, a compare function between carriers, and a zero element, together with the structural laws required by universal forcing. ArithmeticOf R is the arithmetic object forced by such a realization; it contains a PeanoObject that is initial. physicsRealization is the concrete skeleton with PhysicsState as carrier, natural numbers as cost, and physicsCost as the comparison map. The module supplies a stable lightweight interface for the physics segment of the forcing chain, using identity ticks as the step action and recognition states as the carrier. Upstream, equivOfInitial constructs the canonical equivalence between any two initial Peano objects by mutual lifting.
proof idea
This definition is a one-line wrapper that applies ArithmeticOf.equivOfInitial to the arithmetic objects extracted from physicsRealization and from R.
why it matters
The definition records that the arithmetic extracted from the physics realization is invariant across all logic realizations, supplying the stable interface for the physics forcing chain described in the module documentation. It closes the extraction step in the universal forcing program by showing that the Peano carrier is canonical up to equivalence. It touches the open question of how physical arithmetic emerges invariantly from the underlying logic structure.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.