preferenceCompose_left_id
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.
claimLet 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 in Recognition Science
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.
scope and limits
- Does not prove the corresponding right-identity property for preferenceCompose.
- Does not establish the result for the other four domains.
- Does not address invariance under bijective relabeling of the carrier.
- Does not supply a general identity theorem for arbitrary composition operations.
formal statement (Lean)
154theorem preferenceCompose_left_id (a : ActionState) :
155 preferenceCompose ethicalZero a =
156 { agent := ethicalZero.agent, improvementRank := a.improvementRank } := by
proof body
Term-mode proof.
157 unfold preferenceCompose ethicalZero
158 congr 1
159 simp
160
161end EthicsRich
162
163/-! ## Metaphysical -/
164
165namespace MetaphysicalRich
166
167open Metaphysical
168
169/-- The metaphysical ground supplies an invariant equivalence on arithmetics. -/