morphism
plain-language theorem explainer
Packages the data of a structure-preserving map between arithmetic objects forced by two Law-of-Logic realizations. Anyone proving uniqueness of the forced Peano carrier, zero, or step map cites this type. It is a pure structure definition: fields only, no proof obligations beyond what the fields already state.
Claim. A morphism between the arithmetic objects forced by two Law-of-Logic realizations is a map of their Peano carriers that is compatible with the forced zero and successor data (the initial-algebra structure extracted from each realization).
background
A Law-of-Logic realization supplies a carrier, a comparison cost, a distinguished zero, and a step/generator action, together with the structural laws the Universal Forcing program needs. The invariant target is not the ambient carrier; it is the arithmetic object extracted from the identity/step data.
That extracted object is an ArithmeticOf package: a Peano algebra together with an initiality witness. Initiality is data (a lift of the algebra to any other Peano object, plus uniqueness of the underlying function), so uniqueness of maps out of the forced arithmetic is available as structure rather than as a separate theorem.
Between two such initial Peano objects one already has a natural equivalence of carriers built by lifting each way. The present morphism type is the local language in CanonicalForcing for talking about those structure-preserving comparisons, including the universe pinning needed so that uniqueness statements type-check across realizations.
proof idea
No proof body: this is a structure declaration. It records the map data (and the zero/step preservation obligations as fields) used by the surrounding uniqueness lemmas. Downstream results such as uniqueness of the forcing map and of the forcing equivalence consume inhabitants of this type rather than re-deriving the field layout.
why it matters
CanonicalForcing is the hub that turns Law-of-Logic realizations into a unique arithmetic object. This morphism type is the comparison arrow in that hub: siblings such as uniqueness of the forcing map, the forcing equivalence, and the universal forcing map are stated in its language.
Downstream it is consumed widely. Cost-algebra uniqueness in clean Aczél form (T5: the canonical cost is $J$) and the cost-algebra morphism structure sit on the same forcing spine. Foundation results that close the nothing-to-distinction-to-arithmetic arc also mention it, so the type is load-bearing for the claim that arithmetic is forced rather than chosen.
In the broader RS chain this is pre-physics scaffolding for T5 J-uniqueness and the Recognition Composition Law: without a rigid notion of morphism between forced arithmetic objects, uniqueness of the cost functional cannot even be stated cleanly.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.