ethics_arith_equiv_logicNat
plain-language theorem explainer
The declaration defines an equivalence showing that the Peano carrier extracted from the arithmetic of the strict ethics realization matches the LogicNat type. Researchers tracing forced arithmetic in Recognition Science would cite this to confirm that ethical action states with minimal improvement generators produce the same naturals as the law of logic. The definition is a one-line wrapper that invokes the orbit equivalence from the lightweight conversion of the strict realization.
Claim. Let $R$ be the strict ethical realization over action states with natural-number costs. The carrier of the Peano arithmetic extracted from $R$ is equivalent to the inductive type of natural numbers forced by the law of logic, written $LogicNat$.
background
The Strict/Ethics module constructs domain-rich ethical realizations over action states with agent and improvement-rank coordinates, taking the smallest recognized improvement step as generator. The strictEthicsRealization instance supplies ActionState as carrier, Nat as cost (with zero instance), actionCost for ordering, and preferenceCompose for the binary operation. LogicNat is the inductive type whose identity constructor marks the zero-cost element and whose step constructor iterates the generator, forming the smallest subset of positive reals closed under multiplication by the generator and containing 1. The arith operation on any StrictLogicRealization first converts the structure to its lightweight form via toLightweight and then applies arithmeticOf to obtain the forced Peano structure.
proof idea
The definition is a one-line wrapper that directly returns the orbitEquivLogicNat equivalence supplied by toLightweight applied to strictEthicsRealization. It relies on the upstream arith definition, which constructs ArithmeticOf from the lightweight realization, and on the documented fact that every strict realization yields arithmetic canonically equivalent to LogicNat.
why it matters
This equivalence ties the ethical action-state realization back to the core arithmetic of the Recognition Science foundation, confirming that minimal-improvement generators produce the same LogicNat structure as the law of logic. It supports the StrictLogicRealization interface and the arith extraction without adding hypotheses, reinforcing consistency across all strict realizations in the UniversalForcing layer. No open questions are directly closed here, but the definition prevents divergence between ethical and logical arithmetic.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.