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

arith

show as:
view Lean formalization →

This definition extracts the forced arithmetic object from any strict law-of-logic realization by first mapping it to the lightweight interface and then invoking the universal extraction. Domain auditors in biology, categorical logic, ethics, and music cite it to obtain the Peano carrier and initiality data for their specific realizations. The implementation is a one-line wrapper delegating directly to the existing arithmetic extraction on the converted realization.

claimLet $R$ be a strict realization supplying only native comparison, composition, identity, and non-contradiction data on a carrier. Then arith$(R)$ is the arithmetic object whose Peano structure and initiality are obtained by first deriving the orbit fields from the forced natural numbers and then extracting the arithmetic via the universal forcing map.

background

StrictLogicRealization is the structure that carries only native law-of-logic data: a carrier type, a cost type equipped with zero, comparison and composition maps, distinguished one and generator elements, plus the identity and non-contradiction laws. The module derives the free orbit uniformly as LogicNat, the inductive type whose constructors identity and step mirror the smallest multiplicative orbit containing 1 and closed under the generator. toLightweight converts any such strict realization into the standard lightweight interface by setting the zero element to the supplied one and populating the remaining orbit fields from LogicNat. ArithmeticOf packages the resulting Peano object together with its initiality proof; the upstream arithmeticOf function performs the extraction for any lightweight realization.

proof idea

The definition is a one-line wrapper that applies the arithmeticOf extraction to the lightweight realization produced by toLightweight on the input strict realization.

why it matters in Recognition Science

arith feeds the AxiomAudit checks that confirm equivalence of extracted arithmetic to LogicNat for strict realizations in biology, categorical structures, ethics, music, narrative, and ordered domains. It closes the strict path of the Universal Forcing theorem by ensuring the orbit is derived rather than supplied, completing the step from native laws to the forced natural numbers. The construction sits inside the T5–T8 forcing chain and supplies the arithmetic substrate used by downstream mass-ladder and constant derivations.

scope and limits

formal statement (Lean)

  95def arith (R : StrictLogicRealization) : ArithmeticOf (toLightweight R) :=

proof body

Definition body.

  96  arithmeticOf (toLightweight R)
  97
  98/-- Every strict realization has forced arithmetic canonically equivalent to
  99`LogicNat`. -/

used by (29)

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

depends on (6)

Lean names referenced from this declaration's body.