Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Reversibility/WaitingValueReversibility.waiting_value_from_information_and_option_preservation (✓ std3). ∎
Source. Repository-derived.
Commentary.
When every immediate action remains available through an admissible constant policy, waiting attains exactly the immediate action’s value. Free, world-preserving observation then lets the frozen decision-value theorem compare the two optima.
The public statement also carries five unconditional same-model breakdown witnesses. The first three reuse the frozen opportunity-loss, positive-cost, and world-change countermodels.
The disclosure witness uses two distinguishable states, observations, and public signals, with zero penalty on one signal and positive penalty on the other. Its penalty-free informed optimum is at least the uninformed optimum, while exposure strictly reverses the comparison. The response witness separately models a triggered third-party state transition.
Repository, pinned-Mathlib, and installed-package searches found no exact whole theorem. The extension imports every existing family owner and adds only the two absent carriers.