preferenceCompose_left_id
plain-language theorem explainer
The theorem establishes that the zero action state functions as a left identity under preference composition for any action state in the ethics domain. Researchers verifying algebraic laws in strict realizations of domain costs would cite this when confirming that the ethics cost satisfies the required identity axiom. The proof is a direct term-mode reduction that unfolds the two definitions, applies congruence on the resulting structure, and simplifies the rank addition.
Claim. Let ActionState be the structure with fields agent and improvementRank, both natural numbers. Let ethicalZero be the state with both fields equal to zero. Define preferenceCompose(x, y) to be the state whose agent equals that of x and whose improvementRank equals the sum of the ranks of x and y. Then for every action state a, preferenceCompose(ethicalZero, a) equals the state whose agent is zero and whose improvementRank equals that of a.
background
ActionState is the structure whose fields are a natural-number agent and a natural-number improvementRank. ethicalZero is the concrete element with both fields set to zero. preferenceCompose is the binary operation that copies the agent of its first argument and adds the improvement ranks of its two arguments. These three definitions appear in the Ethics module and are imported here to supply the concrete operations whose laws are proved in the rich-domain layer. The surrounding module proves the full set of composition, decidability, and invariance statements for each of the five domains (Music, Biology, Narrative, Ethics, Metaphysical) that realize StrictLogicRealization with the placeholder laws set to true; the present theorem supplies the left-identity instance for the ethics preference operation.
proof idea
The proof is a one-line wrapper that unfolds the definitions of preferenceCompose and ethicalZero, applies congr 1 to equate the two structure literals, and finishes with simp to discharge the resulting equality on the improvementRank component.
why it matters
The declaration supplies the left-identity law for preference composition inside the ethics domain, one of the five concrete realizations required to replace the placeholder composition_law := True in StrictLogicRealization. It therefore contributes directly to the module's claim that each domain cost is non-trivially law-bearing. The result sits inside the larger verification that the strict forcing chain carries associative composition and identity elements for every listed domain; no downstream use sites are recorded yet, and the theorem does not touch open questions about the remaining invariance or triangle-inequality statements.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.