Feedback Normalization Criterion

Abstract

Finite feedback normalization is equivalent to prefix causality and sequential kernel factorization.

Definition 1.1 (Dependent output and action prefixes).

$$\begin{gathered} \forall T:\mathbb{N},X:(\mathrm{Fin}(T))\to \mathrm{Type},n:\mathbb{N}, \\ \mathrm{Prefix}(X,n)=(i:\{i:\mathrm{Fin}(T)//i.val<n\})\to X(i.1). \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.Prefix (✓ std3).

Source. Repository-derived.

Commentary.

A prefix of length n is a dependent word on precisely the rounds whose indices are below n.

Definition 1.2 (Restriction to an initial prefix).

$$\begin{gathered} \forall T:\mathbb{N},X:(\mathrm{Fin}(T))\to \mathrm{Type},x:(t:\mathrm{Fin}(T))\to X(t),n:\mathbb{N},i:\{i:\mathrm{Fin}(T)//i.val<n\}, \\ \mathrm{restrictPrefix}(x,n)(i)=x(i.1). \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.restrictPrefix (✓ std3).

Source. Repository-derived.

Commentary.

A complete dependent word restricts to a prefix by evaluation at the underlying round index.

Definition 1.3 (Splicing at a round cut).

$$\begin{gathered} \forall T:\mathbb{N},X:(\mathrm{Fin}(T))\to \mathrm{Type},n:\mathbb{N},u:\mathrm{Prefix}(X,n),v:(i:\{i:\mathrm{Fin}(T)//n\le i.val\})\to X(i.1), \\ \forall i:\mathrm{Fin}(T),\mathrm{spliceWords}(n,u,v)(i)=\text{if}i.val<n\text{then}u(⟨i,i.val<n⟩)\text{else}v(⟨i,n\le i.val⟩). \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.spliceWords (✓ std3).

Source. Repository-derived.

Commentary.

A prefix and a suffix beginning at the cut determine a complete dependent word.

Definition 1.4 (Actions selected by causal feedback).

$$\begin{gathered} \forall T:\mathbb{N},A:(\mathrm{Fin}(T))\to \mathrm{Type},Y:(\mathrm{Fin}(T))\to \mathrm{Type},f:(t:\mathrm{Fin}(T))\to (\mathrm{Prefix}(Y,t.val))\to A(t),y:(t:\mathrm{Fin}(T))\to Y(t), \\ \forall t:\mathrm{Fin}(T),\mathrm{feedbackActions}(f,y)(t)=f(t)(\mathrm{restrictPrefix}(y,t.val)). \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.feedbackActions (✓ std3).

Source. Repository-derived.

Commentary.

At round t, the feedback action is the strategy value on the output prefix strictly before t.

Definition 1.5 (Fed-back total mass).

$$\begin{gathered} \forall T:\mathbb{N},A:(\mathrm{Fin}(T))\to \mathrm{Type},Y:(\mathrm{Fin}(T))\to \mathrm{Type},[\forall t:\mathrm{Fin}(T),\mathrm{Fintype}(Y(t))],P:((t:\mathrm{Fin}(T))\to Y(t))\to ((t:\mathrm{Fin}(T))\to A(t))\to \mathbb{R},f:(t:\mathrm{Fin}(T))\to (\mathrm{Prefix}(Y,t.val))\to A(t), \\ \mathrm{feedbackMass}(P,f)=\sum _{y:(t:\mathrm{Fin}(T))\to Y(t)}P(y)(\mathrm{feedbackActions}(f,y)). \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.feedbackMass (✓ std3).

Source. Repository-derived.

Commentary.

The fed-back mass sums the response table over output words after substituting the causal action word.

Definition 1.6 (Point prefix marginal).

$$\begin{gathered} \forall T:\mathbb{N},A:(\mathrm{Fin}(T))\to \mathrm{Type},Y:(\mathrm{Fin}(T))\to \mathrm{Type},[\forall t:\mathrm{Fin}(T),\mathrm{Fintype}(Y(t))],[\forall t:\mathrm{Fin}(T),\mathrm{DecidableEq}(Y(t))],P:((t:\mathrm{Fin}(T))\to Y(t))\to ((t:\mathrm{Fin}(T))\to A(t))\to \mathbb{R},n:\mathbb{N},x:\mathrm{Prefix}(Y,n),a:(t:\mathrm{Fin}(T))\to A(t), \\ \mathrm{prefixMarginal}(P,n,x,a)=\sum _{y:(t:\mathrm{Fin}(T))\to Y(t)}\text{if}\mathrm{restrictPrefix}(y,n)=x\text{then}P(y)(a)\text{else}0. \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.prefixMarginal (✓ std3).

Source. Repository-derived.

Commentary.

The point prefix marginal sums the response table over complete output words with the specified restriction.

Definition 1.7 (Event prefix marginal).

$$\begin{gathered} \forall T:\mathbb{N},A:(\mathrm{Fin}(T))\to \mathrm{Type},Y:(\mathrm{Fin}(T))\to \mathrm{Type},[\forall t:\mathrm{Fin}(T),\mathrm{Fintype}(Y(t))],[\forall t:\mathrm{Fin}(T),\mathrm{DecidableEq}(Y(t))],P:((t:\mathrm{Fin}(T))\to Y(t))\to ((t:\mathrm{Fin}(T))\to A(t))\to \mathbb{R},n:\mathbb{N},E:\mathrm{Set}(\mathrm{Prefix}(Y,n)),a:(t:\mathrm{Fin}(T))\to A(t), \\ \mathrm{prefixEventMarginal}(P,n,E,a)=\sum _{y:(t:\mathrm{Fin}(T))\to Y(t)}\text{if}\mathrm{restrictPrefix}(y,n)\in E\text{then}P(y)(a)\text{else}0. \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.prefixEventMarginal (✓ std3).

Source. Repository-derived.

Commentary.

The event prefix marginal sums over complete output words whose restriction belongs to the event.

Definition 1.8 (Single-cut feedback switch).

$$\begin{gathered} \forall T:\mathbb{N},A:(\mathrm{Fin}(T))\to \mathrm{Type},Y:(\mathrm{Fin}(T))\to \mathrm{Type},n:\mathbb{N},u:\mathrm{Prefix}(A,n),v:(i:\{i:\mathrm{Fin}(T)//n\le i.val\})\to A(i.1),w:(i:\{i:\mathrm{Fin}(T)//n\le i.val\})\to A(i.1),E:\mathrm{Set}(\mathrm{Prefix}(Y,n)), \\ \forall t:\mathrm{Fin}(T),history:\mathrm{Prefix}(Y,t.val),\mathrm{singleCutSwitch}(n,u,v,w,E)(t)(history)=\text{if}t.val<n\text{then}u(⟨t,t.val<n⟩)\text{else}\text{let}x:\mathrm{Prefix}(Y,n):=\lambda i\mapsto history(⟨i.1,i.1.val<t.val⟩);\text{if}x\in E\text{then}v(⟨t,n\le t.val⟩)\text{else}w(⟨t,n\le t.val⟩). \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.singleCutSwitch (✓ std3).

Source. Repository-derived.

Commentary.

Before the cut the strategy follows u; from the cut onward it selects v or w according to the observed prefix event.

Theorem 1.9 (Feedback normalization, prefix causality, and sequential kernels).

$$\begin{gathered} \forall T:\mathbb{N},1\le T, \\ A:(\mathrm{Fin}(T))\to \mathrm{Type},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{DecidableEq}(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))], \\ 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),a:(t:\mathrm{Fin}(T))\to A(t),0\le P(y)(a)), \\ (\forall a:(t:\mathrm{Fin}(T))\to A(t),\sum _{y:(t:\mathrm{Fin}(T))\to Y(t)}P(y)(a)=1), \\ List.TFAE([(\forall f:(t:\mathrm{Fin}(T))\to (\mathrm{Prefix}(Y,t.val))\to A(t),\mathrm{feedbackMass}(P,f)=1), \\ (\forall n:\mathbb{N},(1\le n)\Rightarrow ((n<T)\Rightarrow (\forall u:\mathrm{Prefix}(A,n),v:(i:\{i:\mathrm{Fin}(T)//n\le i.val\})\to A(i.1),w:(i:\{i:\mathrm{Fin}(T)//n\le i.val\})\to A(i.1),E:\mathrm{Set}(\mathrm{Prefix}(Y,n)),\mathrm{feedbackMass}(P,\mathrm{singleCutSwitch}(n,u,v,w,E))=1))), \\ (\forall n:\mathbb{N},(n\le T)\Rightarrow (\forall x:\mathrm{Prefix}(Y,n),a:(t:\mathrm{Fin}(T))\to A(t),b:(t:\mathrm{Fin}(T))\to A(t),(\forall i:\mathrm{Fin}(T),(i.val<n)\Rightarrow (a(i)=b(i)))\Rightarrow (\mathrm{prefixMarginal}(P,n,x,a)=\mathrm{prefixMarginal}(P,n,x,b)))), \\ (\exists q:(t:\mathrm{Fin}(T))\to (\mathrm{Prefix}(A,t.val+1))\to (\mathrm{Prefix}(Y,t.val))\to (Y(t))\to \mathbb{R},(\forall t:\mathrm{Fin}(T),a:\mathrm{Prefix}(A,t.val+1),h:\mathrm{Prefix}(Y,t.val),z:Y(t),0\le q(t)(a)(h)(z))\wedge (\forall t:\mathrm{Fin}(T),a:\mathrm{Prefix}(A,t.val+1),h:\mathrm{Prefix}(Y,t.val),\sum _{z:Y(t)}q(t)(a)(h)(z)=1)\wedge (\forall y:(t:\mathrm{Fin}(T))\to Y(t),a:(t:\mathrm{Fin}(T))\to A(t),P(y)(a)=\prod _{t:\mathrm{Fin}(T)}q(t)(\mathrm{restrictPrefix}(a,t.val+1))(\mathrm{restrictPrefix}(y,t.val))(y(t))))]). \end{gathered}$$

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

Source. Repository-derived.

Commentary.

For finite nonempty dependent round alphabets and a nonnegative normalized response table, the four displayed conditions are equivalent.

A single-cut switch has mass one plus the difference of its two prefix-event marginals. Singleton events therefore force future-action independence of every prefix marginal.

Recursive marginalization yields normalized ratio kernels on positive parent prefixes and one fixed normalized extension on null parents. Conversely, backward summation of normalized kernels makes every causal feedback mass equal to one.

References

• Truth anchor: D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.Prefix
• Truth anchor: D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.feedbackActions
• Truth anchor: D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.feedbackMass
• Truth anchor: D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.feedback_normalization_prefix_causality_sequential_kernels
• Truth anchor: D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.prefixEventMarginal
• Truth anchor: D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.prefixMarginal
• Truth anchor: D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.restrictPrefix
• Truth anchor: D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.singleCutSwitch
• Truth anchor: D5/S3/ObserverMemory/Prediction/FeedbackNormalizationCriterion.spliceWords