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

categoricalRealization

show as:
view Lean formalization →

Canonical categorical realization supplies the LogicRealization whose carrier is the LogicNat Peano object inside the universal forcing setup. Researchers extracting arithmetic from logic realizations or building the Recognition Science forcing chain cite it to obtain the Lawvere-style model without universe noise. The definition is a one-line wrapper that delegates directly to the canonical construction in CategoricalLogicRealization.

claimLet $R$ be the LogicRealization with carrier the LogicNat Peano object, cost type the natural numbers, zero-cost instance, comparison returning 0 on equality and 1 otherwise, and zero element the LogicNat zero.

background

LogicRealization is the structure that packages a carrier type, a cost type equipped with zero, a compare function from carrier to cost, and a distinguished zero element; these fields supply the topology, order, or category needed by the universal forcing program while the invariant target remains the arithmetic object extracted from the identity and step data. The module re-exports the canonical categorical/Lawvere-style realization under the UniversalForcing tree. The upstream canonicalCategoricalRealization hard-codes the NNO as carrier to avoid universe inference noise from the generic ofNNO wrapper.

proof idea

One-line wrapper that applies canonicalCategoricalRealization.

why it matters in Recognition Science

The definition feeds the downstream equivalence categorical_arith_equiv_logicNat that identifies the arithmetic extracted from the realization with LogicNat. It supplies the categorical model required by the UniversalForcing program and thereby supports extraction of Peano structure from logic realizations in the Recognition framework. No open scaffolding is closed here; the declaration simply re-exports the canonical object for use in the forcing chain.

scope and limits

Lean usage

categoricalRealization.orbitEquivLogicNat

formal statement (Lean)

  18def categoricalRealization : LogicRealization :=

proof body

Definition body.

  19  canonicalCategoricalRealization
  20
  21/-- Categorical realization carries the universal forced arithmetic. -/

used by (1)

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

depends on (2)

Lean names referenced from this declaration's body.