ethicsInterpret
plain-language theorem explainer
The definition maps a LogicNat element, built from the identity constructor and repeated step applications that mirror the multiplicative orbit, to its iteration count in natural numbers, which acts as the carrier for counting moral improvement steps in the ethics layer of Universal Forcing. Researchers extending Recognition Science to ethical structures would cite this map when embedding logical arithmetic into improvement counts. It is realized as a direct one-line wrapper applying the toNat function.
Claim. Let $n$ be an element of the inductive type generated by the constructors identity (zero-cost element) and step (one generator iteration). Then the map sends $n$ to the natural number obtained by reading off its iteration count, where the carrier type for moral improvement steps is identified with the natural numbers.
background
LogicNat is the inductive type with constructors identity (the zero-cost multiplicative identity in the orbit) and step (one more iteration of the generator), mirroring the smallest subset of positive reals closed under multiplication by the generator and containing 1. MoralImprovementStep is the abbreviation for the natural numbers, serving as the carrier for counting morally meaningful improvements.
proof idea
The definition is a one-line wrapper that applies the toNat function from ArithmeticFromLogic, which sends identity to 0 and step n to the successor of toNat n.
why it matters
This supplies the carrier MoralImprovementStep for the ethicsRealization structure that embeds ethical improvement counts into Universal Forcing. It connects the logical arithmetic forced by the Law of Logic to the moral improvement steps required for ethical realization. The parent definition ethicsRealization uses this carrier together with zero cost and the ethicsCost comparison to complete the realization object.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.