preferenceCompose
preferenceCompose equips pairs of ActionState records with a binary operation that preserves the agent coordinate and adds the improvement ranks. Workers on admissible ethical realizations cite this when constructing the StrictLogicRealization for strict ethics. The definition is a direct record constructor that delegates addition to the natural numbers.
claimFor action states $a$ and $b$ with agent and improvement-rank coordinates, their composition is the action state whose agent equals the agent of $a$ and whose improvement rank equals the sum of the improvement ranks of $a$ and $b$.
background
ActionState is the structure with fields agent : Nat and improvementRank : Nat. The module Strict/Ethics develops domain-rich ethical realizations over these states, taking the smallest recognized improvement step as generator. This builds directly on the ActionState structure to define costs and compositions for ethical actions.
proof idea
This is a direct definition that constructs the composed ActionState by copying the agent from the first argument and adding the improvement ranks using natural number addition.
why it matters in Recognition Science
This definition supplies the compose operation for the StrictLogicRealization in strictEthicsRealization. It is used to establish ethics_admissible and to prove associativity and left identity in RichDomainCosts. It realizes the composition law for ethical preferences in the Recognition framework, feeding into admissible class constructions.
scope and limits
- Does not define a cost function or zero element.
- Does not prove any algebraic properties such as associativity.
- Does not extend to non-natural number ranks.
- Does not incorporate agent changes during composition.
formal statement (Lean)
35def preferenceCompose (a b : ActionState) : ActionState :=
proof body
Definition body.
36 { agent := a.agent, improvementRank := a.improvementRank + b.improvementRank }
37