For every data dimension d at least two, keep any fixed complementary pair A,B of positive dimensions in Source(d)=(Fin(d) to ZMod 2) times ZMod 2. Local(A,B) is the disjoint sum of A and the pairs (a,q) for which some b in B satisfies q=ellA(a)+ellB(b). The symmetric local carrier uses B,A. The readout is a or b and initialization uses the unknown copy.
In the formulas pA,pB are the fixed projections, ell(S)=controlRestriction(S), NatCard is Nat.card, ActionApply is Action.apply, and Type with subscript 0 is Type. IsTranslation means a data or control basis translation; get(t,j) is the optional list entry and getD supplies false when absent. mapQuestion maps an internal question through liftQuestion and leaves a leaf unchanged; liftQuestion composes the tagged question with that endpoint localRead. Every submodule value is coerced to Source when used in a sum. The witness has exactly the ControllerData named data(h). Its roots are the local unknown/known modes. Translation is a leaf which adds the public projected basis increment and, in known mode, the public control increment. An unknown rewrite lifts the existing fixed right-then-left exchange to sender-local persistent readouts. A known rewrite is a leaf using only the endpoint’s stored current control. All rewrites store known control zero, including a zero-bit rewrite.
The compliance fields are proved for this actual evaluator-driven implementation: local initialization retractions, agreed local roots, finite termination on reachable pairs, both prescribed local readouts, zero-bit basis translations, and surjectivity onto both local carriers. No joint source readout, remote old state or old word is an endpoint runtime input.
E(h,k,z), written encode below, pairs the two unknown projected states when k is false and the two compatible known states with stored z.c when k is true. Reach is generated by initialization and successful execute-based commits. The equivalence proves both image inclusions. Every known source is reached from initialized zero by one original rewrite and a word containing only original basis translations.
Exec and commit below belong to data(h). nextMode(k,f) is true for every rewrite and otherwise k. protocolCharge(h,k,f) is Ci for an unknown rewrite and zero otherwise. initSource(C,z) initializes from the two original projections of z. runSource uses Action.apply; run uses the actual C.step. Comm uses C.cost, the actual successful transcript’s length. firstRewriteCost is zero if no rewrite occurs and otherwise the Ci of the first rewrite label. One Cstar bound covers all initial pairs and all finite action words.
The live proof lifts successful evaluator paths, uses their proved uniqueness, establishes operational closure, and constructs known reachability using a subgroup containing the full original basis. Word induction then follows the persistent mode rather than paid events. The operational image yields a finite joint equivalence with Bool times Source(d). Local known states are equivalent to the local summand times the opposite control range; each readout fiber is one initial point plus that range. These equivalences give the exact fiber, local and joint capacities.
The same witness attains Cstar as a cumulative budget. The existing fixed-split directional bound excludes every smaller budget for all compliant competitors, giving the displayed least-budget statement over Type-valued carriers. Its necessity supplier also quantifies arbitrary universes.
StorageOptimal(C) strengthens this same witness with simultaneous universal minima. Every compliant competitor Cprime with any uniform cumulative budget K admits the five finite embeddings displayed below, including competitors whose local or joint carriers are infinite. All universe levels u,v,w are arbitrary. Here nA,nB and nQ are the actual finite cardinalities of C’s left, right and joint carriers; fiberA(x) and fiberB(y) are its exact fibers. No finiteness premise is imposed on a competitor for these embeddings.
BinaryEncoding(M,k) means an injective function from the entire persistent carrier M to Fin(k) to Bool. The two endpoint minima are Nat.clog(2,nA), Nat.clog(2,nB); their attained encodings are independent. The separately attained joint minimum is d+2=D+1. Every finite encoding of a competing endpoint has at least its corresponding minimum width, and every finite centralized encoding of the competing operational joint carrier has at least D+1 bits. These lower bounds need no finite competitor premise because an injection into finite bit strings already excludes an infinite carrier.
For finite competing local carriers only, the sum of their real binary logarithms and the sum of their ceiling logarithms are at least those of the same constructed witness. Thus the finite logarithmic minimum is attained while infinite carriers remain subject to the universal capacity and encoding bounds. On the finite constructed carriers, ceiling(log2(Nat.card)) equals Nat.clog(2,Nat.card). Let r=finrank(A), s=finrank(B), D=d+1; r+s=D. The two control restrictions cannot both vanish, so the three rows exhaust the fixed splits. Each row below gives left/right fiber sizes, local capacities, logarithmic sum, separate endpoint widths, their total, and the sharp uniform budget, in order.
The row values are attained by this same operational controller. The universal embeddings and resource comparisons make each value a lower bound for every compliant uniformly cumulatively bounded competitor. Centralized coding does not provide separately accessible endpoint memory. The roots remain the two Bool modes: known control zero and known control one can select the same leaf root. The three fiber states count persistent states rather than distinct roots.