preferenceCompose
plain-language theorem explainer
preferenceCompose defines the binary operation on action states that adds their improvement ranks while copying the agent from the first operand. It is cited by proofs establishing that the strict ethical realization forms an admissible class with monoid structure. The definition proceeds by direct record construction from the two input states.
Claim. Let $a$ and $b$ be action states. Their composition is the action state whose agent coordinate equals that of $a$ and whose improvement rank equals the sum of the improvement ranks of $a$ and $b$.
background
The module develops domain-rich ethical realization over action states with agent and improvement-rank coordinates. An ActionState is the structure with fields agent : Nat and improvementRank : Nat, deriving decidable equality and representation. The generator is the smallest recognized improvement step, and this composition supplies the monoid operation for the realization.
proof idea
The definition constructs a new ActionState by setting the agent to a.agent and the improvementRank to a.improvementRank + b.improvementRank. It is a direct one-line record update.
why it matters
This supplies the compose field for strictEthicsRealization, which is then used to define ethics_admissible. It enables the proofs of associativity and left identity in RichDomainCosts, and supports the RichDomainCostsCert structure. In the framework it contributes to the ethical component of the universal forcing chain.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.