IndisputableMonolith.Foundation.UniversalForcing.Strict.CanonicalIso
For any two strict Law-of-Logic realizations, the forced arithmetic carriers are not merely in bijection: the map is a Peano-algebra isomorphism, sending zero to zero and commuting with successor. Anyone citing strict universal forcing as structure-preserving arithmetic uniqueness lands here. The module lifts the bare carrier equivalence from the non-strict CanonicalIso layer through the strict invariance theorem.
claimIf $R$ and $S$ are strict Law-of-Logic realizations, the canonical bijection between their forced Peano carriers is a Peano-algebra isomorphism: it sends $0_R$ to $0_S$ and intertwines the successor maps, $f\circ S_R = S_S\circ f$. Uniqueness of that structure-preserving equivalence is recorded alongside a certificate packaging the result.
background
Universal Forcing extracts arithmetic from Law-of-Logic realizations. The non-strict spine already yields a bare carrier bijection between forced Peano carriers of any two realizations; CanonicalIso is the arithmetic-extraction layer that upgrades that bijection toward algebraic structure.
The strict branch works with native Law-of-Logic data that determine a derived free orbit. Strict Invariance states that all such derived free orbits are canonically equivalent. This module sits at the junction: it takes that strict equivalence and the non-strict canonical-iso machinery and specializes to structure-preserving Peano maps.
A Peano algebra here means a carrier with a distinguished zero and a successor operation. Structure preservation is exactly $f(0)=0$ and $f\circ S = S'\circ f$. Sibling names in the module package the equivalence, its uniqueness, and a certificate form of the claim.
proof idea
The module is an assembly layer, not a single free-standing proof. It imports Strict.Invariance (canonical equivalence of derived free orbits under strict Law-of-Logic data) and the non-strict CanonicalIso arithmetic-extraction layer (bare carrier bijections between forced arithmetics).
The main declarations specialize those ingredients to strict realizations: construct the Peano equivalence so that zero and successor are preserved, prove uniqueness of that structure map, and wrap the pair into a certificate object. Expect the argument shape to be: obtain the strict orbit equivalence, transport along the canonical arithmetic extraction, then verify the two Peano homomorphism identities and uniqueness by the universal property of the free orbit.
why it matters in Recognition Science
Strict universal forcing is the claim that Law-of-Logic data force not only a unique arithmetic carrier but a unique Peano algebra structure. Without zero-and-successor preservation, "forced arithmetic" is only a set bijection; with it, induction, numerals, and successor recursion transfer between realizations.
This module is the structure-preserving form of that theorem inside the Strict Universal Forcing branch. It closes the gap left by the bare-carrier story in Universal Forcing Part II: the bijection becomes an isomorphism of Peano algebras. Downstream consumers (none linked yet in the graph) would cite it whenever a proof needs to move arithmetic identities, not merely elements, across two strict realizations.
In the broader Recognition forcing chain, this is foundation-level uniqueness infrastructure: once Peano structure is forced and unique up to unique iso, later extractions (octave period, dimension counts, cost functionals) sit on a single arithmetic skeleton rather than on ad hoc encodings.
scope and limits
- Does not treat non-strict Law-of-Logic realizations; only the strict branch.
- Does not derive physical constants, J-cost identities, or the T0–T8 forcing chain steps.
- Does not construct arithmetic from scratch; it upgrades an existing carrier equivalence to a Peano iso.
- Does not assert computational decidability or an executable numeral embedding.
- Used-by graph is empty here; no downstream theorem is pinned by the supplied edges.