FPRD LabShare an approach

← Claims

Theorem

FPRD-T38

Exact Hankel ranks for generalized Dyck languages

Exact statement

For generalized Dyck language Dk,ℓD_{k,\ell}, the bounded residual window through horizon NN has field rank and Boolean factor rank Sk(N)=∑h=0NkhS_k(N)=\sum_{h=0}^N k^h. Its exact length-N midpoint window has both ranks equal to Ak,ℓ(N)A_{k,\ell}(N), the number of typed stacks reachable at that exact length, with all heights available when a neutral symbol exists and only parity-compatible heights otherwise.

StatusProved, mechanically corroborated, and internally audited
External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

Typed stacks provide both a lower-bound witness and a matching factorization. A stack's canonical closing word accepts from that stack and rejects from every other selected stack.

Definitions

  • Sk(N)=∑h=0NkhS_k(N)=\sum_{h=0}^N k^h counts all typed stacks through height NN.
  • Ak,ℓ(N)=∑h=0NkhA_{k,\ell}(N)=\sum_{h=0}^N k^h when ℓ≥1\ell\ge1, while Ak,0(N)=∑j=0⌊N/2⌋kN−2jA_{k,0}(N)=\sum_{j=0}^{\lfloor N/2\rfloor}k^{N-2j} without neutral symbols.
  • The canonical closer for s=i1⋯ihs=i_1\cdots i_h is s‾=cih⋯ci1\overline{s}=c_{i_h}\cdots c_{i_1}.

Hypotheses and scope

  • There are k≥1k\ge1 matched bracket types and ℓ≥0\ell\ge0 neutral symbols.
  • Ranks are computed over an arbitrary field and over the Boolean semiring separately.
  • The exact midpoint window uses prefixes and continuations of length exactly N.

Proof or evidence

Index live residual rows and canonical closer columns by the same stack set. Their submatrix is the identity, proving the field-rank lower bound and a Boolean fooling-set lower bound. Factoring every row through its saved-stack coordinate gives the matching upper bound over both algebraic settings. At the exact midpoint, neutral padding or parity-preserving opener-closer padding realizes precisely the stated stack set and the same argument applies.

Bounded and exact midpoint rank proofs →

Verification notes

The written proof, saved-stack factorization, earlier finite-field oracles, and the independent result review agree. The new checker covers 41,516 bounded-future cells, 20 exact field-rank computations, 4,370 identity-minor cells, and 1,274 exact-midpoint prefixes. The audit separately tracks the zero failure row: it changes deterministic row/state counts but not either rank.

Limitations

  • The theorem computes finite windows; it is not a finite-automaton claim for the full Dyck language.
  • A reachable all-zero row contributes no rank dimension.
  • The classical deterministic Dyck space lower bound is source-attributed rather than claimed as new.

Open work

Add small literal matrices illustrating the identity minor and the zero-row correction to deterministic width.

Notes

The exact identity is shadow growth minus the zero tail row. The written proof, literal matrices, saved-stack factorization, independent finite-field oracles, M21/M22 bridge corpus, and 21,862-check raw challenge agree. The classical deterministic Dyck lower bound remains source-attributed rather than being claimed as new.