interpret_zero
For any strict logic realization R the recursive interpretation of the base element of the free orbit LogicNat returns exactly the one element supplied by R. Model builders for arithmetic, categorical, or physics realizations cite this base case to confirm their carrier starts the orbit correctly. The proof is immediate reflexivity from the defining equation of interpret.
claimFor any strict logic realization $R$, the interpretation of the base (identity) element of the logic naturals equals the identity element of $R$.
background
StrictLogicRealization is the structure that supplies only native data: a carrier type, a cost type with zero, a symmetric comparison, a binary composition, an identity element one, and a generator, together with the identity and non-contradiction laws. The free orbit is realized by the inductive type LogicNat whose constructors are the identity element and the successor step; this type is the smallest set closed under multiplication by the generator and containing one. The interpret function is defined by primitive recursion on LogicNat, sending the identity constructor to R.one and each step constructor to composition of the generator with the interpretation of the predecessor.
proof idea
One-line reflexivity wrapper. The clause of interpret for the base constructor of LogicNat is literally R.one, so the stated equality holds by the definition of interpret.
why it matters in Recognition Science
The result supplies the base case required by every downstream embedding into LogicRealization, including boolRealization, natOrderedRealization, modularRealization, canonicalCategoricalRealization, and the physics and biology realizations. It closes the strict path of the universal forcing construction so that the derived orbit begins at the supplied identity without an external orbit field. The declaration therefore supports the transition from the lightweight interface to the strict interface used in the main forcing theorem.
scope and limits
- Does not prove the full universal forcing theorem.
- Does not constrain interpretation of positive steps in the orbit.
- Applies only inside the strict realization interface.
- Does not cover ratio-based or continuous realizations directly.
formal statement (Lean)
55@[simp] theorem interpret_zero (R : StrictLogicRealization) :
56 interpret R LogicNat.zero = R.one := rfl
proof body
57
used by (15)
-
canonicalCategoricalRealization -
boolRealization -
LogicRealization -
ofPositiveRatioComparison -
modularRealization -
natOrderedRealization -
physicsRealization -
biologyRealization -
ethicsRealization -
modularRealization -
musicRealization -
narrativeRealization -
orderRealization -
toLightweight -
logicRealizationOfDistinction