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

interpret

show as:
view Lean formalization →

The definition supplies a recursive map from the LogicNat orbit to the carrier of any strict logic realization, sending the base identity to the realization's one element and each successor to composition with the generator. Workers on categorical or discrete realizations cite this when constructing faithful interpretations for the universal forcing theorem. It is defined directly by pattern matching on the two constructors of LogicNat.

claimLet $R$ be a strict logic realization. The interpretation function $i_R :$ LogicNat $→ R$.Carrier satisfies $i_R($identity$) = R$.one and $i_R($step $n) = R$.compose$(R$.generator$, i_R(n))$.

background

A StrictLogicRealization supplies only native data: a Carrier type, a Cost type with zero, a compare function, a compose operation, an identity element one, a generator, and two laws (identity_law and non_contradiction_law). The FreeOrbit abbreviation is exactly LogicNat, the inductive type whose constructors are identity (the zero-cost base) and step (iteration of the generator). The module documentation states that StrictLogicRealization removes the internal-orbit escape hatch present in the earlier LogicRealization interface, forcing the free orbit to be derived uniformly as LogicNat for the main universal forcing path.

proof idea

The definition is given by direct pattern matching on the constructors of LogicNat. The identity case returns the one element of the realization. The step case applies the realization's compose operation to its generator and the recursive call on the predecessor.

why it matters in Recognition Science

This definition supplies the missing interpretation step that lets strict realizations participate in the universal forcing theorem without carrying an internal orbit field. It is invoked by the canonical categorical realization, the boolean realization, the modular realization, and the FaithfulArithmeticInterpretation structure. The construction thereby supports the transition from the lightweight LogicRealization interface to the strict variant described in the module documentation.

scope and limits

formal statement (Lean)

  51def interpret (R : StrictLogicRealization) : FreeOrbit R → R.Carrier
  52  | LogicNat.identity => R.one
  53  | LogicNat.step n => R.compose R.generator (interpret R n)
  54

used by (22)

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

depends on (11)

Lean names referenced from this declaration's body.