ActionState
ActionState encodes ethical positions as pairs of natural numbers for agent and improvement rank. Researchers modeling strict ethical realization over the forcing chain cite this structure to define action costs and preference composition. The definition is a direct structure declaration deriving decidable equality and representation.
claimAn ethical action state consists of an agent index and an improvement rank, both natural numbers.
background
The module Strict/Ethics.lean develops domain-rich ethical realization over action states with agent and improvement-rank coordinates. The generator is the smallest recognized improvement step, instantiated as the pair with agent 0 and rank 1. Action costs are defined as 0 for identical states and 1 otherwise, with symmetry and self-properties following directly. Preference composition adds improvement ranks while preserving the agent.
proof idea
The declaration is a bare structure definition introducing the two fields and deriving DecidableEq and Repr. No tactics or lemmas are applied.
why it matters in Recognition Science
This structure underpins the strict ethics module, serving as the domain for actionCost which measures unit cost between distinct states, ethicalZero at (0,0), minimalImprovement at (0,1), and strictEthicsRealization. It supports the realization of ethical preferences via rank addition. In the Recognition framework it provides a discrete model for improvement steps aligned with the recognition composition law.
scope and limits
- Does not assign physical units or phi-ladder rungs to the ranks.
- Does not prove any invariance under the recognition composition law.
- Does not specify how agents interact across different states.
formal statement (Lean)
17structure ActionState where
18 agent : Nat
19 improvementRank : Nat
20 deriving DecidableEq, Repr
21