FPRD work cycle: the exact adaptive track-allocation law

Date: 2026-07-29
Status: FPRD transfer and minimum service-time image obstruction proved; primary theorem boundary identified; finite compilation checks and independent hostile audit passed.

Contents

Executive result

The earlier example in which an offline width-two event family forces three tracks online is the first nontrivial case of an exact quadratic law.

In the irrevocable announced-event version of the causal-track doctrine, let ww be the maximum number of pairwise incompatible service events on any completed instance. Even when the event order is two-dimensional and its geometric representation is revealed, the exact worst-case number of persistent tracks needed online is

ATR⁡(w)=(w+12). \boxed{\operatorname{ATR}(w)=\binom{w+1}{2}.}

Offline, ww tracks are necessary and sufficient by Dilworth. Online commitment therefore has an exact worst-case overhead

ATR⁡(w)w=w+12. \frac{\operatorname{ATR}(w)}{w}=\frac{w+1}{2}.

This is not a new order-theoretic theorem. The upper bound is Felsner’s exact up-growing chain-partition theorem; the represented two-dimensional lower bound is Theorem 6.2 of Bosek, Felsner, Kloch, Krawczyk, Matecki, and Micek. The FPRD content is the exact compilation of their product order into hold-or-recede causal events, together with the identification of the timing seam that prevents the present proof from implying an overbroad real-time claim.

1. The pinned announced-event doctrine

Planning reveals an abstract event together with its location in an online two-realizer. Each new event is maximal in the order already announced and must be assigned irrevocably to one persistent track. After the finite announcement sequence, choose stable rational coordinates (x,y)(x,y), clear their common denominator, and compile the event to a physical pair e=(t,p)e=(t,p), where tt is a service time and pp is an old-input address. A persistent track follows a path whose address holds or recedes by one per unit of physical time. Event ee can be followed by f=(u,q)f=(u,q) on one track exactly when

e⪯f⟺t≤u,q≤p,p−q≤u−t. e\preceq f \quad\Longleftrightarrow\quad t\le u,\qquad q\le p,\qquad p-q\le u-t.

This planning/execution separation is load-bearing. It is the ordinary online chain-partition game instantiated by causal track geometry. It is not yet a theorem about a machine in which the event is first disclosed at its physical service time, nor about a controller allowed to withdraw and reassign old reservations.

Let ATR⁡(w)\operatorname{ATR}(w) be the least number of tracks with which one online allocator can serve every finite announced event system of width at most ww whose event order is two-dimensional and whose representation is provided online.

2. Geometry is exactly a two-dimensional product order

For product coordinates (x,y)(x,y), choose constants K,CK,C and define

t=K+x+y,p=C−y. \boxed{ t=K+x+y,\qquad p=C-y. }

For e=e(x,y)e=e(x,y) and f=e(x′,y′)f=e(x',y'),

q≤p⟺y≤y′,p−q≤u−t⟺y′−y≤(x′−x)+(y′−y)⟺x≤x′. \begin{aligned} q\le p &\Longleftrightarrow y\le y',\\ p-q\le u-t &\Longleftrightarrow y'-y\le(x'-x)+(y'-y)\\ &\Longleftrightarrow x\le x'. \end{aligned}

Thus

e(x,y)⪯e(x′,y′)⟺x≤x′ and y≤y′. \boxed{ e(x,y)\preceq e(x',y') \Longleftrightarrow x\le x'\ \text{and}\ y\le y'. }

The map is bidirectionally exact: no comparability is lost and no false track route is introduced. When the coordinates are rational, a common positive scaling makes both times and addresses integral. A large CC makes every address nonnegative; a large KK makes every first event reachable from one common initial track address.

An online two-realizer can be assigned stable rational order labels without foreknowledge: whenever an element is inserted between two neighbors in one of the realizer orders, use a rational midpoint. The finite adversarial play therefore has a finite common denominator. The labels determine the reservations online; only after the finite play are they scaled into integral physical times and addresses. They disclose no future adversary move, but this is a reservation compiler rather than a real-time local encoder.

This construction grants whatever finite precision the play needs. It does not prove a bounded-precision version for free.

3. Exact quadratic theorem

Theorem

For every w≥1w\ge1,

ATR⁡(w)=(w+12). \boxed{ \operatorname{ATR}(w)=\binom{w+1}{2}. }

Proof

Upper bound. Every causal event order is a poset. Because each newly announced event is maximal, its presentation is up-growing. Felsner proved that every up-growing poset of width at most ww can be partitioned online into at most

(w+12) \binom{w+1}{2}

chains. Assign one persistent track to each chain. The definition of ⪯\preceq gives a legal hold/recede schedule between every two consecutive events on that track. Hence

ATR⁡(w)≤(w+12). \operatorname{ATR}(w)\le\binom{w+1}{2}.

Lower bound. Bosek et al. proved that an adversary can force every online chain-partition algorithm to use at least

(w+12) \binom{w+1}{2}

chains while keeping the poset up-growing, of width ww, and two-dimensional, even when a two-realizer is supplied online. Apply the coordinate compilation of Section 2 to that realizer. Product comparability is exactly causal-track reachability, so every chain color is exactly one physically feasible persistent track and every forbidden color reuse is exactly a pair of events that one track cannot serve. A geometry-aware allocator induces a representation-aware chain-partition algorithm, so the lower adversary applies. Therefore

ATR⁡(w)≥(w+12). \operatorname{ATR}(w)\ge\binom{w+1}{2}.

The bounds agree. □\square

Boundary checks

  • w=1w=1 gives one track.
  • w=2w=2 gives three tracks, exactly the earlier A,B,C,D/D′A,B,C,D/D' adversary.
  • Offline track demand remains ww, since minimum chain cover equals width.
  • The result survives complete disclosure of the two-dimensional realizer. It is not caused by hiding the geometry.

4. The timing obstruction

It is tempting to identify announcement round with physical service time. That stronger statement does not follow from this product-order proof.

If one insists on keeping a particular supplied realizer, its coordinates must admit monotone rescalings ai,bja_i,b_j for which ai+bja_i+b_j increases in the presentation order. Not every supplied realizer has this property.

A six-element counterexample has second-realizer ranks

(2,5,4,1,0,3) (2,5,4,1,0,3)

relative to first-realizer order 0<1<⋯<50<1<\cdots<5, and presentation order

3,0,1,4,5,2. 3,0,1,4,5,2.

Write Ai=ai+1−ai>0A_i=a_{i+1}-a_i>0 and Bi=bi+1−bi>0B_i=b_{i+1}-b_i>0. Three of the required presentation inequalities give

A0+A1+A2−B1<0,B0+B1+B2+B3+B4−A1−A2−A3<0,A2+A3+A4−B3<0. \begin{aligned} A_0+A_1+A_2-B_1&<0,\\ B_0+B_1+B_2+B_3+B_4-A_1-A_2-A_3&<0,\\ A_2+A_3+A_4-B_3&<0. \end{aligned}

Adding them gives

A0+A2+A4+B0+B2+B4<0, A_0+A_2+A_4+B_0+B_2+B_4<0,

contradicting positivity.

The certificate blocks one tempting proof route: monotonically respacing an arbitrary supplied realizer. It is not an intrinsic obstruction for the poset or presentation. The independent audit found another realizer of this same six-element poset whose coordinate sums increase in presentation order.

A separate exact enumeration found the first intrinsic obstruction at seven events. In announcement order 0,…,60,\ldots,6, take the order with relations

0<1,5,6,1<5,2<3,5,6,4<5. 0<1,5,6,\qquad 1<5,\qquad 2<3,5,6,\qquad 4<5.

Its unordered two-realizer is unique:

Lx=(2,3,0,6,1,4,5),Ly=(4,0,1,2,5,6,3). L_x=(2,3,0,6,1,4,5),\qquad L_y=(4,0,1,2,5,6,3).

For positive consecutive gaps A0,…,A5,B0,…,B5A_0,\ldots,A_5,B_0,\ldots,B_5, the three arrival constraints 1→21\to2, 3→43\to4, and 5→65\to6 sum to

−A0−A3−A5−B0−B1−B3−B5≥0, -A_0-A_3-A_5-B_0-B_1-B_3-B_5\ge0,

which is impossible. Exact enumeration confirms that all 4,794 represented presentations through six events are diagonal and that exactly two dual presentations among 91,206 fail at seven. A small common perturbation by arrival rank removes coordinate ties, so the positive-gap census also covers weak physical embeddings.

So the exact quadratic theorem remains an announced/reserved-event theorem, and the announced class is strictly larger than the real-time diagonal class. A quadratic real-time lower bound still requires either:

  1. a fresh lower construction whose realizer is diagonally presented;
  2. an explicit amount of lookahead between announcement and service; or
  3. a different causal allocation invariant.

The first item may still hold for the published lower-bound adversary; the seven-event image obstruction proves a class separation but does not settle that adversary’s track demand.

5. Comparator and novelty boundary

Primary sources

  1. Stefan Felsner, On-line chain partitions of orders, Theoretical Computer Science 175(2), 283–292 (1997), https://doi.org/10.1016/S0304-3975(96)00204-6. The exact value for up-growing width-ww posets is (w+12)\binom{w+1}{2}.
  2. Bartłomiej Bosek, Stefan Felsner, Kamil Kloch, Tomasz Krawczyk, Grzegorz Matecki, and Piotr Micek, On-Line Chain Partitions of Orders: A Survey, Order 29, 49–73 (2012), https://doi.org/10.1007/s11083-011-9197-1. Theorem 6.2 proves the same lower bound for up-growing two-dimensional orders presented with a realizer. The theorem is original content inside that survey.

Classification

Item Status
Offline width = track count classical Dilworth specialization
Up-growing online value (w+12)\binom{w+1}{2} classical theorem used
Two-dimensional represented lower bound classical theorem used
(x,y)↦(K+x+y,C−y)(x,y)\mapsto(K+x+y,C-y) causal compilation direct specialization
Identification of the announcement/service-time obstruction proved here
Any claim of external novelty not made

The result is still mathematically useful for FPRD: it replaces one isolated width-two adversary by a complete all-ww law and exposes a real named boundary. The adaptive chain-partition variant, in which colors may later be withdrawn and reassigned, remains much less understood in the primary literature; it is the correct comparator if a future causal doctrine permits reservation revision.

6. Formalization and hostile controls

check_causal_poset_transfer.py verifies:

  • 625 product-order/causal-order equivalences;
  • 225 explicit hold/recede track segments;
  • Dilworth equality on all 512 subsets of a 3×33\times3 product grid;
  • the earlier width-two/three-track adversary; and
  • the exact six-element fixed-realizer respacing certificate; and
  • an alternate realizer that repairs diagonal timing for the same poset.

diagonal_embedding_search.py additionally verifies the exact seven-event minimum obstruction, its dual, all 4,794 smaller represented presentations, and both integer Farkas certificates.

The checker passes.

7. What remains unproved

  1. No total language yet. The theorem is an exact finite demand-tree allocation law. It has not yet been compiled into one fixed-alphabet target generated by a stationary bounded-role local encoder.
  2. No quadratic service-time revelation theorem. The seven-event theorem proves that not every announced represented order has a real-time diagonal image. It does not prove that the exact (w+12)\binom{w+1}{2} lower-bound adversary survives inside the realizable subclass.
  3. Precision is charged later. Stable online coordinate insertion can require growing denominator or integer spacing. The track theorem grants that resource and does not hide it inside a bounded-precision claim.
  4. No reassignment. Revocable reservations belong to the adaptive chain-partition game, not this theorem.
  5. No new lower bound for ordinary multihead automata yet. Such a consequence requires a compilation from announcements to one stationary word-input machine.

8. Exact next attack

The next attack should be the causal local-encoder compilation problem: construct a fixed-alphabet append-only input that emits the represented up-growing adversary with bounded roles, while giving each event a controlled announcement-to-service slack. There are three possible outcomes:

  • a compilation transfers the exact quadratic law to one stationary FPRD target;
  • bounded precision or local encoding forces a smaller realizable image, yielding an intrinsic compatibility theorem; or
  • the diagonal timing obstruction survives every bounded-slack encoding, giving a clean reason that the quadratic reservation law cannot become a real-time track theorem.

This is a stronger and more sharply delimited adaptive-access problem than another one-stage late-INDEX construction.