Negative and Positive Rights

Abstract

Empty action states separate non-infringement from positive realization.

Theorem 1.1 (No available action separates the two rights).

$$\forall State,Action:\mathrm{Type},x:State,U_x,V_x:\mathrm{Set}Action,F:Action\to State\to State,G:\mathrm{Set}State,V_x\subseteq U_x\Rightarrow U_x=\varnothing \Rightarrow \neg x\in G\Rightarrow \forall N:\mathrm{Set}Action,N\subseteq U_x\Rightarrow \mathrm{negativeRight}(N,V_x)\wedge \neg \mathrm{positiveRight}(U_x,F,G,x)\wedge \neg x\in G\vee \mathrm{positiveRight}(U_x,F,G,x)\wedge \neg \forall N:\mathrm{Set}Action,N\subseteq U_x\Rightarrow \mathrm{negativeRight}(N,V_x)⟺\mathrm{positiveRight}(U_x,F,G,x).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/ActionStateRightsSeparation.no_action_state_separates_rights (✓ std3). ∎

Source. Repository-derived.

Commentary.

An allowed-action set, a chosen-action set, a transition, and a goal set are the source primitives. A negative right is disjointness from the chosen actions; a positive right requires an allowed transition into the goal.

When the allowed-action set is empty and chosen actions are restricted to it, every forbidden subset is harmless, while the positive goal and its realization condition both fail outside the goal.

The four public conjuncts expose the negative-right clause, positive failure, realization failure, and non-equivalence of the predicates.

References

• Truth anchor: D5/S3/ConceptDynamics/ActionStateRightsSeparation.no_action_state_separates_rights
• Dependency: D5/S3/ConceptDynamics/ConceptFiberDecomposition