FPRD-T175: The stack-clock dichotomy for letter projections
Contents
1. Clock diameter
Let a hidden alphabet be partitioned into calls, returns, and locals, and let
be a letter projection. For a hidden word , define its stack height by
with calls increasing height by one, returns decreasing it by one when it is positive, and locals leaving it unchanged.
For an observed word w, define the stack-clock diameter
This measures how far two compatible hidden histories can disagree about stack depth after the same observation.
2. FPRD-T175: exact dichotomy
Exactly one of the following holds.
Degenerate finite-state tier
There is no call symbol in the hidden alphabet. Then
for every observed word. The stack is never populated, so any visibly pushdown machine over this alphabet reduces to finite-state control with bottom-return transitions.
Synchronized tier
Calls exist, and every visible-letter fiber lies entirely within one of the call, return, or local classes. Then all compatible lifts of every observed word have the same action sequence, so
for every w. This is exactly the action-preserving tier of FPRD-T174.
Unbounded-desynchronization tier
Calls exist, and some visible letter has hidden preimages of two different action types. Then for every , there is an observed word w of length at most such that
Thus a nonzero uniform bound on projection-level stack-clock disagreement is impossible. The clock diameter is either identically zero or unbounded.
3. Proof
Only the third case needs proof. Let x have an action-ambiguous fiber.
If the fiber of x contains a call and either a local or a return, use
One lift chooses a call at every position and reaches height n. The other chooses the noncall action at every position and remains at height zero.
The remaining possibility is that the fiber of x contains both a local and a return but no call. Because calls exist somewhere, choose a visible letter y with a call preimage and use
Choose the call preimage of y in both lifts. Both reach height n after the prefix. On the x suffix, one lift chooses locals and remains at height n, while the other chooses returns and falls to zero. Hence the final diameter is at least n.
4. Consequences for causal selection
FPRD-T174 is not the first point in a hierarchy of projection-level bounds
on stack-clock skew. For ordinary letter projections, all finite bounds collapse to exact synchronization.
Therefore any genuine intermediate positive tier between T174 and the hard forgotten-action setting must use more structure than the projection alone. Candidates include:
- restrictions on which hidden histories the source language permits;
- restrictions on selector outputs;
- bounded phase changes or other structured forms of desynchronization;
- a different presentation that restores a common clock.
This also sharpens the interpretation of forgotten-action projection. Its power does not arise from a small amount of timing uncertainty. As soon as a call is available and one observed letter mixes action types, the projection admits linearly diverging stack histories.
5. Relation to established theory
The call, return, and local partition and the role of synchronized stack depth come from visibly pushdown and nested-word theory. The dichotomy itself is an elementary consequence of applying a memoryless letter projection to those three action types. No literature-priority claim is made without specialist review.
Source for the underlying model:
- Rajeev Alur and P. Madhusudan, Adding Nesting Structure to Words, Journal of the ACM 56(3), 2009: https://www.cis.upenn.edu/~alur/Jacm09.pdf
6. Evidence and limits
The checker exhausts every nonempty action-fiber pattern on observed alphabets of size one, two, and three. For each pattern it verifies the zero diameter cases and the explicit linear witness through eight requested units of separation.
Limits:
- The theorem concerns unrestricted compatible lifts of a letter projection. A source language can forbid the histories used by the witness.
- It measures stack height, not stack-symbol disagreement at equal depth.
- Context-dependent transductions can have bounded nonzero lag and are outside this letter-projection dichotomy.
- The result does not itself decide causal selection in the unbounded tier.