Foundation Universal Forcing Canonical Semiring Iso Forced Ordered Semiring Iso

The forced arithmetic

Think of a ledger, a discrete record of events. Recognition Science starts from the claim that reality keeps such a ledger, and that the cost of recording a recognition is forced by logic alone. The framework's library, a machine-checked collection of formal theorems, has already shown that any two such ledgers are structurally identical as counting systems: they have the same zero and the same successor operation. The declaration ForcedOrderedSemiringIsoCert extends that identity to the full arithmetic a counting system determines.

In plain terms, the certificate proves that the addition, multiplication, and ordering you can define on any forced ledger are exactly the same as on any other. If you take two ledgers and line them up by their counting structure, the sum of two entries in the first maps to the sum of the corresponding entries in the second, and likewise for products and for the less-than-or-equal relation. The zero and the one of one ledger land on the zero and the one of the other. The proof works by folding every ledger onto a single reference counting system, the natural numbers built from logic, and showing the fold respects every operation. The key lemma, called fold compatibility, is pure initiality: both sides are homomorphisms from the same initial object, so they must be equal.

The result is a theorem in the machine-checked library, meaning every step is verified by a proof checker with no gaps and no framework-specific axioms. The library audits to the three standard axioms of the ambient type theory: propositional extensionality, choice, and quotient soundness. The certificate does not merely assert the isomorphism; it packages the five preservation theorems, one each for zero, one, addition, multiplication, and order, into a single structure that any later proof can invoke.

What the certificate does not claim is just as important. It does not bundle the reference arithmetic as a typeclass instance in the library's algebraic hierarchy; that is a separate enrichment of the reference object alone. It does not say that the ledgers are physically real, only that if they exist, their arithmetic is forced. And it does not derive any physical constant or empirical prediction. The payoff is structural: within the framework, arithmetic is not a human convention layered on top of reality. It is what any recognition ledger must already contain, because the logic of counting leaves no room for variation.

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

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

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

/-- 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 certificate does not bundle LogicNat as a typeclass instance in the algebraic hierarchy. The certificate does not assert that the ledgers are physically real, only that their arithmetic is forced if they exist. The certificate does not derive any physical constant or empirical prediction.

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: