Foundation Universal Forcing Canonical Semiring Iso Iso Map Forced Zero

The forced zero

The number zero is the starting point of counting. In the framework of Recognition Science, the question is whether this starting point is a free choice or an inevitable one. The declaration iso_map_forcedZero proves that it is inevitable: for any two valid counting structures, the unique structure-preserving map between them sends the zero of the first structure exactly to the zero of the second. In plain terms, every way of building a counting system from the framework's basic assumptions must agree on where counting begins.

This result is part of a larger machine-checked library of formal theorems. The library shows that the framework's counting structures, called forced arithmetics, are not just similar but isomorphic: the unique map between any two of them preserves zero, one, addition, multiplication, and the order relation. The theorem about zero is the first and simplest of these preservation results. It follows from a deeper fact about how any counting structure folds onto a reference structure called LogicNat. Since both structures fold onto the same reference, the map between them must send the zero of one to the zero of the other.

The theorem does not claim that zero is a physical object or that the framework explains why counting starts at zero rather than one. It claims only that within the framework's assumptions, the location of zero is forced. The framework models counting as a discrete record of events, and this theorem says that all such records share the same starting point. This is a structural fact about the framework's own definitions, not a claim about the empirical world.

What the result changes is the status of zero in the framework. Zero is not an arbitrary choice that each counting structure makes independently. It is a fixed point that every structure must respect. This makes the framework's arithmetic canonical: there is exactly one way to count, up to the unique isomorphism that preserves the starting point. The theorem is a small but load-bearing piece of the framework's claim that its arithmetic is not invented but derived.

The theorem is proved in the machine-checked library, meaning it has been verified by a computer to follow from the framework's axioms. It is not a conjecture or a heuristic. The proof is complete and checked. This is the strongest kind of claim the framework makes: a theorem that has been formally verified.

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

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

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

What this page does not claim

The theorem does not claim that zero is a physical object or that the framework explains why counting starts at zero rather than one. The theorem does not claim that the framework's arithmetic is the only possible arithmetic, only that within the framework it is forced. The theorem does not claim that the framework's counting structures are the same as conventional natural numbers, only that they are isomorphic to them. The theorem does not claim that the framework's assumptions are true, only that the theorem follows from them.

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: