Joint Resource Safety Criterion

Abstract

Jointly attainable local extraction caps guarantee resource safety exactly when their total fits the stock-plus-recovery budget.

Theorem 1.1 (Jointly attainable caps characterize resource safety).

$(\forall A g e n t \in T y p e, s \in R e a l, s min \in R e a l, g \in R e a l \to R e a l, c \in A g e n t \to R e a l, F e a s ib l e \in (A g e n t \to R e a l) \to P ro p, ((Fintype (A g e n t) \land F e a s ib l e (c)) \land (\forall a \in A g e n t \to R e a l, F e a s ib l e (a) \Rightarrow (\forall i \in A g e n t, 0 \leq a (i) \land a (i) \leq c (i)))) \Rightarrow ((\forall a \in A g e n t \to R e a l, F e a s ib l e (a) \Rightarrow s min \leq s + g (s) - sum (a)) \Leftrightarrow sum (c) \leq s + g (s) - s min)) \land (\exists s \in R e a l, s min \in R e a l, g \in R e a l \to R e a l, c \in Fin (2) \to R e a l, a \in Fin (2) \to R e a l, ((((((s = 1 \land s min = 0) \land g = const (0)) \land c = const (\frac{3}{4})) \land a = c) \land (\forall j \in Fin (2), 0 \leq a (j) \land a (j) \leq c (j))) \land (\forall j \in Fin (2), s min \leq s + g (s) - a (j))) \land s + g (s) - sum (a) < s min)$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/TargetRisk/JointResourceSafetyCriterion.jointly_attainable_caps_characterize_resource_safety (✓ std3). ∎

Source. Repository-derived.

Commentary.

A feasible extraction is constructed from a finite family of agents, a current stock, its recovery rule, and local extraction caps. The cap vector itself is explicitly required to be feasible.

If every feasible extraction is nonnegative and bounded pointwise by the caps, then all feasible next-period stocks meet the minimum exactly when the sum of the caps fits the recoverable budget.

The same two-agent cap and extraction vectors witness the contrast: each three-quarter extraction alone leaves nonnegative stock, while their joint extraction drives the next stock below zero.

References

Truth anchor: D5/S3/ConceptDynamics/TargetRisk/JointResourceSafetyCriterion.jointly_attainable_caps_characterize_resource_safety

Keyboard shortcuts

trureturing Blueprint

Joint Resource Safety Criterion

Abstract

References