Static and Adaptive Submodularity Separation

Abstract

A rare posterior branch separates expected from pathwise diminishing returns.

Theorem 1.1 (Adaptive submodularity implies static submodularity).

$\forall m u, A, g P r i or, g P a t h, AdaptiveSubmodular (m u, A, g P r i or, g P a t h) \Rightarrow StaticSubmodular (m u, A, g P r i or, g P a t h) .$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.adaptive_submodular_implies_static_submodular (✓ std3). ∎

Source. Repository-derived.

Commentary.

A positive-mass pathwise bound can be multiplied by its mass and summed. Zero-mass outputs contribute zero, and normalization gives the static expected bound.

Theorem 1.2 (The prior and gate law are normalized).

$ProbabilityMass (r a re P r i or M a ss) \land ProbabilityMass (r a re G a t e O u t co m e M a ss) \land rareGateOutcomeMass (f a l se) = \frac{1}{10} .$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.rare_prior_and_gate_are_normalized (✓ std3). ∎

Source. Repository-derived.

Commentary.

The common state has mass 9/10 and the two rare states each have mass 1/20. The gate’s rare output therefore has total mass 1/10.

Theorem 1.3 (A rare output activates the specialist).

$posteriorAfterReadout (g a t e E x p er im e n t, f a l se, n o n e) = 0 \land posteriorAfterReadout (g a t e E x p er im e n t, f a l se, some (f a l se)) = \frac{1}{2} \land posteriorAfterReadout (g a t e E x p er im e n t, f a l se, some (t r u e)) = \frac{1}{2} \land rarePriorMarginalGain (s p ec ia l i s tE x p er im e n t) = \frac{1}{20} \land rarePathMarginalGain (f a l se, s p ec ia l i s tE x p er im e n t) = \frac{1}{2} .$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.rare_output_posterior_activates_specialist (✓ std3). ∎

Source. Repository-derived.

Commentary.

Conditioning on the rare gate output removes the common state. The two remaining states become equiprobable, so specialist value rises from 1/20 to 1/2.

Theorem 1.4 (The rare-branch instance is statically submodular).

$StaticSubmodular (r a re G a t e O u t co m e M a ss, a v ai l ab l e A f t er G a t e, r a re P r i or M a r g ina lG ain, r a re P a t h M a r g ina lG ain) .$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.rare_branch_static_submodular (✓ std3). ∎

Source. Repository-derived.

Commentary.

The specialist has gain zero on the common output and gain 1/2 on the rare output. Its expected posterior gain is exactly 1/20, equal to its prior gain.

Theorem 1.5 (The rare-branch instance is not adaptively submodular).

$\neg AdaptiveSubmodular (r a re G a t e O u t co m e M a ss, a v ai l ab l e A f t er G a t e, r a re P r i or M a r g ina lG ain, r a re P a t h M a r g ina lG ain) .$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.rare_branch_not_adaptive_submodular (✓ std3). ∎

Source. Repository-derived.

Commentary.

The rare output has positive probability, yet its realized specialist gain 1/2 exceeds the prior gain 1/20. This violates the pathwise bound.

Theorem 1.6 (FPOD principle 246.1).

$\neg StaticSubmodular (r a re G a t e O u t co m e M a ss, a v ai l ab l e A f t er G a t e, r a re P r i or M a r g ina lG ain, r a re P a t h M a r g ina lG ain) \Rightarrow AdaptiveSubmodular (r a re G a t e O u t co m e M a ss, a v ai l ab l e A f t er G a t e, r a re P r i or M a r g ina lG ain, r a re P a t h M a r g ina lG ain) .$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.fpod_principle_246_1 (✓ std3). ∎

Source. Repository-derived.

Commentary.

The same finite instance satisfies expected diminishing returns and fails pathwise diminishing returns. Static submodularity therefore does not imply adaptive submodularity.

Theorem 1.7 (An empty experiment family satisfies both properties).

$StaticSubmodular (r a re G a t e O u t co m e M a ss, unavailable (E m pt y), e m pt y P r i or G ain, e m pt y P a t h G ain) \land AdaptiveSubmodular (r a re G a t e O u t co m e M a ss, unavailable (E m pt y), e m pt y P r i or G ain, e m pt y P a t h G ain) .$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.empty_experiment_family_satisfies_both (✓ std3). ∎

Source. Repository-derived.

Commentary.

With no next experiment, both marginal-return conditions are vacuous. Only normalization of the gate-output law remains.

Theorem 1.8 (An unavailable singleton family satisfies both properties).

$StaticSubmodular (r a re G a t e O u t co m e M a ss, unavailable (U ni t), zero G ain, zero G ain) \land AdaptiveSubmodular (r a re G a t e O u t co m e M a ss, unavailable (U ni t), zero G ain, zero G ain) .$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.singleton_experiment_family_satisfies_both (✓ std3). ∎

Source. Repository-derived.

Commentary.

A singleton experiment family whose sole member is unavailable has no next-step obligation, so both conditions again hold vacuously.

Theorem 1.9 (Constant zero gain satisfies both properties).

$StaticSubmodular (r a re G a t e O u t co m e M a ss, a llE x p er im e n t s, zero G ain, zero G ain) \land AdaptiveSubmodular (r a re G a t e O u t co m e M a ss, a llE x p er im e n t s, zero G ain, zero G ain) .$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.constant_gain_satisfies_both (✓ std3). ∎

Source. Repository-derived.

Commentary.

When every prior and posterior marginal gain is zero, all expected and pathwise comparisons reduce to equality.

Theorem 1.10 (Posterior-independent gain satisfies both properties).

$StaticSubmodular (r a re G a t e O u t co m e M a ss, a v ai l ab l e A f t er G a t e, r a re P r i or M a r g ina lG ain, posteriorIndependent (r a re P r i or M a r g ina lG ain)) \land AdaptiveSubmodular (r a re G a t e O u t co m e M a ss, a v ai l ab l e A f t er G a t e, r a re P r i or M a r g ina lG ain, posteriorIndependent (r a re P r i or M a r g ina lG ain)) .$

Proof. Machine-checked in Lean as D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.posterior_not_updating_satisfies_both (✓ std3). ∎

Source. Repository-derived.

Commentary.

If every posterior marginal equals its prior marginal, conditioning cannot create a pathwise increase and both notions reduce to equality.

References

Truth anchor: D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.adaptive_submodular_implies_static_submodular
Truth anchor: D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.constant_gain_satisfies_both
Truth anchor: D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.empty_experiment_family_satisfies_both
Truth anchor: D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.fpod_principle_246_1
Truth anchor: D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.posterior_not_updating_satisfies_both
Truth anchor: D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.rare_branch_not_adaptive_submodular
Truth anchor: D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.rare_branch_static_submodular
Truth anchor: D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.rare_output_posterior_activates_specialist
Truth anchor: D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.rare_prior_and_gate_are_normalized
Truth anchor: D5/S3/Estimation/ExperimentCost/StaticAdaptiveSubmodularitySeparation.singleton_experiment_family_satisfies_both

Keyboard shortcuts

trureturing Blueprint

Static and Adaptive Submodularity Separation

Abstract

References