IndisputableMonolith.Foundation.UniversalForcing.CanonicalSemiringIso
Packages the canonical fold from any Law-of-Logic realization's forced arithmetic onto the reference LogicNat as a Peano homomorphism. Supplies forced zero, one, addition, multiplication, and order, plus compatibility of the fold with the bare carrier iso from CanonicalIso. Anyone extracting a unique semiring structure from universal forcing cites this layer. The argument is definitional packaging of the fold map and pointwise iso-commutation lemmas.
claimFor a Law-of-Logic realization $R$, the forced arithmetic on $R$ folds onto the reference $\mathrm{LogicNat}$ via a Peano homomorphism $\mathrm{fold}: (\mathrm{arithmeticOf}\, R).\mathrm{carrier} \to \mathrm{LogicNat}$ that preserves $0$, $1$, $+$, $\cdot$, and $\le$. This fold is compatible with the bare carrier bijection of CanonicalIso: isomorphisms of forced arithmetics commute with fold.
background
Universal Forcing extracts arithmetic from any realization of the Law of Logic. Part I yields a bare carrier bijection between the Peano carriers of any two realizations. CanonicalIso (Part II) is the arithmetic-extraction layer that turns that spine into comparable forced arithmetics; its module doc states that the existing spine produces only a carrier equivalence $(\mathrm{arithmeticOf}, R).\mathrm{peano.carrier} \simeq (\mathrm{arithmeticOf}, S).\mathrm{peano.carrier}$.
This module sits one step further: it names the forced constants and operations (zero, one, add, mul, le) on a realization and packages the canonical fold of that structure onto the fixed reference $\mathrm{LogicNat}$ as a Peano homomorphism. The fold is the concrete map that identifies every forced natural with its standard counterpart, so uniqueness of arithmetic becomes a homomorphism statement rather than a bare bijection.
proof idea
Definition-and-compatibility module rather than a single deep proof. It introduces the forced arithmetic operations as named maps, defines the fold homomorphism into LogicNat (with an explicit toFun projection), then proves pointwise that the CanonicalIso carrier equivalence intertwines forced zero, one, add, and mul with their images under fold. The fold-iso compatibility lemma is the structural glue: transporting along the bare iso and then folding equals folding on each side. No independent forcing argument is re-run here; the work is packaging and commutation.
why it matters in Recognition Science
Closes the gap between bare carrier bijections and a usable unique semiring of naturals inside the Universal Forcing spine. Downstream work that needs actual arithmetic (not just equipotence of carriers) depends on having forced $0,1,+, imes$ and a canonical Peano fold onto LogicNat. In the broader Recognition framework this is foundation infrastructure for the forcing chain: once arithmetic is uniquely folded, later steps that force $\varphi$, the eight-tick octave, and $D=3$ can treat the naturals as the standard ones. The module currently has no recorded used_by edges in the graph, so it is a leaf packaging layer awaiting consumers that quote the fold homomorphism or the iso-commutation lemmas.
scope and limits
- Does not re-prove universal forcing or construct the bare carrier bijection; that lives in CanonicalIso and above.
- Does not force physical constants, $\varphi$, dimension, or the eight-tick period.
- Does not claim a unique semiring beyond Peano structure folded onto LogicNat.
- Does not supply computational evaluation or decidability results for the forced operations.
- Does not identify which downstream theorems currently import these fold maps.
depends on (1)
declarations in this module (15)
-
def
foldHom -
theorem
foldHom_toFun -
theorem
fold_iso_compat -
def
forcedZero -
def
forcedOne -
def
forcedAdd -
def
forcedMul -
def
forcedLe -
theorem
iso_map_forcedZero -
theorem
iso_map_forcedOne -
theorem
iso_map_forcedAdd -
theorem
iso_map_forcedMul -
theorem
iso_map_forcedLe -
structure
ForcedOrderedSemiringIsoCert -
def
forcedOrderedSemiringIsoCert