pith. machine review for the scientific record. sign in
def definition def or abbrev high

equivOfInitial

show as:
view Lean formalization →

The declaration supplies the canonical isomorphism between carriers of initial Peano objects extracted from any two Law-of-Logic realizations. Researchers on universal forcing or realization invariance cite it to establish that arithmetic content is independent of the chosen realization. The construction uses the initiality lifts in each direction and verifies mutual inverses via the uniqueness clause of the initial object.

claimLet $A$ be the arithmetic object forced by realization $R$ and $B$ the arithmetic object forced by realization $S$. Then there is a canonical equivalence $A. peano. carrier ≃ B. peano. carrier$ whose forward map is the unique morphism from $A$'s initial Peano object into $B$'s Peano object and whose inverse is the morphism in the opposite direction.

background

ArithmeticOf is the structure consisting of a PeanoObject together with a proof that it is initial. The module extracts arithmetic from an abstract Law-of-Logic realization by taking the initial Peano algebra generated by the identity and successor data supplied by the realization. Initial objects are unique up to unique isomorphism; this supplies the invariant arithmetic content across realizations.

proof idea

This is a definition that builds the equivalence explicitly. The forward map is the lift of A's initial object into B's Peano object. The inverse map is the lift in the opposite direction. The left inverse property follows because the composition of the two lifts equals the identity morphism on A's Peano object, by the uniqueness property of the initial object. The right inverse is symmetric using B's initiality.

why it matters in Recognition Science

This definition is the core of the arithmetic invariance theorems. It is invoked directly by categorical_arithmetic_invariant, bool_arithmetic_invariant, modular_arithmetic_invariant, ordered_arithmetic_invariant, physics_arithmetic_invariant, and the main arithmetic_invariant in UniversalForcing. It realizes the statement that the forced arithmetic of every realization is canonically equivalent, which is the first theorem form of Universal Forcing. In the framework this closes the initiality step that makes arithmetic realization-independent.

scope and limits

Lean usage

noncomputable def example (R S : LogicRealization) : (arithmeticOf R).peano.carrier ≃ (arithmeticOf S).peano.carrier := equivOfInitial (arithmeticOf R) (arithmeticOf S)

formal statement (Lean)

 209noncomputable def equivOfInitial {R S : LogicRealization}
 210    (A : ArithmeticOf R) (B : ArithmeticOf S) : A.peano.carrier ≃ B.peano.carrier where
 211  toFun := (A.initial.lift B.peano).toFun

proof body

Definition body.

 212  invFun := (B.initial.lift A.peano).toFun
 213  left_inv := by
 214    intro x
 215    have hcomp :
 216        (PeanoObject.Hom.comp (B.initial.lift A.peano) (A.initial.lift B.peano)).toFun =
 217          (PeanoObject.Hom.id A.peano).toFun :=
 218      A.initial.uniq A.peano
 219        (PeanoObject.Hom.comp (B.initial.lift A.peano) (A.initial.lift B.peano))
 220        (PeanoObject.Hom.id A.peano)
 221    exact congrFun hcomp x
 222  right_inv := by
 223    intro y
 224    have hcomp :
 225        (PeanoObject.Hom.comp (A.initial.lift B.peano) (B.initial.lift A.peano)).toFun =
 226          (PeanoObject.Hom.id B.peano).toFun :=
 227      B.initial.uniq B.peano
 228        (PeanoObject.Hom.comp (A.initial.lift B.peano) (B.initial.lift A.peano))
 229        (PeanoObject.Hom.id B.peano)
 230    exact congrFun hcomp y
 231
 232/-- Canonical arithmetic object for any realization: the initial Peano object.
 233
 234This definition is intentionally realization-independent at this stage. The
 235realization supplies the interpretation; initiality supplies the invariant
 236arithmetic content. -/

used by (19)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (24)

Lean names referenced from this declaration's body.