realization_initial
The definition shows that for any LogicRealization R the associated Peano algebra is initial among all Peano algebras. Workers on the universal forcing chain cite it to guarantee that arithmetic is uniquely determined by the logic realization. The construction supplies the lift homomorphism directly from realizationLift and proves uniqueness by reduction to realizationLift_unique_fun.
claimFor any LogicRealization $R$, the Peano algebra generated by the orbit of $R$ admits a unique homomorphism to every other Peano algebra $B$ (a type equipped with a zero element and successor map).
background
In the ArithmeticOf module arithmetic is extracted from an abstract Law-of-Logic realization. A PeanoObject is a structure consisting of a carrier type together with a zero element and a step map. The IsInitial structure on such an algebra supplies a lift homomorphism to any target Peano algebra together with a uniqueness clause asserting that any two lifts agree as functions.
proof idea
The definition is a one-line wrapper that sets the lift field to realizationLift R. The uniqueness clause is discharged by rewriting both candidate homomorphisms with realizationLift_unique_fun R B f and realizationLift_unique_fun R B g.
why it matters in Recognition Science
This declaration supplies the initiality data required by the extracted definition, which packages the Peano algebra and its initiality into an ArithmeticOf structure. It realizes the module's key point that initial objects are unique up to unique isomorphism, providing the mechanism behind Universal Forcing. It connects directly to the forcing chain by ensuring the arithmetic extracted from any logic realization is canonical.
scope and limits
- Does not construct an explicit LogicRealization.
- Does not verify that the generated Peano algebra satisfies the full Peano axioms beyond initiality.
- Does not address non-discrete or higher-dimensional realizations.
- Does not compute numerical values for physical constants.
Lean usage
def exampleExtracted (R : LogicRealization) : ArithmeticOf R := extracted Rformal statement (Lean)
189def realization_initial (R : LogicRealization) :
190 PeanoObject.IsInitial (realizationPeano R) where
191 lift := realizationLift R
proof body
Definition body.
192 uniq := by
193 intro B f g
194 rw [realizationLift_unique_fun R B f, realizationLift_unique_fun R B g]
195
196/-- Arithmetic extracted from the realization's own identity-step orbit. -/