Encyclopedia Foundation Foundation Universal Forcing Canonical Semiring Iso Fold Iso Compat

ARTICLE 3 claims 3 theorems

Foundation Universal Forcing Canonical Semiring Iso Fold Iso Compat

A single lemma shows why every forced arithmetic structure is the same one, by making the comparison map agree with the reference counting map.

Verify this page

The canonical fold

In the Recognition Science framework, a ledger is a discrete record of events, and a recognition is an event that the ledger records. The framework's library is a machine-checked collection of formal theorems that starts from a minimal cost condition and derives arithmetic, constants, and geometry. A central step is showing that the arithmetic forced by any two ledgers is the same arithmetic, up to a unique comparison map.

The declaration fold_iso_compat is the load-bearing lemma in that step. It says: take any two ledgers, each with its own forced arithmetic structure. The unique comparison map between them, followed by the second ledger's canonical fold onto the reference counting structure, equals the first ledger's canonical fold. In plainer words, the comparison map does not scramble the counting. It agrees with the reference counting map, so the two ledgers count in the same order.

The proof is pure initiality. Both sides of the equality are Peano homomorphisms from the first ledger's forced arithmetic into the reference structure. Since the forced arithmetic is initial, there is only one such homomorphism, so the two sides must be equal. The lemma is a theorem in the machine-checked library, not a postulate or a convention.

From this lemma, the library derives the full ordered-semiring isomorphism content: the comparison map sends the forced zero to the forced zero, the forced one to the forced one, preserves forced addition and multiplication, and preserves and reflects the forced order. The certificate bundles these five properties into a single statement that the forced arithmetics are canonically isomorphic as ordered commutative semirings across all ledgers.

The lemma does not claim that the reference structure or any carrier is registered as a typeclass instance in the ambient mathematical library. That is a separate, purely structural enrichment, and the forcing statement does not need it. The lemma also does not claim anything about what the forced arithmetic is, only that it is the same across ledgers.

THEOREM fold_iso_compat · IndisputableMonolith/Foundation/UniversalForcing/CanonicalSemiringIso.lean
fold_iso_compat · IndisputableMonolith/Foundation/UniversalForcing/CanonicalSemiringIso.lean:65 
/-- **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
THEOREM iso_map_forcedZero · iso_map_forcedOne · iso_map_forcedAdd · iso_map_forcedMul · iso_map_forcedLe · IndisputableMonolith/Foundation/UniversalForcing/CanonicalSemiringIso.lean
iso_map_forcedZero · IndisputableMonolith/Foundation/UniversalForcing/CanonicalSemiringIso.lean:110 
/-- 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]
iso_map_forcedOne · IndisputableMonolith/Foundation/UniversalForcing/CanonicalSemiringIso.lean:116 
/-- 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]
iso_map_forcedAdd · IndisputableMonolith/Foundation/UniversalForcing/CanonicalSemiringIso.lean:122 
/-- **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]
iso_map_forcedMul · IndisputableMonolith/Foundation/UniversalForcing/CanonicalSemiringIso.lean:132 
/-- **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]
iso_map_forcedLe · IndisputableMonolith/Foundation/UniversalForcing/CanonicalSemiringIso.lean:142 
/-- **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]
THEOREM fold_iso_compat · IndisputableMonolith/Foundation/UniversalForcing/CanonicalSemiringIso.lean
fold_iso_compat · IndisputableMonolith/Foundation/UniversalForcing/CanonicalSemiringIso.lean:65 
/-- **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

What this page does not claim

The lemma does not register any carrier as a typeclass instance in the ambient mathematical library. The lemma does not state what the forced arithmetic is, only that it is canonically the same across ledgers. The lemma does not depend on any empirical measurement or physical constant.

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:

MACHINE LAYER · GROUNDED CLAIM TABLE · CLICK TO EXPAND