IndisputableMonolith.Foundation.UniversalForcing.CanonicalForcing
Canonical forcing records the unique Peano-algebra morphism out of the arithmetic object forced by a Law-of-Logic realization. Anyone proving Universal Forcing uniqueness, or wiring distinction data into a forced arithmetic carrier, cites this layer. The proofs are initiality plus uniqueness of the zero-and-step-preserving map (and its equivalence form).
claimFrom the initial Peano algebra forced by a logic realization $R$, there is a unique morphism into any other carrier of the same identity and successor data. That forcing map sends zero to zero and commutes with the step; the induced equivalence of initial objects is unique up to unique isomorphism.
background
Universal Forcing rests on initiality. Once a realization supplies identity and step data, ArithmeticOf extracts the forced arithmetic object: the initial Peano algebra generated by that data. Initial objects are unique up to unique isomorphism; that is the mechanism behind the forcing theorems.
The strict realization interface tightens the older lightweight one. A strict realization supplies only native comparison structure and does not carry an internal orbit as a field, so the main theorem path cannot smuggle a pre-chosen copy of the naturals past the uniqueness argument.
This module sits between those two imports. It names the canonical morphism out of the forced arithmetic object, the zero and step preservation lemmas for that map, and the uniqueness and iff characterizations of both the map and the induced equivalence.
proof idea
The module is a short uniqueness layer, not a definition dump. It builds the forcing morphism from initiality of the arithmetic object, then proves zero preservation and step commutation by the universal property of that initial algebra.
Uniqueness of the map (and of the equivalence of initial objects) is the standard initial-object argument: any two zero-and-step morphisms agree by induction along the forced carrier. Parallel lemmas are stated once for general realizations and again in the universal-forcing packaging used downstream. Several results are thin wrappers that restate the same uniqueness in iff or equivalence form.
why it matters in Recognition Science
This is the canonical-morphism spine of the Universal Forcing program in the Foundation domain. Downstream, DistinctionToArithmetic imports it to weld the distinction-side analysis to a forced ArithmeticOf and to prove that object is canonical (the L5 register item: native analysis and unification from distinction).
ForcedSemiring also imports the module, so the unique forcing map is available when the forced arithmetic carrier is promoted to semiring structure. Without unique zero-and-step morphisms out of the initial object, later claims that physics constants or mass ladders sit on a single forced arithmetic backbone would not be well-defined up to unique isomorphism.
scope and limits
- Does not construct ArithmeticOf; that lives in the imported arithmetic module.
- Does not itself weld distinction data to arithmetic; DistinctionToArithmetic does that.
- Does not force physical constants, phi, or spacetime dimension.
- Does not replace StrictRealization; it consumes that interface.
- Does not claim uniqueness without matching identity and step data.
used by (2)
depends on (2)
declarations in this module (14)
-
structure
morphism -
theorem
equivOfInitial_map_zero -
theorem
equivOfInitial_map_step -
theorem
forcing_map_unique -
theorem
forcing_map_iff -
theorem
forcing_equiv_unique -
theorem
universal_objective -
theorem
universal_forcing_map_zero -
theorem
universal_forcing_map_step -
theorem
universal_forcing_unique -
theorem
universal_forcing_iff -
theorem
universal_forcing_equiv_unique -
structure
CanonicalForcingCert -
def
canonicalForcingCert_holds