Independent recurrence obstructs a prefix quotient

Exact statement

Let $\alpha=\beta\amalg\gamma$ . In the full asynchronous-product location automaton, if the two components have recurrent locations with self-loops on distinct letters $a\ne b$ , then $A_{\mathrm{Pre}}(\alpha)$ is not an existential state quotient of $A_{\mathrm{POS}}(\alpha)$ . For a construction that trims unreachable locations, the paired product location must be reachable.

StatusSelf-contained proof; exact small-case verification

External reviewNo documented external or specialist review of these FPRD results is recorded.

Context

Shuffle advances one component while holding the other fixed, so independent recurrences accumulate at a single product frontier.

Hypotheses and scope

The component loop labels are distinct.
The location automaton uses the asynchronous shuffle product of the cited construction.
If unreachable product locations are trimmed, the paired mixed-loop location is reachable.

Proof or evidence

The product location carries both component loops. FPRD-SH-T01 forces both labels onto its quotient image, while FPRD-SH-L01 forbids such a prefix state.

Independent-recurrence theorem and proof →

Verification notes

The proof was checked symbolically and on every matching generated example in the bounded starred-word census.

Limitations

The condition is sufficient, not necessary; FPRD-SH-T04 now catches the published 2023 example without requiring recurrence.
No external novelty or priority claim is made.

Open work

Treat this loop theorem as a special case of the exact incoming-spectrum classification FPRD-SH-T05.