Shared Control-Bit Storage Bound

Abstract

Shared control rewrites force a sharp product bound for two jointly faithful finite codes.

Definition 1.1 (A control bit is written into one data coordinate).

$$\begin{gathered} \forall d:\mathbb{N},i:\mathrm{Fin}(d),z:((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2)), \\ controlRewrit{e}_i(z)=(\mathrm{single}(i,z_2),0). \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.controlRewrite (✓ std3).

Source. Repository-derived.

Commentary.

The rewrite indexed by i clears every data coordinate except i, copies the control bit into coordinate i, and then clears the control bit.

Definition 1.2 (The allowed translations and rewrites).

$$\forall d:\mathbb{N},sharedControlAction{s}_d=\{f:(((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2)))\to ((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2))\mid (\exists i:\mathrm{Fin}(d),f=(z:((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2))\mapsto z+(\mathrm{single}(i,1),0)))\vee (f=(z:((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2))\mapsto z+(0,1)))\vee (\exists i:\mathrm{Fin}(d),f=controlRewrit{e}_i)\}.$$

Formalization. D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.sharedControlActions (✓ std3).

Source. Repository-derived.

Commentary.

The action set contains translation by each data basis vector, translation by the control basis vector, and every indexed control rewrite.

Definition 1.3 (Every state action descends to the code).

$$\begin{gathered} \forall d:\mathbb{N},\alpha :Type,u:(((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2)))\to \alpha , \\ \mathrm{DynamicallyClosed}(u)⟺\forall f\in sharedControlAction{s}_d,\exists F:(\alpha )\to \alpha ,u\circ f=F\circ u. \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.DynamicallyClosed (✓ std3).

Source. Repository-derived.

Commentary.

A code is dynamically closed when each allowed action has an induced update on code values, with the two routes from a state to a new code value equal.

Definition 1.4 (The prefix code).

$$\begin{gathered} \forall d:\mathbb{N},h:\mathbb{N},p:h\le d,z:((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2)), \\ prefixCod{e}_p(z)=((i:\mathrm{Fin}(h)\mapsto z_1(\mathrm{castLE}(p,i))),z_2). \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.prefixCode (✓ std3).

Source. Repository-derived.

Commentary.

For h at most d, the prefix code retains the first h data coordinates and the shared control bit.

Definition 1.5 (The suffix code).

$$\begin{gathered} \forall d:\mathbb{N},h:\mathbb{N},p:h\le d,z:((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2)), \\ suffixCod{e}_p(z)=((i:\mathrm{Fin}(d-h)\mapsto z_1(h+i)),z_2). \end{gathered}$$

Formalization. D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.suffixCode (✓ std3).

Source. Repository-derived.

Commentary.

For h at most d, the suffix code retains data coordinates h through d minus one and the shared control bit.

Theorem 1.6 (Classification, storage lower bound, and attainment).

$$\begin{gathered} \forall d:\mathbb{N},2\le d,\alpha :Type,\beta :Type,[\mathrm{Finite}(\alpha )],[\mathrm{Finite}(\beta )], \\ u:(((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2)))\to \alpha ,v:(((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2)))\to \beta , \\ (\mathrm{DynamicallyClosed}(u)\wedge \mathrm{DynamicallyClosed}(v)\wedge \mathrm{Injective}((z:((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2))\mapsto (u(z),v(z)))))\Rightarrow \\ (\exists K:\mathrm{Submodule}(\mathrm{ZMod}(2),((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2))), \\ (\forall z:((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2)),y:((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2)),(u(z)=u(y))⟺((z-y)\in K))\wedge \\ ((K\subseteq \mathrm{range}(\mathrm{inl}(\mathrm{ZMod}(2),(\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2))))\vee (K=\mathrm{top}())))\wedge \\ (\forall K:\mathrm{Submodule}(\mathrm{ZMod}(2),((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2))), \\ ((K\subseteq \mathrm{range}(\mathrm{inl}(\mathrm{ZMod}(2),(\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2))))\vee (K=\mathrm{top}()))\Rightarrow \\ ((\mathrm{DynamicallyClosed}(\mathrm{mkQ}(K)))\wedge \\ (\forall z:((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2)),y:((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2)),(\mathrm{mkQ}(K)(z)=\mathrm{mkQ}(K)(y))⟺((z-y)\in K))))\wedge \\ (((\neg \mathrm{Injective}(u))\wedge (\neg \mathrm{Injective}(v)))\Rightarrow (2^{(d+2)}\le (\mathrm{ncard}(\mathrm{range}(u))\cdot \mathrm{ncard}(\mathrm{range}(v)))))\wedge \\ (\forall h:\mathbb{N},((1\le h)\wedge (h\le (d-1)))\Rightarrow \\ ((\mathrm{DynamicallyClosed}(suffixCod{e}_{h\le d}))\wedge (\mathrm{DynamicallyClosed}(prefixCod{e}_{h\le d}))\wedge \\ (\mathrm{Injective}((z:((\mathrm{Fin}(d))\to \mathrm{ZMod}(2),\mathrm{ZMod}(2))\mapsto (suffixCod{e}_{h\le d}(z),prefixCod{e}_{h\le d}(z)))))\wedge \\ ((\mathrm{ncard}(\mathrm{range}(suffixCod{e}_{h\le d}))\cdot \mathrm{ncard}(\mathrm{range}(prefixCod{e}_{h\le d})))=2^{(d+2)}))). \end{gathered}$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.shared_control_bit_storage_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Translation closure makes each fiber relation a coset relation of a ZMod 2 subspace. Stability under the control rewrites then forces that subspace either into the data hyperplane or to be the whole state space.

Conversely, every subspace of the data hyperplane, together with the whole state space, is realized by its finite quotient code. Translations descend by quotient addition, while each linear control rewrite vanishes on the data hyperplane and therefore descends as well. Equality of quotient values is exactly membership of the state difference in the chosen subspace.

For two jointly faithful noninjective codes, their kernel subspaces meet only at zero. The dimension formula for a sum and intersection, together with quotient cardinality, gives the displayed storage product bound.

Complementary prefix and suffix codes are dynamically closed and jointly injective. Each keeps the control bit, and their finite range sizes multiply to the lower bound.

References

• Truth anchor: D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.DynamicallyClosed
• Truth anchor: D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.controlRewrite
• Truth anchor: D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.prefixCode
• Truth anchor: D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.sharedControlActions
• Truth anchor: D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.shared_control_bit_storage_bound
• Truth anchor: D5/S3/ObserverMemory/Algorithms/SharedControlBitStorageBound.suffixCode