Cocycle And Policy Separation

Abstract

Cocycle accounting does not determine which legal action a policy selects.

Theorem 1.1 (Cocycle composition leaves policy choice nonunique).

$$\forall U,Sigma,Case,PublicFact,Outcome:\mathrm{Type},[\mathrm{Nonempty}\left(U\right)],[\mathrm{AddCommGroup}\left(Sigma\right)],projection:\mathrm{AddMonoidHom}\left(Sigma,\mathrm{AddCircle}\left(1\right)\right),hProjectionSurjective:\mathrm{Surjective}\left(projection\right),hiddenEquiv:\mathrm{AdditiveEquiv}\left(HiddenJumpCoordinates,\ker \left(projection\right)\right),sectionAlpha,sectionBeta,sectionGamma:U\to Sigma,jumpAlphaBeta,jumpBetaGamma,jumpAlphaGamma:U\to HiddenJumpCoordinates,hAlphaBeta:\forall u,sectionBeta(u)=sectionAlpha(u)+hiddenEquiv(jumpAlphaBeta(u)),hBetaGamma:\forall u,sectionGamma(u)=sectionBeta(u)+hiddenEquiv(jumpBetaGamma(u)),publicLaw:Case\to PublicFact,admissible:Case\to \mathrm{Prop},permitted:Case\to Outcome\to \mathrm{Prop},b:PublicFact,\exists leftOutcome,rightOutcome:Outcome,leftOutcome\ne rightOutcome\wedge (\exists x:Case,admissible(x)\wedge publicLaw(x)=b\wedge permitted(x)(leftOutcome))\wedge \exists x:Case,admissible(x)\wedge publicLaw(x)=b\wedge permitted(x)(rightOutcome)\Rightarrow ((\forall u,projection(sectionAlpha(u))=projection(sectionBeta(u))\wedge projection(sectionBeta(u))=projection(sectionGamma(u)))\wedge (\forall u,sectionGamma(u)=sectionAlpha(u)+hiddenEquiv(jumpAlphaGamma(u))⟺\forall u,jumpAlphaGamma(u)=jumpAlphaBeta(u)+jumpBetaGamma(u))\wedge (\exists u,jumpAlphaGamma(u)\ne jumpAlphaBeta(u)+jumpBetaGamma(u)\Rightarrow \exists u,sectionGamma(u)\ne sectionAlpha(u)+hiddenEquiv(jumpAlphaGamma(u))))\wedge \neg (\exists !candidate:Outcome,\exists x:Case,admissible(x)\wedge publicLaw(x)=b\wedge permitted(x)(candidate)).$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/Policy/CocyclePolicySeparation.cocycle_does_not_select_policy (✓ std3). ∎

Source. Repository-derived.

Commentary.

The hidden-jump construction records visible agreement, the endpoint/cocycle equivalence, and an explicit endpoint residual when the selected jumps disagree.

The same public model carries a permitted-outcome relation with two distinct outcomes in one public-law fiber. Consequently the cocycle law supplies composition and accounting, but no unique policy choice.

References

• Truth anchor: D5/S3/ConceptDynamics/Policy/CocyclePolicySeparation.cocycle_does_not_select_policy
• Dependency: D5/S1/Dynamics/JumpCocycle
• Dependency: D5/S3/ConceptDynamics/Policy/DiscretionaryOutcomeNonuniqueness