Initialized endpoint control protocols

Abstract

Persistent endpoint states, agreed public roots and sender-local bit queries generate actual support and protocol-realized transitions.

Definition 1.1 (A source-local public prefix protocol).

$$\forall MA:Typ{e}_u,(\forall MB:Typ{e}_v,(\forall OA:Typ{e}_w,(\forall OB:Typ{e}_x,((\mathrm{Question}(MA,MB)=\mathrm{Sum}((MA)\to (\mathrm{Bool}()),(MB)\to (\mathrm{Bool}())))\wedge (\mathrm{EndpointProtocol}(MA,MB,OA,OB)=\{node:(\mathrm{List}(\mathrm{Bool}()))\to (\mathrm{Sum}(\mathrm{Question}(MA,MB),\mathrm{Unit}())),outA:(MA)\to ((\mathrm{List}(\mathrm{Bool}()))\to (OA)),outB:(MB)\to ((\mathrm{List}(\mathrm{Bool}()))\to (OB))\})))))$$

Formalization. D5/S3/ObserverMemory/Algorithms/InitializedControlProtocol.EndpointProtocol (✓ std3).

Source. Repository-derived.

Commentary.

A public bit prefix determines either a tagged sender-local Boolean question or a leaf. A left question reads only the old left state and a right question reads only the old right state. Each leaf output takes only its own old local state and the transmitted Boolean string. Query labels are evaluator data reconstructed from the public prefix, and the leaf outputs never read them as an additional channel.

$\forall MA:Typ{e}_u,(\forall MB:Typ{e}_v,(\forall OA:Typ{e}_w,(\forall OB:Typ{e}_x,(\forall p:\mathrm{EndpointProtocol}(MA,MB,OA,OB),((\mathrm{Trace}(MA,MB)=\mathrm{List}(\mathrm{Sigma}(q:\mathrm{Question}(MA,MB)\mapsto \mathrm{Bool}())))\wedge (\forall t:\mathrm{Trace}(MA,MB),(\mathrm{bits}(t)=\mathrm{map}(e\mapsto \mathrm{snd}(e),t)))\wedge (\forall left:(MA)\to (\mathrm{Bool}()),(\forall a:MA,(\forall b:MB,(\mathrm{answer}(\mathrm{inl}(left),(a,b))=\mathrm{apply}(left,a)))))\wedge (\forall right:(MB)\to (\mathrm{Bool}()),(\forall a:MA,(\forall b:MB,(\mathrm{answer}(\mathrm{inr}(right),(a,b))=\mathrm{apply}(right,b)))))\wedge (\forall t:\mathrm{Trace}(MA,MB),((\mathrm{policy}(p,t)=\mathrm{node}(p,\mathrm{bits}(t)))\wedge (\mathrm{rightCount}(t)=\mathrm{length}(\mathrm{filter}(\mathrm{rightSender}(),t)))\wedge (\mathrm{leftCount}(t)=\mathrm{length}(\mathrm{filter}(\mathrm{leftSender}(),t)))))\wedge (\forall h:\mathrm{List}(\mathrm{Bool}()),((\mathrm{PublicTrace}(p,h,\mathrm{nil}())⟺(\mathrm{node}(p,h)=\mathrm{inr}(\mathrm{unit}())))\wedge (\forall q:\mathrm{Question}(MA,MB),(\forall y:\mathrm{Bool}(),(\forall tail:\mathrm{Trace}(MA,MB),(\mathrm{PublicTrace}(p,h,\mathrm{cons}((q,y),tail))⟺((\mathrm{node}(p,h)=\mathrm{inl}(q))\wedge (\mathrm{PublicTrace}(p,\mathrm{append}(h,\mathrm{singleton}(y)),tail))))))))))))))$

All universe levels u,v,w,x are arbitrary. rightSender and leftSender test the right and left question tags of a trace entry. The evaluator is PassivePolicyNormalization.execute. Its input and the two local carriers are arbitrary types. Finite fuel is evidence of termination on the actual input; it is not a uniform tree depth or an endpoint runtime argument.

Definition 1.2 (Initialized persistent endpoint compliance).

$$\forall d:\mathbb{N},(\forall A:\mathrm{Submodule}(\mathrm{ZMod}(2),\mathrm{Source}(d)),(\forall B:\mathrm{Submodule}(\mathrm{ZMod}(2),\mathrm{Source}(d)),(\forall h:\mathrm{IsCompl}(A,B),(\forall MA:Typ{e}_u,(\forall MB:Typ{e}_v,(\forall Root:Typ{e}_w,((\mathrm{Source}(d)=\mathrm{Prod}((\mathrm{Fin}(d))\to (\mathrm{ZMod}(2)),\mathrm{ZMod}(2)))\wedge (\mathrm{pA}()=\mathrm{projectionOnto}(A,B,h))\wedge (\mathrm{pB}()=\mathrm{projectionOnto}(B,A,\mathrm{symm}(h)))\wedge (\mathrm{ControllerData}(d,A,B,MA,MB,Root)=\{readA:(MA)\to (A),readB:(MB)\to (B),initA:(A)\to (MA),initB:(B)\to (MB),readInitA:\forall a:A,(\mathrm{readA}(\mathrm{initA}(a))=a),readInitB:\forall b:B,(\mathrm{readB}(\mathrm{initB}(b))=b),rootA:(\mathrm{Action}(d))\to ((MA)\to (Root)),rootB:(\mathrm{Action}(d))\to ((MB)\to (Root)),protocol:(\mathrm{Action}(d))\to ((Root)\to (\mathrm{EndpointProtocol}(MA,MB,MA,MB)))\})\wedge (\forall C:\mathrm{ControllerData}(d,A,B,MA,MB,Root),(\forall f:\mathrm{Action}(d),(\forall m:\mathrm{Prod}(MA,MB),(\forall t:\mathrm{Trace}(MA,MB),((\mathrm{Exec}(C,f,m,t)⟺(\exists n:\mathbb{N},(\mathrm{execute}(\mathrm{answer}(),\mathrm{policy}(\mathrm{protocol}(C,f,\mathrm{rootA}(C,f,\mathrm{fst}(m)))),n,\mathrm{nil}(),m)=\mathrm{some}((t,\mathrm{unit}())))))\wedge (\mathrm{commit}(C,f,m,t)=(\mathrm{outA}(\mathrm{protocol}(C,f,\mathrm{rootA}(C,f,\mathrm{fst}(m))),\mathrm{fst}(m),\mathrm{bits}(t)),\mathrm{outB}(\mathrm{protocol}(C,f,\mathrm{rootA}(C,f,\mathrm{fst}(m))),\mathrm{snd}(m),\mathrm{bits}(t))))\wedge (\mathrm{Reachable}(C,m)⟺(\forall R:(\mathrm{Prod}(MA,MB))\to (\mathrm{Prop}()),(((\forall a:A,(\forall b:B,(\mathrm{apply}(R,(\mathrm{initA}(C,a),\mathrm{initB}(C,b))))))\wedge (\forall mzero:\mathrm{Prod}(MA,MB),((\mathrm{apply}(R,mzero))⟹(\forall f:\mathrm{Action}(d),(\forall t:\mathrm{Trace}(MA,MB),((\mathrm{Exec}(C,f,mzero,t))⟹(\mathrm{apply}(R,\mathrm{commit}(C,f,mzero,t)))))))))⟹(\mathrm{apply}(R,m))))))))))\wedge (\mathrm{Controller}(h,MA,MB,Root)=\{C:\mathrm{ControllerData}(d,A,B,MA,MB,Root)\mid (\forall m:\mathrm{Prod}(MA,MB),((\mathrm{Reachable}(C,m))⟹(\forall f:\mathrm{Action}(d),(\mathrm{rootA}(C,f,\mathrm{fst}(m))=\mathrm{rootB}(C,f,\mathrm{snd}(m))))))\wedge (\forall m:\mathrm{Prod}(MA,MB),((\mathrm{Reachable}(C,m))⟹(\forall f:\mathrm{Action}(d),(\exists t:\mathrm{Trace}(MA,MB),(\mathrm{Exec}(C,f,m,t))))))\wedge (\forall x:MA,(\exists y:MB,(\mathrm{Reachable}(C,(x,y)))))\wedge (\forall y:MB,(\exists x:MA,(\mathrm{Reachable}(C,(x,y)))))\wedge (\forall m:\mathrm{Prod}(MA,MB),((\mathrm{Reachable}(C,m))⟹(\forall f:\mathrm{Action}(d),(\forall t:\mathrm{Trace}(MA,MB),((\mathrm{Exec}(C,f,m,t))⟹((\mathrm{readA}(C,\mathrm{fst}(\mathrm{commit}(C,f,m,t)))=\mathrm{pA}(\mathrm{apply}(f,\mathrm{readA}(C,\mathrm{fst}(m))+\mathrm{readB}(C,\mathrm{snd}(m)))))\wedge (\mathrm{readB}(C,\mathrm{snd}(\mathrm{commit}(C,f,m,t)))=\mathrm{pB}(\mathrm{apply}(f,\mathrm{readA}(C,\mathrm{fst}(m))+\mathrm{readB}(C,\mathrm{snd}(m)))))))))))\wedge (\forall m:\mathrm{Prod}(MA,MB),((\mathrm{Reachable}(C,m))⟹(\forall t:\mathrm{Trace}(MA,MB),((\forall i:\mathrm{Fin}(d),((\mathrm{Exec}(C,\mathrm{dataTranslation}(i),m,t))⟹(t=\mathrm{nil}())))\wedge ((\mathrm{Exec}(C,\mathrm{controlTranslation}(),m,t))⟹(t=\mathrm{nil}()))))))\}))))))))$$

Formalization. D5/S3/ObserverMemory/Algorithms/InitializedControlProtocol.Controller (✓ std3).

Source. Repository-derived.

Commentary.

The original source is the direct product of the data vector and its control coordinate. The action alphabet includes every data basis translation, the control basis translation, and every established controlRewrite. A fixed complementary pair of submodules supplies the two original readouts.

$\forall d:\mathbb{N},((\mathrm{Source}(d)=\mathrm{Prod}((\mathrm{Fin}(d))\to (\mathrm{ZMod}(2)),\mathrm{ZMod}(2)))\wedge (\mathrm{Action}(d)=\{\mathrm{dataTranslation}(i)\mid i\in \mathrm{Fin}(d)\}\cup \{\mathrm{controlTranslation}()\}\cup \{\mathrm{rewrite}(i)\mid i\in \mathrm{Fin}(d)\})\wedge (\forall i:\mathrm{Fin}(d),(\forall z:\mathrm{Source}(d),((\mathrm{apply}(\mathrm{dataTranslation}(i),z)=z+(\mathrm{single}(i,1),0))\wedge (\mathrm{apply}(\mathrm{rewrite}(i),z)=\mathrm{controlRewrite}(i,z))\wedge (\mathrm{controlRewrite}(i,z)=(\mathrm{single}(i,\mathrm{snd}(z)),0)))))\wedge (\forall z:\mathrm{Source}(d),(\mathrm{apply}(\mathrm{controlTranslation}(),z)=z+(0,1))))$

Reachable is the least predicate containing all initial pairs and closed under successful commits; the formula gives its induction characterization. Each endpoint initializes from its own original projection and reads that projection back exactly. Operational reachability begins with the full local initialization product and closes under successful executions and the two local leaf commits. Both local carriers must be exactly projections of this operational support.

Compliance requires locally selected roots to agree on actual support, finite termination there, both prescribed source readout equations after every execution, and zero-bit basis translations. Neither local carrier nor the root type is assumed finite. The readout equations specify correctness and do not implement a centralized transition.

Definition 1.3 (Actual support determines a total realized step).

$$\forall d:\mathbb{N},(\forall A:\mathrm{Submodule}(\mathrm{ZMod}(2),\mathrm{Source}(d)),(\forall B:\mathrm{Submodule}(\mathrm{ZMod}(2),\mathrm{Source}(d)),(\forall h:\mathrm{IsCompl}(A,B),(\forall MA:Typ{e}_u,(\forall MB:Typ{e}_v,(\forall Root:Typ{e}_w,(\forall C:\mathrm{Controller}(h,MA,MB,Root),(\forall a:A,(\forall b:B,(\forall f:\mathrm{Action}(d),(\forall m:\mathrm{State}(C),((\mathrm{State}(C)=\{q:\mathrm{Prod}(MA,MB)\mid \mathrm{Reachable}(\mathrm{toControllerData}(C),q)\})\wedge (\mathrm{trace}(C,f,m)=\mathrm{choose}(\exists t:\mathrm{Trace}(MA,MB),(\mathrm{Exec}(\mathrm{toControllerData}(C),f,\mathrm{val}(m),t))))\wedge (\mathrm{val}(\mathrm{step}(C,f,m))=\mathrm{commit}(\mathrm{toControllerData}(C),f,\mathrm{val}(m),\mathrm{trace}(C,f,m)))\wedge (\mathrm{cost}(C,m,f)=\mathrm{length}(\mathrm{trace}(C,f,m)))\wedge (\mathrm{val}(\mathrm{initial}(C,a,b))=(\mathrm{initA}(C,a),\mathrm{initB}(C,b)))\wedge (\mathrm{readout}(C,m)=\mathrm{readA}(C,\mathrm{fst}(\mathrm{val}(m)))+\mathrm{readB}(C,\mathrm{snd}(\mathrm{val}(m))))))))))))))))$$

Formalization. D5/S3/ObserverMemory/Algorithms/InitializedControlProtocol.step (✓ std3).

Source. Repository-derived.

Commentary.

For an actual reachable pair and a public action, finite termination selects a successful evaluator transcript. The successor consists of the two local leaf updates on its Boolean responses. Operational closure places it back in the actual reachable subtype. Step cost is the transcript length. Existing runWord and Comm supply word execution and cumulative cost.

References

• Truth anchor: D5/S3/ObserverMemory/Algorithms/InitializedControlProtocol.Controller
• Truth anchor: D5/S3/ObserverMemory/Algorithms/InitializedControlProtocol.EndpointProtocol
• Truth anchor: D5/S3/ObserverMemory/Algorithms/InitializedControlProtocol.step
• Dependency: D5/S3/ConceptDynamics/Experiment/PassivePolicyNormalization
• Dependency: D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound
• Dependency: D5/S3/ObserverMemory/Prediction/ActionGraphCommunicationBound