preferenceCompose_assoc
plain-language theorem explainer
Associativity of preference composition on ActionStates follows directly from addition associativity in the Ethics domain. It is invoked when constructing the admissible realization for strict ethics logic. The proof is a short term script that unfolds the composition definition and applies the associativity lemma to the improvement ranks.
Claim. Let $a, b, c$ be ActionStates, each a structure with fields agent and improvementRank in the natural numbers. Define the composition operation by retaining the agent of the first argument and adding the improvement ranks. Then $(a$ composed with $b)$ composed with $c$ equals $a$ composed with $(b$ composed with $c)$.
background
The Rich Domain Costs module supplies the concrete theorems that realize the composition, decidability, and invariance laws for the five domain modules (Music, Biology, Narrative, Ethics, Metaphysical). These replace the placeholder True values in the StrictLogicRealization instances. ActionState is defined as the structure with fields agent : Nat and improvementRank : Nat, deriving decidable equality. The preference composition operation is the function that constructs a new ActionState by copying the agent from the first argument and summing the improvement ranks. The proof relies on the upstream theorem add_assoc, which establishes associativity of addition on the underlying natural numbers.
proof idea
The proof proceeds by unfolding the definition of preference composition on both sides of the equality. The congr tactic then reduces the problem to showing equality of the summed improvement ranks. This is discharged by the exact application of the associativity theorem for addition.
why it matters
This result provides the associativity component for the Ethics domain in the RichDomainCostsCert theorem, which certifies all the required properties across domains. It is used in the construction of ethics_admissible to witness that the strict ethics realization satisfies the admissible conditions. Within the framework, it ensures that the composition law holds concretely for the Ethics strict realization, completing one of the six required properties listed in the module documentation for non-trivial law-bearing realizations.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.