Foundation Universal Forcing Canonical Semiring Iso Iso Map Forced Le

The forced order

The natural numbers come with a built-in sense of size: 0 is less than 1, 1 is less than 2, and so on. The declaration iso_map_forcedLe is a theorem in the Recognition Science framework's machine-checked library of formal theorems. It states that this ordering is not an accident of how we happened to define the numbers. In the framework, every realization of the core law forces a copy of the natural numbers into existence, complete with its own arithmetic. The theorem proves that the canonical isomorphism between any two such copies preserves and reflects the order: if one copy says a number is at most another, the corresponding numbers in the other copy stand in the same relation.

The proof rests on a single idea, pure initiality. Each forced copy of the natural numbers folds canonically onto a reference object called LogicNat, which already carries the standard order. The theorem shows that the fold of one realization, followed by the canonical isomorphism, equals the fold of the other realization. Since both folds are homomorphisms out of an initial structure, they must agree. From that compatibility, the order preservation follows by a short algebraic argument. The same pattern proves that the isomorphism preserves zero, one, addition, and multiplication, so the forced arithmetics are isomorphic as ordered commutative semirings, canonically, across all realizations.

What the theorem does not claim is just as important. It does not claim that the framework derives the order from nothing. The order on LogicNat is taken as given, a definitional choice, not a forced consequence. The theorem also does not claim that the forced carriers are bundled as instances of a standard algebraic typeclass; that is a separate, purely LogicNat-side enrichment. Finally, the theorem says nothing about which specific numbers exist or how large they are. It only says that whatever numbers are forced, their ordering is uniquely determined up to isomorphism.

/-- **Order isomorphism.**  The canonical isomorphism preserves and reflects the
forced order. -/
theorem iso_map_forcedLe (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w})
    (a b : (forcedArith R).peano.carrier) :
    forcedLe R a b
      ↔ forcedLe S ((universalForcingPeanoEquiv R S).toEquiv a)
          ((universalForcingPeanoEquiv R S).toEquiv b) := by
  simp only [forcedLe, fold_iso_compat]

/-- The canonical isomorphism sends the forced zero to the forced zero. -/
theorem iso_map_forcedZero (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w}) :
    (universalForcingPeanoEquiv R S).toEquiv (forcedZero R) = forcedZero S := by
  apply S.orbitEquivLogicNat.injective
  simp only [forcedZero, fold_iso_compat, Equiv.apply_symm_apply]

/-- The canonical isomorphism sends the forced one to the forced one. -/
theorem iso_map_forcedOne (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w}) :
    (universalForcingPeanoEquiv R S).toEquiv (forcedOne R) = forcedOne S := by
  apply S.orbitEquivLogicNat.injective
  simp only [forcedOne, fold_iso_compat, Equiv.apply_symm_apply]

/-- **Additivity.**  The canonical isomorphism is a homomorphism for forced
addition. -/
theorem iso_map_forcedAdd (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w})
    (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) := by
  apply S.orbitEquivLogicNat.injective
  simp only [forcedAdd, fold_iso_compat, Equiv.apply_symm_apply]

/-- **Multiplicativity.**  The canonical isomorphism is a homomorphism for forced
multiplication. -/
theorem iso_map_forcedMul (R : LogicRealization.{0, v}) (S : LogicRealization.{0, w})
    (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) := by
  apply S.orbitEquivLogicNat.injective
  simp only [forcedMul, fold_iso_compat, Equiv.apply_symm_apply]

/-- Forced order (transported `≤` on `LogicNat`). -/
def forcedLe (R : LogicRealization.{0, v})
    (a b : (forcedArith R).peano.carrier) : Prop :=
  R.orbitEquivLogicNat a ≤ R.orbitEquivLogicNat b

What this page does not claim

The theorem does not derive the order on LogicNat; it takes that order as a definitional starting point. The theorem does not bundle the forced carriers as typeclass instances of an ordered semiring. The theorem says nothing about which specific numbers exist or how large they are, only that the ordering is unique up to isomorphism.

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: