IndisputableMonolith.Foundation.UniversalForcing.CanonicalForcing
Canonical forcing packages the unique morphism from the initial Peano algebra of a Law-of-Logic realization into any other realization of the same arithmetic data. Anyone citing Universal Forcing uniqueness, zero/step preservation, or the forced arithmetic object uses this layer. The argument is initiality plus uniqueness of the induced map on the generated orbit.
claimGiven a strict (or general) realization of the Law of Logic, there is a unique structure-preserving map from the initial Peano algebra generated by identity and step into any other realization of the same data. That map sends zero to zero and step to step, and any two such maps coincide; the induced equivalence of initial objects is therefore unique.
background
Recognition Science extracts arithmetic from an abstract Law-of-Logic realization. Once a realization supplies identity and step, the forced arithmetic object is the initial Peano algebra on that data. Initial objects are unique up to unique isomorphism; that is the mechanism behind Universal Forcing (ArithmeticOf).
StrictRealization tightens the interface: a strict realization supplies only native comparison and forbids carrying an internal orbit as a free field, so the main theorem path cannot smuggle in a pre-chosen copy of the naturals. CanonicalForcing sits on top of those two modules and names the forced maps, their uniqueness, and the zero/step preservation lemmas that make the initiality argument usable downstream.
Sibling material in the module covers both the general realization case (forcing map uniqueness, equivalence uniqueness) and the universal/strict case (universal objective, universal forcing uniqueness and iff characterizations).
proof idea
The module is a thin uniqueness layer over initiality, not a single monolithic proof. Zero and step preservation for the equivalence of initial objects are proved by the universal property of the generated Peano algebra. Uniqueness of the forcing map (and of the induced equivalence) is the standard initial-object argument: any two morphisms out of the initial algebra that preserve identity and step agree on the whole orbit. Universal variants repeat the same pattern under the strict-realization interface, with iff forms packaging the characterizing equations.
why it matters in Recognition Science
This module is the named home of the canonical forcing maps that make Universal Forcing a concrete Lean object rather than a slogan. DistinctionToArithmetic imports it to weld the distinction-side analysis to a forced ArithmeticOf and prove canonicity, filling the program register item on unification from distinction (L5). ForcedSemiring imports it to equip the forced arithmetic with semiring structure on the same unique skeleton.
In the broader foundation chain, unique initial arithmetic is what later forces the discrete tick structure and the eight-tick octave (T7) once the self-similar fixed point and dimension constraints are in place. Without a unique zero/step-preserving map, downstream claims that every realization sees the same arithmetic would be only informal.
scope and limits
- Does not construct physical constants, masses, or the J-cost functional.
- Does not by itself force dimension D = 3 or the eight-tick period.
- Does not prove existence of a realization; it assumes realization data and forces the map.
- Does not define the distinction-to-arithmetic bridge; that lives downstream.
- Does not equip the forced object with full semiring axioms; ForcedSemiring does.
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