Exact Causal Repair Error

Abstract

Common causal envelopes give an optimal repair of a finite response table.

Definition 1.1 (Feedback event distance).

$$\forall T:\mathbb{N},\forall A:(\mathrm{Fin}(T))\to \mathrm{Type}(),\forall Y:(\mathrm{Fin}(T))\to \mathrm{Type}(),[\forall t:\mathrm{Fin}(T),\mathrm{Fintype}(A(t))],[\forall t:\mathrm{Fin}(T),\mathrm{Nonempty}(A(t))],[\forall t:\mathrm{Fin}(T),\mathrm{Fintype}(Y(t))],\forall P:((t:\mathrm{Fin}(T))\to Y(t))\to ((t:\mathrm{Fin}(T))\to A(t))\to \mathbb{R},\forall Q:((t:\mathrm{Fin}(T))\to Y(t))\to ((t:\mathrm{Fin}(T))\to A(t))\to \mathbb{R},\mathrm{feedbackDistance}(P,Q)=\underset{f:(t:\mathrm{Fin}(T))\to (\mathrm{Prefix}(Y,t.val))\to A(t),E:\mathrm{Set}((t:\mathrm{Fin}(T))\to Y(t))}{\max }|\sum _{y:(t:\mathrm{Fin}(T))\to Y(t),y\in E}(P(y)(\mathrm{feedbackActions}(f,y))-Q(y)(\mathrm{feedbackActions}(f,y)))|$$

Formalization. D5/S3/ObserverMemory/Prediction/CausalRepairEnvelopes.feedbackDistance (✓ std3).

Source. Repository-derived.

Commentary.

The maximum ranges over every deterministic causal strategy and every event of complete output words. The response after feedback need not be normalized, so the quantity compares event masses.

Definition 1.2 (Feedback normalization defect).

$$\forall T:\mathbb{N},\forall A:(\mathrm{Fin}(T))\to \mathrm{Type}(),\forall Y:(\mathrm{Fin}(T))\to \mathrm{Type}(),[\forall t:\mathrm{Fin}(T),\mathrm{Fintype}(A(t))],[\forall t:\mathrm{Fin}(T),\mathrm{Nonempty}(A(t))],[\forall t:\mathrm{Fin}(T),\mathrm{Fintype}(Y(t))],\forall P:((t:\mathrm{Fin}(T))\to Y(t))\to ((t:\mathrm{Fin}(T))\to A(t))\to \mathbb{R},\mathrm{feedbackDefect}(P)=\underset{f:(t:\mathrm{Fin}(T))\to (\mathrm{Prefix}(Y,t.val))\to A(t)}{\max }|\mathrm{feedbackMass}(P,f)-1|$$

Formalization. D5/S3/ObserverMemory/Prediction/CausalRepairEnvelopes.feedbackDefect (✓ std3).

Source. Repository-derived.

Commentary.

The defect is the largest absolute difference between a fed-back total mass and one.

Theorem 1.3 (Attained optimal causal repair).

$$\forall T:\mathbb{N},\forall A:(\mathrm{Fin}(T))\to \mathrm{Type}(),\forall Y:(\mathrm{Fin}(T))\to \mathrm{Type}(),[\forall t:\mathrm{Fin}(T),\mathrm{Fintype}(A(t))],[\forall t:\mathrm{Fin}(T),\mathrm{Nonempty}(A(t))],[\forall t:\mathrm{Fin}(T),\mathrm{Fintype}(Y(t))],[\forall t:\mathrm{Fin}(T),\mathrm{Nonempty}(Y(t))],[\forall t:\mathrm{Fin}(T),\mathrm{DecidableEq}(Y(t))],(1\le T)\Rightarrow (\forall P:((t:\mathrm{Fin}(T))\to Y(t))\to ((t:\mathrm{Fin}(T))\to A(t))\to \mathbb{R},(\forall y:(t:\mathrm{Fin}(T))\to Y(t),\forall a:(t:\mathrm{Fin}(T))\to A(t),0\le P(y)(a))\Rightarrow ((\forall a:(t:\mathrm{Fin}(T))\to A(t),\sum _{y:(t:\mathrm{Fin}(T))\to Y(t)}P(y)(a)=1)\Rightarrow (\exists Q:((t:\mathrm{Fin}(T))\to Y(t))\to ((t:\mathrm{Fin}(T))\to A(t))\to \mathbb{R},(\forall y:(t:\mathrm{Fin}(T))\to Y(t),\forall a:(t:\mathrm{Fin}(T))\to A(t),0\le Q(y)(a))\wedge (\forall a:(t:\mathrm{Fin}(T))\to A(t),\sum _{y:(t:\mathrm{Fin}(T))\to Y(t)}Q(y)(a)=1)\wedge (\forall n:\mathbb{N},(n\le T)\Rightarrow (\forall x:\mathrm{Prefix}(Y,n),\forall a:(t:\mathrm{Fin}(T))\to A(t),\forall b:(t:\mathrm{Fin}(T))\to A(t),(\forall i:\mathrm{Fin}(T),(i.val<n)\Rightarrow (a(i)=b(i)))\Rightarrow (\mathrm{prefixMarginal}(Q,n,x,a)=\mathrm{prefixMarginal}(Q,n,x,b))))\wedge (\mathrm{feedbackDistance}(P,Q)=\mathrm{feedbackDefect}(P))\wedge (\forall R:((t:\mathrm{Fin}(T))\to Y(t))\to ((t:\mathrm{Fin}(T))\to A(t))\to \mathbb{R},(\forall y:(t:\mathrm{Fin}(T))\to Y(t),\forall a:(t:\mathrm{Fin}(T))\to A(t),0\le R(y)(a))\Rightarrow ((\forall a:(t:\mathrm{Fin}(T))\to A(t),\sum _{y:(t:\mathrm{Fin}(T))\to Y(t)}R(y)(a)=1)\Rightarrow ((\forall n:\mathbb{N},(n\le T)\Rightarrow (\forall x:\mathrm{Prefix}(Y,n),\forall a:(t:\mathrm{Fin}(T))\to A(t),\forall b:(t:\mathrm{Fin}(T))\to A(t),(\forall i:\mathrm{Fin}(T),(i.val<n)\Rightarrow (a(i)=b(i)))\Rightarrow (\mathrm{prefixMarginal}(R,n,x,a)=\mathrm{prefixMarginal}(R,n,x,b))))\Rightarrow (\mathrm{feedbackDefect}(P)\le \mathrm{feedbackDistance}(P,R))))))))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/CausalRepairEnvelopes.result (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every nonnegative finite response table normalized at each fixed action word admits a causal probability table with event distance exactly equal to its feedback normalization defect. Every other causal probability table has at least that distance.

Backward recursion takes the maximum and minimum, over the next action, of the sums of branch continuation masses. Tail strategies chosen independently on different output branches join into one causal strategy.

The forward upper construction pads the maximizing branch envelopes with nonnegative mass on a fixed output word. The lower construction scales the minimizing branch envelopes by the parent-to-child total-mass ratio; a zero denominator has zero parent mass.

A convex combination of these common envelopes has total mass one under every strategy. The feedback normalization criterion then gives prefix causality. Event discrepancies are bounded by the upper mass minus one and by one minus the lower mass; the complete output event supplies the matching universal lower bound.

References

• Truth anchor: D5/S3/ObserverMemory/Prediction/CausalRepairEnvelopes.feedbackDefect
• Truth anchor: D5/S3/ObserverMemory/Prediction/CausalRepairEnvelopes.feedbackDistance
• Truth anchor: D5/S3/ObserverMemory/Prediction/CausalRepairEnvelopes.result
• Dependency: D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion