Exact generalized-Dyck residual dynamics

Exact statement

Every left residual of a generalized Dyck language is exactly $K_s$ for one live stack $s$ , or $K_\bot$ ; all are reachable and pairwise distinct. Distinct live stacks satisfy $\operatorname{sep}(K_s,K_t)=\min(|s|,|t|)$ , while $\operatorname{sep}(K_s,K_\bot)=|s|$ . The induced ultrametric makes openers half-contractions, neutrals isometries, and closers at most $2$ -Lipschitz.

StatusProved and internally audited

External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

The unmatched stack is not merely an implementation state: canonical completions show that it is the complete Myhill–Nerode coordinate of the prefix.

Definitions

$\operatorname{sep}(K,H)$ is the least length of a word on which the two future languages disagree.
The residual metric is $d(K,H)=2^{-\operatorname{sep}(K,H)}$ , with the usual convention for equal languages.

Hypotheses and scope

Residuals and stack actions use the model in FPRD-D18.
The faithful transition-monoid statement uses the proof record's execution-order convention.

Proof or evidence

Reading a prefix from the empty stack yields a live stack or failure, so every residual has the stated form. A stack's canonical completion accepts from that stack and separates it from every competing state at the sharp minimum length. The metric bounds then follow by tracking how each symbol changes shortest distinguishing length.

Exact residual theorem →

Verification notes

The M21 closure audit reports 30,128 independent checks, eight mutation separators, clean mathematical and implementation reviews, and a passing 684-test repository gate. The proof of the infinite theorem remains the written argument, not the finite checks.

Limitations

The faithful polycyclic-monoid statement is for at least two bracket types; the rank-one case is bicyclic and generates no zero.
The compact one-point topology describes finite stacks plus failure; it does not add phantom infinite stacks.

Open work

Compare the transition monoid and ultrametric formulation with standard polycyclic-monoid treatments.

Notes

The classical stack roles and polycyclic monoid are source-calibrated. M21's obligation is their exact residual, readout, topology, and M6 bridge inside the FPRD architecture.