Three Rule Forms and Actor Readout

Abstract

All three actor-relative rule forms descend on the full action-input carrier.

Theorem 1.1 (Compatibility, separation, and recipient descent).

$$\begin{array}{r}\forall X,U,I:\mathrm{Type},\\ B:I\to \mathrm{Type},\\ readout:(agent:I)\to X\to B(agent),\\ transition:X\to \left(U\to \left(I\to \left(I\to X\right)\right)\right),\\ actor:I,\\ \mathrm{let}actorInputReadout:X\times U\times I\to B(actor)\times U\times I:=(input:X\times U\times I\mapsto \mathrm{triple}(readout(actor)(\mathrm{state}(input)),\mathrm{action}(input),\mathrm{recipient}(input))),\\ mirroredTransition:X\times U\times I\to X:=(input:X\times U\times I\mapsto transition(\mathrm{state}(input),\mathrm{action}(input),\mathrm{recipient}(input),actor)),\\ actualTransition:X\times U\times I\to X:=(input:X\times U\times I\mapsto transition(\mathrm{state}(input),\mathrm{action}(input),actor,\mathrm{recipient}(input))),\\ compatible:\mathrm{Prop}:=\mathrm{FactorsThrough}(\mathrm{compose}(readout(actor),mirroredTransition),actorInputReadout)\mathrm{in}\\ (\forall wish\in X\to \mathrm{Prop},\mathrm{FactorsThrough}(wish,readout(actor))\Rightarrow compatible\Rightarrow \mathrm{FactorsThrough}((input:X\times U\times I\mapsto \neg wish(mirroredTransition(input))),actorInputReadout))\wedge \\ (\neg compatible\Rightarrow \exists wish\in X\to \mathrm{Prop},\mathrm{FactorsThrough}(wish,readout(actor))\wedge \neg \mathrm{FactorsThrough}((input:X\times U\times I\mapsto \neg wish(mirroredTransition(input))),actorInputReadout))\wedge \\ (compatible\iff (\forall wish\in X\to \mathrm{Prop},\mathrm{FactorsThrough}(wish,readout(actor))\Rightarrow \mathrm{FactorsThrough}((input:X\times U\times I\mapsto \neg wish(mirroredTransition(input))),actorInputReadout)))\wedge \\ (\forall wish\in X\to \mathrm{Prop},capable\in X\times U\times I\to \mathrm{Prop},\mathrm{FactorsThrough}(wish,readout(actor))\Rightarrow \mathrm{FactorsThrough}(capable,actorInputReadout)\Rightarrow compatible\Rightarrow \mathrm{FactorsThrough}((input:X\times U\times I\mapsto wish(mirroredTransition(input))\wedge capable(input)),actorInputReadout))\wedge \\ (\forall otherWish\in \forall recipient:I,X\to \mathrm{Prop},\mathrm{FactorsThrough}((input:X\times U\times I\mapsto \neg otherWish(\mathrm{recipient}(input),actualTransition(input))),actorInputReadout)\iff \exists descended\in B(actor)\times U\times I\to \mathrm{Prop},(input:X\times U\times I\mapsto otherWish(\mathrm{recipient}(input),actualTransition(input)))=\mathrm{compose}(descended,actorInputReadout)).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/VisibleDescent/ThreeRuleActorDecidability.three_rule_actor_decidability (✓ std3). ∎

Source. Repository-derived.

Commentary.

The actor-visible input retains the action and recipient coordinates while replacing the state by the actor’s readout.

The frozen observer-action criterion supplies compatibility, universal preservation, and the positive desire-and-ability rule on this carrier. Its contrapositive yields the separating desire.

For the actual transition evaluated by the recipient’s desire, Mathlib’s factorization criterion exposes the descended predicate explicitly.

Repository search found the frozen full-carrier owner but no declaration that publicly states both the separating witness and descended predicate. Pinned Mathlib supplies the latter factorization step.

References

• Truth anchor: D5/S3/Observer/VisibleDescent/ThreeRuleActorDecidability.three_rule_actor_decidability
• Dependency: D5/S3/ConceptDynamics/NormativeStructure/ObserverActionRuleDecidability