Waiting preserves immediate value, while genuine exposure can reverse it.
Theorem 1.1 (Waiting value comes from information and preserved options).
( ∀ X ∈ Type , E ∈ Type , U ∈ Type , M ∈ Concept ( X → R , R ) , q ∈ Concept ( X , E ) , T ∈ E → X → X , V ∈ Concept ( X , U → R ) , A 0 ∈ Set ( U ) , A 1 ∈ E → Set ( U ) , P ∈ Set ( E → U ) , ( ( ∀ e ∈ E , x ∈ X , T ( e , x ) = x ) ∧ ( ( ∀ u ∈ U , u ∈ A 0 ⇒ (( e : E ) ↦ u ) ∈ P ) ∧ ( ∀ e ∈ E , A 0 ⊆ A 1 ( e ) ) ) ) ⇒ ( ∀ u ∈ U , u ∈ A 0 ⇒ ( (( e : E ) ↦ u ) ∈ admissiblePolicies ( P , A 1 ) ∧ informedExpectedValue ( M , q , T , V , 0 , (( e : E ) ↦ u ) ) = uninformedExpectedValue ( M , V , u ) ) ) ) ∧ ( ∀ X ∈ Type , E ∈ Type , U ∈ Type , M ∈ Concept ( X → R , R ) , q ∈ Concept ( X , E ) , T ∈ E → X → X , V ∈ Concept ( X , U → R ) , c ∈ R , A 0 ∈ Set ( U ) , A 1 ∈ E → Set ( U ) , P ∈ Set ( E → U ) , W 0 ∈ R , W 1 ∈ R , h 0 ∈ IsGreatest ( image ( uninformedExpectedValue ( M , V ) , A 0 ) , W 0 ) , h 1 ∈ IsGreatest ( image ( informedExpectedValue ( M , q , T , V , c ) , admissiblePolicies ( P , A 1 ) ) , W 1 ) , ( c = 0 ∧ ( ( ∀ e ∈ E , x ∈ X , T ( e , x ) = x ) ∧ ( ( ∀ u ∈ U , u ∈ A 0 ⇒ (( e : E ) ↦ u ) ∈ P ) ∧ ( ∀ e ∈ E , A 0 ⊆ A 1 ( e ) ) ) ) ) ⇒ W 0 ≤ W 1 ) ∧ ( ∃ M 2 ∈ Concept ( U ni t → R , R ) , q 2 ∈ Concept ( U ni t , U ni t ) , T 2 ∈ U ni t → U ni t → U ni t , V 2 ∈ Concept ( U ni t , B oo l → R ) , A 20 ∈ Set ( B oo l ) , A 21 ∈ U ni t → Set ( B oo l ) , P 2 ∈ Set ( U ni t → B oo l ) , W 20 ∈ R , W 21 ∈ R , ( ∀ e 2 ∈ U ni t , x 2 ∈ U ni t , T 2 ( e 2 , x 2 ) = x 2 ) ∧ ( ( ∀ u 2 ∈ B oo l , u 2 ∈ A 20 ⇒ (( e 2 : U ni t ) ↦ u 2 ) ∈ P 2 ) ∧ ( ( ∃ e 2 ∈ U ni t , u 2 ∈ B oo l , u 2 ∈ A 20 ∧ ¬ ( u 2 ∈ A 21 ( e 2 )) ) ∧ ( IsGreatest ( image ( uninformedExpectedValue ( M 2 , V 2 ) , A 20 ) , W 20 ) ∧ ( IsGreatest ( image ( informedExpectedValue ( M 2 , q 2 , T 2 , V 2 , 0 ) , admissiblePolicies ( P 2 , A 21 ) ) , W 21 ) ∧ W 21 < W 20 ) ) ) ) ) ∧ ( ∃ M 3 ∈ Concept ( U ni t → R , R ) , q 3 ∈ Concept ( U ni t , U ni t ) , T 3 ∈ U ni t → U ni t → U ni t , V 3 ∈ Concept ( U ni t , U ni t → R ) , A 30 ∈ Set ( U ni t ) , A 31 ∈ U ni t → Set ( U ni t ) , P 3 ∈ Set ( U ni t → U ni t ) , c 3 ∈ R , W 30 ∈ R , W 31 ∈ R , 0 < c 3 ∧ ( ( ∀ e 3 ∈ U ni t , x 3 ∈ U ni t , T 3 ( e 3 , x 3 ) = x 3 ) ∧ ( ( ∀ u 3 ∈ U ni t , u 3 ∈ A 30 ⇒ (( e 3 : U ni t ) ↦ u 3 ) ∈ P 3 ) ∧ ( ( ∀ e 3 ∈ U ni t , A 31 ( e 3 ) = A 30 ) ∧ ( IsGreatest ( image ( uninformedExpectedValue ( M 3 , V 3 ) , A 30 ) , W 30 ) ∧ ( IsGreatest ( image ( informedExpectedValue ( M 3 , q 3 , T 3 , V 3 , c 3 ) , admissiblePolicies ( P 3 , A 31 ) ) , W 31 ) ∧ W 31 < W 30 ) ) ) ) ) ) ∧ ( ∃ M 4 ∈ Concept ( B oo l → R , R ) , q 4 ∈ Concept ( B oo l , U ni t ) , T 4 ∈ U ni t → B oo l → B oo l , V 4 ∈ Concept ( B oo l , U ni t → R ) , A 40 ∈ Set ( U ni t ) , A 41 ∈ U ni t → Set ( U ni t ) , P 4 ∈ Set ( U ni t → U ni t ) , W 40 ∈ R , W 41 ∈ R , ( ∃ e 4 ∈ U ni t , x 4 ∈ B oo l , T 4 ( e 4 , x 4 ) = x 4 ) ∧ ( ( ∀ u 4 ∈ U ni t , u 4 ∈ A 40 ⇒ (( e 4 : U ni t ) ↦ u 4 ) ∈ P 4 ) ∧ ( ( ∀ e 4 ∈ U ni t , A 40 ⊆ A 41 ( e 4 ) ) ∧ ( IsGreatest ( image ( uninformedExpectedValue ( M 4 , V 4 ) , A 40 ) , W 40 ) ∧ ( IsGreatest ( image ( informedExpectedValue ( M 4 , q 4 , T 4 , V 4 , 0 ) , admissiblePolicies ( P 4 , A 41 ) ) , W 41 ) ∧ W 41 < W 40 ) ) ) ) ) ∧ ( ∃ M 5 ∈ Concept ( B oo l → R , R ) , q 5 ∈ Concept ( B oo l , B oo l ) , T 5 ∈ B oo l → B oo l → B oo l , V 5 ∈ Concept ( B oo l , U ni t → R ) , d 5 ∈ Concept ( B oo l , B oo l ) , c 5 ∈ B oo l → R , A 50 ∈ Set ( U ni t ) , A 51 ∈ B oo l → Set ( U ni t ) , P 5 ∈ Set ( B oo l → U ni t ) , W 50 ∈ R , W 51 ∈ R , W 52 ∈ R , ( ∀ e 5 ∈ B oo l , x 5 ∈ B oo l , T 5 ( e 5 , x 5 ) = x 5 ) ∧ ( ( ∀ u 5 ∈ U ni t , u 5 ∈ A 50 ⇒ (( e 5 : B oo l ) ↦ u 5 ) ∈ P 5 ) ∧ ( ( ∀ e 5 ∈ B oo l , A 50 ⊆ A 51 ( e 5 ) ) ∧ ( ( ∃ a ∈ B oo l , b ∈ B oo l , q 5 ( a ) = q 5 ( b ) ∧ ( d 5 ( q 5 ( a )) = d 5 ( q 5 ( b )) ∧ ( c 5 ( d 5 ( q 5 ( a ))) = 0 ∧ 0 < c 5 ( d 5 ( q 5 ( b ))) ) ) ) ∧ ( IsGreatest ( image ( uninformedExpectedValue ( M 5 , V 5 ) , A 50 ) , W 50 ) ∧ ( IsGreatest ( image ( informedExpectedValue ( M 5 , q 5 , T 5 , V 5 , 0 ) , admissiblePolicies ( P 5 , A 51 ) ) , W 51 ) ∧ ( W 50 ≤ W 51 ∧ ( IsGreatest ( image ( ( p 5 : B oo l → U ni t ) ↦ M 5 (( x 5 : B oo l ) ↦ V 5 ( T 5 ( q 5 ( x 5 ) , x 5 ) , p 5 ( q 5 ( x 5 ))) − c 5 ( d 5 ( q 5 ( x 5 )))) , admissiblePolicies ( P 5 , A 51 ) ) , W 52 ) ∧ W 52 < W 50 ) ) ) ) ) ) ) ) ∧ ( ∃ M 6 ∈ Concept ( B oo l → R , R ) , q 6 ∈ Concept ( B oo l , U ni t ) , T 6 ∈ U ni t → B oo l → B oo l , R 6 ∈ U ni t → B oo l → B oo l , V 6 ∈ Concept ( B oo l , U ni t → R ) , A 60 ∈ Set ( U ni t ) , A 61 ∈ U ni t → Set ( U ni t ) , P 6 ∈ Set ( U ni t → U ni t ) , W 60 ∈ R , W 61 ∈ R , ( ∀ e 6 ∈ U ni t , x 6 ∈ B oo l , T 6 ( e 6 , x 6 ) = x 6 ) ∧ ( ( ∃ e 6 ∈ U ni t , x 6 ∈ B oo l , R 6 ( e 6 , T 6 ( e 6 , x 6 )) = T 6 ( e 6 , x 6 ) ) ∧ ( ( ∀ u 6 ∈ U ni t , u 6 ∈ A 60 ⇒ (( e 6 : U ni t ) ↦ u 6 ) ∈ P 6 ) ∧ ( ( ∀ e 6 ∈ U ni t , A 60 ⊆ A 61 ( e 6 ) ) ∧ ( IsGreatest ( image ( uninformedExpectedValue ( M 6 , V 6 ) , A 60 ) , W 60 ) ∧ ( IsGreatest ( image ( informedExpectedValue ( M 6 , q 6 , ( e 6 : U ni t , x 6 : B oo l ) ↦ R 6 ( e 6 , T 6 ( e 6 , x 6 )) , V 6 , 0 ) , admissiblePolicies ( P 6 , A 61 ) ) , W 61 ) ∧ W 61 < W 60 ) ) ) ) ) ) .
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.