Foundation Universal Forcing Canonical Semiring Iso

The arithmetic that cannot vary

An isomorphism is a dictionary that translates between two mathematical structures without losing any information. The canonical semiring isomorphism in Recognition Science is the strongest such dictionary yet proved: it says that any two realizations of the framework's fundamental laws not only have the same shape, but also agree on their arithmetic. If one universe's counting behaves like 2 + 2 = 4, the other's must too, under a translation that preserves every operation.

The framework begins with a ledger, a discrete record of recognition events, and forces a cost function J(x) = (x + 1/x)/2 - 1 from five plain conditions. Earlier work showed that any two ledgers forced by these laws are linked by a unique structure-preserving map, one that respects the idea of a starting point and the act of moving to the next step. The result goes further. It proves that the same canonical map also respects the arithmetic those steps determine: the constants 0 and 1, the operations of addition and multiplication, and the ordering that says one number comes before another.

The proof works by folding every forced structure onto a single reference object, LogicNat, which already carries the recovered arithmetic. The key lemma, fold_iso_compat, shows that the canonical map composed with one structure's fold equals the other's fold directly. Since both are homomorphisms from an initial object, they must be identical. From that single fact, the preservation of 0, 1, +, ×, and ≤ follows by routine algebra. The result is a certificate, ForcedOrderedSemiringIsoCert, that packages all five preservation properties into one statement.

In Recognition Science, this means the arithmetic of counting is not an assumption but a consequence. Any two universes that obey the framework's laws must share the same natural-number arithmetic, canonically and uniquely. The result establishes this at the element level, without bundling the structures as typeclass instances, which is a separate enrichment not needed for the forcing statement. The practical payoff: the framework's derived physics, including its constants and particle ladder, rests on arithmetic that cannot vary between realizations.

/-- **Universal Forcing ordered-semiring isomorphism certificate.**

For any two Law-of-Logic realizations, the canonical isomorphism between their
forced arithmetics preserves `0`, `1`, addition, multiplication, and the order.
Together with `UniversalForcingIsoCert` (zero/successor preservation and
uniqueness) this says the forced arithmetics are isomorphic as ordered
commutative semirings, canonically, across all realizations. -/
structure ForcedOrderedSemiringIsoCert where
  preserves_zero : ∀ (R S : LogicRealization.{0, 0}),
    (universalForcingPeanoEquiv R S).toEquiv (forcedZero R) = forcedZero S
  preserves_one : ∀ (R S : LogicRealization.{0, 0}),
    (universalForcingPeanoEquiv R S).toEquiv (forcedOne R) = forcedOne S
  preserves_add : ∀ (R S : LogicRealization.{0, 0}) (a b : (forcedArith R).peano.carrier),
    (universalForcingPeanoEquiv R S).toEquiv (forcedAdd R a b)
      = forcedAdd S ((universalForcingPeanoEquiv R S).toEquiv a)
          ((universalForcingPeanoEquiv R S).toEquiv b)
  preserves_mul : ∀ (R S : LogicRealization.{0, 0}) (a b : (forcedArith R).peano.carrier),
    (universalForcingPeanoEquiv R S).toEquiv (forcedMul R a b)
      = forcedMul S ((universalForcingPeanoEquiv R S).toEquiv a)
          ((universalForcingPeanoEquiv R S).toEquiv b)
  preserves_le : ∀ (R S : LogicRealization.{0, 0}) (a b : (forcedArith R).peano.carrier),
    forcedLe R a b
      ↔ forcedLe S ((universalForcingPeanoEquiv R S).toEquiv a)
          ((universalForcingPeanoEquiv R S).toEquiv b)

/-- The ordered-semiring isomorphism certificate is inhabited. -/
noncomputable def forcedOrderedSemiringIsoCert : ForcedOrderedSemiringIsoCert where
  preserves_zero := fun R S => iso_map_forcedZero R S
  preserves_one := fun R S => iso_map_forcedOne R S
  preserves_add := fun R S => iso_map_forcedAdd R S
  preserves_mul := fun R S => iso_map_forcedMul R S
  preserves_le := fun R S => iso_map_forcedLe R S

/-- **Fold compatibility (pure initiality).**  The universal forcing isomorphism
`R ⥲ S`, followed by `S`'s fold onto `LogicNat`, equals `R`'s fold onto
`LogicNat`.  Both are Peano homomorphisms out of the initial forced arithmetic of
`R`, so initiality forces them equal. -/
theorem fold_iso_compat (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w})
    (x : (forcedArith R).peano.carrier) :
    S.orbitEquivLogicNat ((universalForcingPeanoEquiv R S).toEquiv x)
      = R.orbitEquivLogicNat x := by
  have h := (forcedArith R).initial.uniq logicNatPeano
    (PeanoObject.Hom.comp (foldHom S) (universalForcingPeanoEquiv R S).toHom)
    (foldHom R)
  exact congrFun h x

/-- Forced addition (transported `+` on `LogicNat`). -/
noncomputable def forcedAdd (R : LogicRealization.{0, v})
    (a b : (forcedArith R).peano.carrier) : (forcedArith R).peano.carrier :=
  R.orbitEquivLogicNat.symm (R.orbitEquivLogicNat a + R.orbitEquivLogicNat b)

/-- Forced multiplication (transported `×` on `LogicNat`). -/
noncomputable def forcedMul (R : LogicRealization.{0, v})
    (a b : (forcedArith R).peano.carrier) : (forcedArith R).peano.carrier :=
  R.orbitEquivLogicNat.symm (R.orbitEquivLogicNat a * R.orbitEquivLogicNat b)

What this page does not claim

This result does not bundle LogicNat or the carriers as Mathlib OrderedCommSemiring typeclass instances. The proof does not establish the forcing conditions themselves; it assumes realizations satisfying them. The isomorphism does not depend on any particular choice of cost function beyond the five plain conditions.

Verify this page

Every tagged claim above names its theorem. To check one yourself rather than trust this page, elaborate the source module with Lean 4 and audit its axiom basis:

$ lake env lean IndisputableMonolith/Foundation/UniversalForcing/CanonicalSemiringIso.lean
expected axiom basis: [propext, Classical.choice, Quot.sound] (the Lean kernel's standard three; no RS-specific axioms)

A page whose claims cannot be reproduced this way does not ship. In production, every anchor links to the exact declaration in the public source release, and this block carries the build receipt for the page itself.

Derived articles

This page is generated by a question-recursion engine: the questions its answers raise become the next pages. The current agenda, with open targets marked red: