Foundation Universal Forcing Canonical Semiring Iso Iso Map Forced One

The forced one

The number one is the first thing you count, the identity of multiplication, and the unit that makes arithmetic hang together. In the Recognition Science framework, the question is whether this number is truly universal: if the framework's basic structure, a ledger (a discrete record of events), can be built in many different ways, do all those ways agree on what 1 is? The declaration iso_map_forcedOne answers yes, and it does so with the force of a formal proof.

The framework models each possible ledger as a "realization." From any realization, it can construct an entire arithmetic: a zero, a one, addition, multiplication, and an ordering. The theorem iso_map_forcedOne states that for any two realizations, the canonical isomorphism between their arithmetics sends the one of the first to the one of the second. In plainer terms, the number 1 that emerges from one ledger is exactly the number 1 that emerges from any other. The proof is not a numerical coincidence; it follows from the structure of the ledgers themselves.

This is part of a larger result. The same proof technique shows that the canonical isomorphism preserves zero, addition, multiplication, and the ordering, not just the number one. Together, these theorems assemble into a certificate that any two forced arithmetics are isomorphic as ordered commutative semirings. The framework proves that the arithmetic you get is not an accident of how you built the ledger; it is the same arithmetic, every time.

What the theorem does not claim is just as important. It does not say that the framework's number 1 is the same as the 1 of everyday mathematics; that comparison is a separate question. It also does not claim that the framework's arithmetic is the only possible arithmetic, only that all the arithmetics the framework can generate agree with each other. The theorem is about internal consistency, not external uniqueness.

The practical consequence is that the framework's arithmetic is stable. If you build a ledger one way and someone else builds it another way, you will both count to the same 1, add the same way, and order things the same way. This is what makes the framework's claims about physics possible: if the arithmetic were different in different realizations, no universal statement about numbers could ever be made.

/-- 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]

/-- 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]

/-- **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]

/-- **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 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

What this page does not claim

The theorem does not claim that the framework's number 1 is identical to the 1 of everyday mathematics. The theorem does not claim that the framework's arithmetic is the only possible arithmetic, only that all framework-generated arithmetics agree. The theorem does not claim that the framework can construct every possible arithmetic structure.

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: