value-change-base-layer

Theorem 2.4 of the value-change note (a reflection-satisfying change is closer to the value variable in mean square and selects acts of higher expected value) and the three-term decomposition of its section 1.4 hold over the finite distributions of the formalization library as kernel-checked statements, with the note's fixture numbers as witnesses.

A change of an agent's utility function can be written as a change of belief about a value variable on an expanded algebra, and the agent that results acts identically on the original propositions; the direction from the expanded algebra back to the original is marginalization and the converse is a choice of decomposition that is not unique.

The murder-pill inequality, that the utility of the best act under U is at least the utility under U of the best act under the changed utility, yields resistance to value change only for a utility that does not depend on the modification event; in the note's two-step example an expected-utility agent strictly prefers having its values changed, 0.9 for accepting against 0.6 for declining.

The value to an agent of a change of its utility function splits exactly into a term that is never positive (the murder-pill term), a payment term (intrinsic preference for the change) and an information term (instrumental preference, positive only when the outcome of the change is uncertain).

An update that satisfies no expected net update can be valued strictly below no update (the note's coin-driven change, 0.5 against 0.6), so the rule that licenses wanting a modification is reflection with respect to the modification event and not the martingale condition alone.

The representation of value change as belief change on an expanded algebra can be improved until it reflects a trained system corrected through its training data well.

The representation of corrigibility covers changes of the sigma-algebra, taken up after the absolutely continuous case has been studied thoroughly.