FPRD-D18 For a generalized Dyck alphabet with k bracket types and any number of neutral symbols, the exact residual carrier consists of finite typed stacks together with an absorbing failure state. A live stack s has future language K_s of words that empty it without failure; failure has the empty future language. Definition Precisely stated and self-contained Evidence and limits → Automata and formal languages Generalized-Dyck residual dynamics Model and exact residuals No recorded dependencies FPRD Dyck-residual and finite-observation proof records Reviewed 2026-08-25 No documented external or specialist review of this FPRD result is recorded. Add a small worked residual calculation for two bracket types and one neutral symbol. FPRD-T34 Every left residual of a generalized Dyck language is exactly K s K_s K s s s s K ⊥ K_\bot K ⊥ sep ( K s , K t ) = min ( ∣ s ∣ , ∣ t ∣ ) \operatorname{sep}(K_s,K_t)=\min(|s|,|t|) sep ( K s , K t ) = min ( ∣ s ∣ , ∣ t ∣ ) sep ( K s , K ⊥ ) = ∣ s ∣ \operatorname{sep}(K_s,K_\bot)=|s| sep ( K s , K ⊥ ) = ∣ s ∣ 2 2 2 Theorem Proved and internally audited Evidence and limits → Automata and formal languages Generalized-Dyck residual dynamics Exact residual theorem FPRD-D18 FPRD Dyck-residual and finite-observation proof records Reviewed 2026-08-25 No documented external or specialist review of this FPRD result is recorded. Compare the transition monoid and ultrametric formulation with standard polycyclic-monoid treatments. FPRD-T35 The depth-N N N N N N 1 + ∑ h = 0 N k h 1+\sum_{h=0}^{N}k^h 1 + ∑ h = 0 N k h r r r N + r N+r N + r N N N Theorem Proved and internally audited Evidence and limits → Automata and formal languages Generalized-Dyck residual dynamics Finite shadows and reconstruction FPRD-D18; FPRD-T34 FPRD Dyck-residual and finite-observation proof records Reviewed 2026-08-25 No documented external or specialist review of this FPRD result is recorded. Publish a diagram of the bonding maps and one explicit failure of same-level closer action. FPRD-T49 For L f = { a n b a f ( n ) : n ≥ 0 } L_f=\{a^n b a^{f(n)}:n\ge0\} L f = { a n b a f ( n ) : n ≥ 0 } f : N → N f:\mathbb N\to\mathbb N f : N → N Theorem Proved and internally audited Evidence and limits → Automata and formal languages Formal languages and automata Sparse-marker access FPRD-T48; FPRD-T47 FPRD proofs on residual access and controlled-Dyck presentations Reviewed 2026-08-26 No documented external or specialist review of this FPRD result is recorded. Classify which finite-presentation families constrain the jump term that controls access. FPRD-T50 For a finite controller (M) intersected with a generalized-Dyck language, shortest balanced-controller distances determine exact raw-coordinate arrivals. Minimizing those arrivals inside each bounded semantic row and then maximizing computes (a_{L_M}(N)). If (B_M) is the largest finite balanced distance from an underlying-DFA-reachable source, then a L M ( N ) ≤ max { 1 , ( N + 1 ) B M + N } a_{L_M}(N)\le\max\{1,(N+1)B_M+N\} a L M ( N ) ≤ max { 1 , ( N + 1 ) B M + N } Theorem and algorithm Proved and internally audited Evidence and limits → Automata and formal languages Formal languages and automata Controlled-Dyck access calculus FPRD-D24; FPRD-T40; FPRD-T44; FPRD-T49 FPRD proofs on residual access and controlled-Dyck presentations Reviewed 2026-08-26 No documented external or specialist review of this FPRD result is recorded. Compare the presentation certificate with established visibly-pushdown and weighted shortest-witness formulations. FPRD-T51 For generalized-Dyck words whose stack height reaches at least r ≥ 1 r\ge1 r ≥ 1 q k , r ≥ ( N ) = 1 + ∑ h = 0 N k h + ∑ h = max ( 0 , 2 r − N ) r − 1 k h q_{k,r}^{\ge}(N)=1+\sum_{h=0}^{N}k^h+\sum_{h=\max(0,2r-N)}^{r-1}k^h q k , r ≥ ( N ) = 1 + ∑ h = 0 N k h + ∑ h = m a x ( 0 , 2 r − N ) r − 1 k h a k , r ≥ ( N ) = max ( 2 r , N ) a_{k,r}^{\ge}(N)=\max(2r,N) a k , r ≥ ( N ) = max ( 2 r , N ) q k , r < ( N ) = 1 + ∑ h = 0 min ( N , r − 1 ) k h q_{k,r}^{<}(N)=1+\sum_{h=0}^{\min(N,r-1)}k^h q k , r < ( N ) = 1 + ∑ h = 0 m i n ( N , r − 1 ) k h a k , r < ( N ) = max ( 1 , min ( N , r − 1 ) ) a_{k,r}^{<}(N)=\max(1,\min(N,r-1)) a k , r < ( N ) = max ( 1 , min ( N , r − 1 )) Theorem Proved and internally audited Evidence and limits → Automata and formal languages Formal languages and automata Depth-threshold profiles FPRD-D24; FPRD-T40; FPRD-T50 FPRD proofs on residual access and controlled-Dyck presentations Reviewed 2026-08-26 No documented external or specialist review of this FPRD result is recorded. Use the threshold families as calibrations when comparing access certificates across equivalent controllers. FPRD-T52 Only controller states that actually begin balanced segments of legal prefixes are needed in the replacement proof. Their entry balanced diameter cannot increase under a surjective reachable DFA morphism. Minimizing this diameter over regular controllers with the same trace on a fixed Dyck language defines β D ( L ) \beta_D(L) β D ( L ) a L ( N ) ≤ max { 1 , ( N + 1 ) β D ( L ) + N } a_L(N)\le\max\{1,(N+1)\beta_D(L)+N\} a L ( N ) ≤ max { 1 , ( N + 1 ) β D ( L ) + N } Theorem Proved and internally audited Evidence and limits → Automata and formal languages Formal languages and automata Dyck-trace minimax FPRD-D25; FPRD-T40; FPRD-T50 FPRD proofs on residual access and controlled-Dyck presentations Reviewed 2026-08-26 No documented external or specialist review of this FPRD result is recorded. Investigate computable subclasses of the trace-class minimization problem and dependence on the chosen Dyck envelope. FPRD-T53 For a controlled-Dyck language, entry-context residual access η D \eta_D η D γ D \gamma_D γ D τ D \tau_D τ D β D ≥ η D ≥ γ D ≥ τ D \beta_D\ge\eta_D\ge\gamma_D\ge\tau_D β D ≥ η D ≥ γ D ≥ τ D η D \eta_D η D σ D = β D − η D \sigma_D=\beta_D-\eta_D σ D = β D − η D Theorem and exact finite procedure Proved and internally audited Evidence and limits → Automata and formal languages Formal languages and automata Semantic access hierarchy FPRD-D25; FPRD-T51; FPRD-T52 FPRD proofs on residual access and controlled-Dyck presentations Reviewed 2026-08-26 No documented external or specialist review of this FPRD result is recorded. Find either a positive sewing-defect example or a proof that every controlled-Dyck trace has zero defect. FPRD-T54 Let (K_3) contain epsilon and the nonempty one-bracket Dyck words whose terminal run of closing brackets has length 2 m o d 3 2\bmod 3 2 mod 3 η D ( K 3 ) = β D ( K 3 ) = 4 \eta_D(K_3)=\beta_D(K_3)=4 η D ( K 3 ) = β D ( K 3 ) = 4 Theorem and exact example Proved; finite-state lower bound is computer-assisted and internally audited Evidence and limits → Automata and formal languages Formal languages and automata Terminal-descent tradeoff FPRD-D26; FPRD-T53 FPRD proofs on residual access and controlled-Dyck presentations Reviewed 2026-08-26 No documented external or specialist review of this FPRD result is recorded. Determine whether any controlled-Dyck trace has positive sewing defect. FPRD-T55 The minimum controller size for K 3 K_3 K 3 ( 3 , 6 ) (3,6) ( 3 , 6 ) ( 6 , 4 ) (6,4) ( 6 , 4 ) Theorem and exact finite-state classification Proved; the five-state exclusion is computer-assisted and internally audited Evidence and limits → Automata and formal languages Formal languages and automata Modulus-three frontier FPRD-D26; FPRD-T54 FPRD proofs on residual access and controlled-Dyck presentations Reviewed 2026-08-26 No documented external or specialist review of this FPRD result is recorded. Produce a portable unsatisfiability certificate if the finite-state encoding is revisited. FPRD-T56 The modulus-two trace K 2 K_2 K 2 η D ( K 2 ) = β D ( K 2 ) = 4 \eta_D(K_2)=\beta_D(K_2)=4 η D ( K 2 ) = β D ( K 2 ) = 4 ( 2 , 4 ) (2,4) ( 2 , 4 ) Theorem and exact finite-state classification Proved and internally audited Evidence and limits → Automata and formal languages Formal languages and automata Modulus-two frontier FPRD-D27; FPRD-T53 FPRD proofs on residual access and controlled-Dyck presentations Reviewed 2026-08-26 No documented external or specialist review of this FPRD result is recorded. Use the exceptional top-level residual at modulus two as a boundary test for broader terminal-descent constructions. FPRD-T57 The modulus-four trace K 4 K_4 K 4 η D ( K 4 ) = β D ( K 4 ) = 6 \eta_D(K_4)=\beta_D(K_4)=6 η D ( K 4 ) = β D ( K 4 ) = 6 ( 4 , 8 ) (4,8) ( 4 , 8 ) ( 6 , 6 ) (6,6) ( 6 , 6 ) Theorem and exact finite-state classification Proved; the five-state exclusion is computer-assisted and internally audited Evidence and limits → Automata and formal languages Formal languages and automata Modulus-four frontier FPRD-D27; FPRD-T55 FPRD proofs on residual access and controlled-Dyck presentations Reviewed 2026-08-26 No documented external or specialist review of this FPRD result is recorded. Seek a checkable certificate for the five-state exclusion and avoid extrapolating an unproved minimum-state law. FPRD-T58 For terminal-descent traces, η D ( K 2 ) = β D ( K 2 ) = 4 \eta_D(K_2)=\beta_D(K_2)=4 η D ( K 2 ) = β D ( K 2 ) = 4 m ≥ 3 m\ge3 m ≥ 3 η D ( K m ) = β D ( K m ) = 2 ( m − 1 ) \eta_D(K_m)=\beta_D(K_m)=2(m-1) η D ( K m ) = β D ( K m ) = 2 ( m − 1 ) 2 m 2m 2 m Theorem and uniform construction Proved and internally audited Evidence and limits → Automata and formal languages Formal languages and automata All-modulus theorem FPRD-D27; FPRD-T53 FPRD proofs on residual access and controlled-Dyck presentations Reviewed 2026-08-26 No documented external or specialist review of this FPRD result is recorded. Determine the minimum number of states needed to attain optimal access beyond moduli two, three, and four. FPRD-T59 For every even modulus m m m ( m + 2 ) (m+2) ( m + 2 ) K m K_m K m β D ( K m ) \beta_D(K_m) β D ( K m ) m = 4 m=4 m = 4 Theorem and uniform construction Proved and internally audited Evidence and limits → Automata and formal languages Formal languages and automata Even-modulus construction FPRD-D27; FPRD-T58 FPRD proofs on residual access and controlled-Dyck presentations Reviewed 2026-08-26 No documented external or specialist review of this FPRD result is recorded. Determine whether m+2 is minimal at optimal cost for any even modulus beyond four. FPRD-D33 A forgotten-action frontier machine has a finite transition list ( q , a , X , q ′ , γ ) (q,a,X,q',\gamma) ( q , a , X , q ′ , γ ) γ \gamma γ Definition and executable machine model Defined self-containedly and used by the checked recurrence Evidence and limits → Automata and formal languages Pushdown frontiers and visible projections Machine and frontier No recorded dependencies FPRD pushdown-frontier proof and formalization records Reviewed 2026-08-26 No documented external or specialist review of this FPRD exposition is recorded. Use this fixed interface when comparing stationary frontier representations; do not conflate it with a PEG or scaffold. FPRD-T91 For every finite alphabet Σ \Sigma Σ L ⊆ Σ ∗ L\subseteq\Sigma^* L ⊆ Σ ∗ L = π ( A ) L=\pi(A) L = π ( A ) A ⊆ ( Σ × { c , r , l } ) ∗ A\subseteq(\Sigma\times\{\mathsf c,\mathsf r,\mathsf l\})^* A ⊆ ( Σ × { c , r , l } ) ∗ π \pi π Source theorem and elementary converse Source-verified and reconstructed; not mechanically checked Evidence and limits → Automata and formal languages Pushdown frontiers and visible projections Visible-projection theorem Alur–Madhusudan Proposition 1 and Theorem 2; Closure of context-free languages under homomorphism FPRD pushdown-frontier proof and formalization records Reviewed 2026-08-26 The forward construction and determinization are published results of Alur and Madhusudan; the FPRD application has no documented specialist review. Add a direct theorem-level primary-source locator to the public bibliography and seek a specialist check of the normalization conventions. FPRD-T92 For a forgotten-action frontier machine, (S_{ua}(q')) is the union of γ ( X − 1 S u ( q ) ) \gamma(X^{-1}S_u(q)) γ ( X − 1 S u ( q )) ( q , a , X , q ′ , γ ) (q,a,X,q',\gamma) ( q , a , X , q ′ , γ ) Theorem with Lean verification Mechanically checked and internally audited Evidence and limits → Automata and formal languages Pushdown frontiers and visible projections Frontier recurrence and readout FPRD-D33 FPRD pushdown-frontier proof and formalization records Reviewed 2026-08-26 No documented external or specialist review of this FPRD exposition is recorded. Use the recurrence as the exact semantic target for proposed finite or persistent frontier representations. FPRD-T93 Let K 0 ⊆ K 1 ⊆ ⋯ \mathcal K_0\subseteq\mathcal K_1\subseteq\cdots K 0 ⊆ K 1 ⊆ ⋯ K k \mathcal K_k K k L ∈ P E L L\in\mathsf{PEL} L ∈ PEL sup N e L ( N ) < ∞ \sup_N e_L(N)<\infty sup N e L ( N ) < ∞ Theorem and finite pigeonhole argument Proved and internally audited Evidence and limits → Automata and formal languages Pushdown frontiers and visible projections Finite-core sewing Loff–Moreira–Reis Theorem 16 FPRD pushdown-frontier proof and formalization records Reviewed 2026-08-26 No documented external or specialist review of this FPRD exposition is recorded. Apply the criterion only to finite normalized strata; test whether projected visible frontiers escape every fixed stratum. FPRD-T94 Suppose a fixed synchronous multistack executor represents a forgotten-action frontier through a fixed derivative basis and fixed slots, with exact initialization, a preserved validity invariant, exact one-letter updates, and exact final-state readout. Then after every word its represented relation equals the pushdown frontier. The executor and its compiled scaffold therefore recognize exactly the source language, including at the empty word. Conditional compilation theorem with Lean verification Mechanically checked and internally audited Evidence and limits → Automata and formal languages Pushdown frontiers and visible projections Stationary-cover transfer FPRD-T89; FPRD-T92 FPRD pushdown-frontier proof and formalization records Reviewed 2026-08-26 No documented external or specialist review of this FPRD exposition is recorded. Construct a stationary bounded-slot cover for broader projected frontiers, or prove a representation-independent resource obstruction. FPRD-T161 Let a scaffolding automaton have tuple (d,k,g,q) with k>=1, put D=sum_(i=1)^k d^i, and m=ceil(log_2(1+gq)). It has an equivalent tuple (D+m,2,1,2). Shortcut ports expose every source endpoint in one hop, and marker ports encode each ordinary source label-control pair as local SELF/missing geometry. The zero marker code is reserved for the distinguished base node. Hence Tr(L) is nonempty exactly when it contains some tuple (D,2,1,2). Theorem · structural normal form and one-dimensional existence criterion Self-contained constructive proof with combined compiler and structural-code audits Evidence and limits → Automata and formal languages Replayable memory and cut responses Structural scaffold normal-form theorem FPRD-T160; FPRD-T157; Loff--Moreira--Reis scaffolding automata Structural normal form for scaffolding automata Reviewed 2026-09-23 A targeted literature search found the original scaffold model but no published unary-label, two-control structural normal form; no specialist review or priority claim is recorded. Study the minimum canonical structural degree delta_str(L), including composition laws and lower bounds that survive every finite label and control encoding. FPRD-T160 If a scaffolding automaton has tuple (d,k,g,q) with k>=2, then it has an equivalent tuple (sum_(i=1)^k d^i,2,g,q). The compiler gives each physical node one shortcut port for every original port word of length at most k. The compiled radius-two view reconstructs the original radius-k view, distinguishing base from missing at shortcut endpoints; at most two hops install every shortcut on the next node. Hence SA_<=2=SA. Combined with FPRD-T159, SA_<=1=REG is a strict subset of SA_<=2=SA. Theorem · complete distance normalization for scaffolding automata Self-contained constructive proof with machine, symbolic-descriptor, and strictness audits Evidence and limits → Automata and formal languages Replayable memory and cut responses Distance-two normal-form theorem FPRD-T159; Loff--Moreira--Reis scaffolding automata Distance-two normal form for scaffolding automata Reviewed 2026-09-23 A targeted literature search found the original scaffold model but no published distance-two normalization; no specialist review or priority claim is recorded. Replace distance-based expressiveness questions with degree-versus-distance succinctness bounds and seek lower bounds against the entire distance-two normal form. FPRD-T159 Every distance-one scaffolding automaton of degree d, working-alphabet size g, and q controls compiles to a DFA with at most N=q[1+(g+1)^(d+1)] states, so its residual tower stabilizes by horizon N-1. Conversely, every regular language has a distance-one scaffold presentation. Hence SA_<=1=REG. The explicit degree-two, distance-two persistent selector is nonregular, so REG=SA_<=1 is a strict subset of SA_<=2. Theorem · exact base tier and strict first step of the scaffold distance hierarchy Self-contained constructive proof with compiler and strictness audits Evidence and limits → Automata and formal languages Replayable memory and cut responses Distance-one collapse theorem FPRD-T153; FPRD-T151; Loff--Moreira--Reis scaffolding automata Distance-one scaffolds collapse to finite automata Reviewed 2026-09-23 A targeted literature search found the original scaffold model but no published statement of this distance-one characterization; no specialist review or priority claim is recorded. Use T160's complete distance normalization to study degree-versus-distance succinctness and optimal degree rather than further expressiveness levels. FPRD-T158 Let (d,k,g,q) lie in Tr(L), let U be a nonempty finite set of fixed suffixes, and let b be any Boolean function of their membership answers. With R_(k,h)=0 for h=0 or k=0 and R_(k,h)=k+(h-1)(k-1) otherwise, put D_U=max over u in U of R_(k,|u|+1). Then the observer language {p : b((1_L(pu))_(u in U))=1} has transport tuple (d,D_U,g,q 2^|U|). The compiled machine uses exactly the original persistent graph. In particular, every fixed right quotient L/u preserves nonempty stationary transport spectrum. Theorem · finite-observer closure with explicit transport bounds Self-contained proof with compiled-control, locality, and sharpness audits Evidence and limits → Automata and formal languages Replayable memory and cut responses Finite future-observer theorem FPRD-T153; FPRD-D45 Finite future observers internalize into stationary transport Reviewed 2026-09-23 The proof uses the locally established readable-cone theorem FPRD-T153; no external or specialist review of this resource-bound formulation is recorded. Define and test observer families whose suffix sets grow with the cut, since every fixed finite right-context observer is now known to compile. FPRD-D45 The stationary transport spectrum Tr(L) is the set of resource ceilings (degree, descriptor distance, working-alphabet size, control-state count) under which the canonical residual dynamics of L has a one-node-per-symbol bounded-locality persistent presentation. It minimizes over all presentations within the scaffolding model. Definition · implementation-minimized stationary transport invariant Defined exactly at the finite scaffolding-automaton boundary Evidence and limits → Automata and formal languages Replayable memory and cut responses Stationary transport spectrum FPRD-T156; Loff--Moreira--Reis scaffolding automata Stationary transport spectra Reviewed 2026-09-23 No documented external or specialist review of this FPRD result is recorded. Place positive forgotten-action tiers inside explicit spectrum cones and search for presentation-independent emptiness criteria. FPRD-T157 For every language L, Tr(L) is upward closed in the componentwise order and therefore, by Dickson's lemma, is generated by a unique finite antichain of Pareto-minimal resource tuples whenever nonempty. Complement preserves Tr exactly. If tuples (d_i,k_i,g_i,q_i) present L_i, then every binary Boolean combination has a presentation bounded by (d_1+d_2, max(k_1,k_2), g_1g_2, q_1q_2). Nonempty spectrum is equivalent to recognition by a finite scaffolding automaton and implies a PEG for the reverse language through FPRD-T110. Theorem · finite basis and Boolean calculus for transport resources Self-contained proof with finite-basis and paired-machine audits Evidence and limits → Automata and formal languages Replayable memory and cut responses Finite Pareto basis theorem FPRD-D45; Dickson's lemma; FPRD-T110 Stationary transport spectra Reviewed 2026-09-23 The finite-basis step is classical Dickson's lemma and the model is due to Loff, Moreira, and Reis; no external review of this FPRD spectrum formulation is recorded. Develop lower bounds that exclude all Pareto tuples simultaneously, or compile projected frontier representations into an explicit feasible tuple. FPRD-D44 For a language L, Q_h is the finite set of response rows of prefixes on continuations of length at most h. Restriction gives surjections Q_(h+1) to Q_h, forming an inverse system. Reading one input symbol maps Q_(h+1) to Q_h by selecting the corresponding response subtree. Definition · canonical finite-horizon quotient system Defined self-containedly and connected to residual derivatives Evidence and limits → Automata and formal languages Replayable memory and cut responses Residual tower FPRD-D42; left quotients; inverse systems of finite sets Residual towers and canonical transport Reviewed 2026-09-23 No documented external or specialist review of this FPRD result is recorded. Use the inverse-limit shift as the semantic object for an encoding-independent theory of stationary transport presentations. FPRD-T156 The inverse limit of the finite-horizon residual tower is a compact totally disconnected deterministic response machine with continuous input transitions. The full Myhill--Nerode residual space embeds equivariantly and densely. A language is regular exactly when the tower stabilizes, equivalently when its quotient sizes are bounded or one restriction map Q_(h+1) to Q_h is bijective. Theorem · canonical residual completion and stabilization criterion Self-contained proof with exhaustive finite audit Evidence and limits → Automata and formal languages Replayable memory and cut responses Residual completion theorem FPRD-D44; Myhill--Nerode theorem; inverse limits of finite sets Residual towers and canonical transport Reviewed 2026-09-23 The theorem is aligned with established profinite and topological recognition theory; no external review of this FPRD formulation is recorded. Use the stationary framework D45/T157 and later compilation results; the remaining frontier is structural lower bounds, spectrum emptiness, or explicit compilation for consequential presentations. FPRD-D43 For a demanded map on a finite product source, operational support records coordinates touched by a replay trace, semantic support records coordinates capable of changing the demanded answer, and quotient memory identifies sources with equal complete answers. These are distinct resources. Definition · three-layer replayable-memory model Defined self-containedly with exact comparison maps Evidence and limits → Automata and formal languages Replayable memory and cut responses Three memory layers FPRD-T150; FPRD-D42 The support-quotient theorem for replayable memory Reviewed 2026-09-23 No documented external or specialist review of this FPRD result is recorded. Define stationary transport cost for updating and naming quotient classes as the cut advances. FPRD-T155 For a map F on a finite product source, the essential-coordinate set E(F) is the unique least sufficient coordinate support; the minimum exact deterministic summary has |F(X)| states; and |F(X)| is at most the product of the alphabets on E(F), with equality exactly when the induced map is injective. For a family of futures, essential support is the union of component supports. Every stable adaptive replay envelope contains E(F). Theorem · exact support-quotient factorization Self-contained proof with exhaustive finite audit Evidence and limits → Automata and formal languages Replayable memory and cut responses Support-quotient theorem FPRD-D43; FPRD-T150; FPRD-T152 The support-quotient theorem for replayable memory Reviewed 2026-09-23 No documented external or specialist review of this FPRD result is recorded. Use D45/T157 and the later normal-form and selector results to study the surviving structural cost of stationary transport across cuts. FPRD-D42 A finite cut-response system records the answer beta(p,c) for each past p and possible continuation c. Its response dimension is log2 of the number of distinct response rows, separating the information needed for readiness across a continuation family from the replay support used by any one completed continuation. Definition · finite-cut communication invariant Defined self-containedly and connected exactly to residual rows Evidence and limits → Automata and formal languages Replayable memory and cut responses Cut-response definition FPRD-D41; deterministic one-way communication Cut-response factorization and linear observer dimension Reviewed 2026-09-23 No documented external or specialist review of this FPRD result is recorded. Extend the finite-horizon scaffold capacity bound to richer stationary frontier presentations. FPRD-T152 For every finite cut-response system, the minimum number of exact deterministic summary states equals the number of distinct response rows. Hence the fixed-length one-way cost is ceil(log2 R) bits for R rows. For linear observers a·x over F_q^n whose span has dimension r, the exact minimum is q^r states, or ceil(r log2 q) bits. Any resource class with at most B(s) cut presentations can realize the system only if R<=B(s). Theorem · exact cut factorization and capacity transfer Self-contained proof and exhaustive finite falsification audit Evidence and limits → Automata and formal languages Replayable memory and cut responses Cut-response factorization FPRD-D42; deterministic one-way communication; rank-nullity Cut-response factorization and linear observer dimension Reviewed 2026-09-23 No documented external or specialist review of this FPRD result is recorded. Use FPRD-T154 to replace row cardinality by a structural response invariant or a tighter reachable-presentation capacity theorem. FPRD-T153 Fix a Loff--Moreira--Reis scaffolding automaton of degree d, distance k, working alphabet size g, and control set Q. For continuation horizon h, every response row is determined by the cut control state and the radius R=k+(h-1)(k-1) unfolded neighbourhood when k,h>=1, with radius zero when k=0 or h=0. If V_0=g+1 and V_(r+1)=1+(g+1)V_r^d, then every horizon-h cut has at most |Q|V_R distinct response rows. The radius R is uniformly sharp. Theorem · readable-cone capacity and sharp horizon radius Self-contained proof with exhaustive finite structural audit Evidence and limits → Automata and formal languages Replayable memory and cut responses Finite-horizon scaffold capacity FPRD-T152; FPRD-T133; Loff--Moreira--Reis scaffolding automata Finite-horizon response capacity of scaffolding automata Reviewed 2026-09-23 No documented external or specialist review of this FPRD result is recorded. Use FPRD-T154 to replace raw row cardinality by a structural invariant that survives larger fixed scaffold parameters. FPRD-T154 For every finite input alphabet of size s, one fixed generic T153 parameter tuple, degree max(2,s), distance 2, one working label, and one control state, has a numerical abstract-view envelope at least as large as the maximum possible number of Boolean response rows over every continuation horizon h. Therefore a lower-bound proof using only finite-horizon response-row cardinality cannot exceed every T153 envelope and cannot by itself separate a language from all scaffolding automata. Any PEG transfer must account for reversal. Theorem · parameter-uniform barrier for a cardinality method Self-contained elementary proof with exact and symbolic finite audit Evidence and limits → Automata and formal languages Replayable memory and cut responses Universal row-count barrier FPRD-T152; FPRD-T153; finite Boolean response tables The universal row-count barrier Reviewed 2026-09-23 No documented external or specialist review of this FPRD result is recorded. Define a cut invariant that records advance compatibility, horizon coherence, or realizability structure rather than only the number of rows. FPRD-D41 For a fixed family of continuations, a prefix's continuation-exposed replay profile records the accept/reject response to each continuation. Pointwise replay width is the largest source slice used by one completed continuation, while the future-exposed union contains every old source coordinate selected across the family. Definition · bridge from execution slices to residual observations Defined self-containedly and calibrated on an exact selector family Evidence and limits → Automata and formal languages Replayable memory and cut responses Replay-profile definition FPRD-D40; FPRD-T150 Replay fan-out theorem Reviewed 2026-09-23 No documented external or specialist review of this FPRD result is recorded. Define transport orbits for persistent roots and test them against a visible lift of the Kim-Park SCA-hard language C. FPRD-T151 Let M contain the nonempty binary words whose middle symbol, at one-based position ceil(n/2), is 1. Every completed word has a one-source-cell replay certificate when length is public shape data. Nevertheless, for every r there are 2^r prefixes of length 2r and r continuations whose response profiles are all distinct. Thus M has at least 2^r residuals at that cut, and every exact deterministic one-pass recognizer needs at least 2^r configurations there. Theorem · replay-width/residual-fan-out separation Self-contained elementary proof and exhaustive finite audit Evidence and limits → Automata and formal languages Replayable memory and cut responses Replay fan-out separation FPRD-D41; FPRD-T150; Myhill--Nerode residual separation Replay fan-out theorem Reviewed 2026-09-23 No documented external or specialist review of this FPRD result is recorded. Use the explicit degree-two unary-query selector as a positive calibration, then study branching and merging demand families rather than a single backwards cursor. FPRD-SH-D01 For a letter-labelled NFA A A A q q q Λ A ( q ) = { σ : q → σ q } \Lambda_A(q)=\{\sigma:q\xrightarrow{\sigma}q\} Λ A ( q ) = { σ : q σ q } Definition · local quotient invariant Precisely stated and used by the obstruction theorem Evidence and limits → Automata and formal languages Prefix quotients under shuffle Loop spectrum and quotient convention No recorded dependencies FPRD Lab definition applied to Broda et al., “Location based automata for expressions with shuffle and intersection” (2023) Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use the stronger incoming-spectrum invariant FPRD-SH-T04 for non-recurrent shuffle failures. FPRD-SH-L01 For every regular expression with shuffle, every noninitial state of its prefix automaton has one incoming transition label; hence no prefix state has self-loops on two distinct letters. Lemma · structural property Self-contained proof at the stated construction Evidence and limits → Automata and formal languages Prefix quotients under shuffle Homogeneity proof Broda et al., “Location based automata for expressions with shuffle and intersection” (2023), Section 6 Broda, Machiavelo, Moreira, and Reis, “Location based automata for expressions with shuffle and intersection” (2023); FPRD reconstruction Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain homogeneity as the target-side invariant in generated quotient tests. FPRD-SH-T01 For every existential state quotient π : A ↠ B \pi:A\twoheadrightarrow B π : A ↠ B Λ A ( q ) ⊆ Λ B ( π ( q ) ) \Lambda_A(q)\subseteq\Lambda_B(\pi(q)) Λ A ( q ) ⊆ Λ B ( π ( q )) q q q Theorem · elementary quotient invariant Self-contained proof Evidence and limits → Automata and formal languages Prefix quotients under shuffle Loop-spectrum monotonicity proof FPRD-SH-D01 Elementary labelled-graph fact; FPRD application to the shuffle/prefix seam Reviewed 2026-08-31 No documented external or specialist review of these FPRD results is recorded. Use the invariant as a constant-time rejection test before exhaustive quotient search. FPRD-SH-T02 Let α = β ⨿ γ \alpha=\beta\amalg\gamma α = β ⨿ γ a ≠ b a\ne b a = b A P r e ( α ) A_{\mathrm{Pre}}(\alpha) A Pre ( α ) A P O S ( α ) A_{\mathrm{POS}}(\alpha) A POS ( α ) Theorem · infinite obstruction family Self-contained proof; exact small-case verification Evidence and limits → Automata and formal languages Prefix quotients under shuffle Independent-recurrence theorem and proof FPRD-SH-L01; FPRD-SH-T01; Broda et al., “Location based automata for expressions with shuffle and intersection” (2023) FPRD Lab analysis of the shuffle location construction in Broda et al. (2023) Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Treat this loop theorem as a special case of the exact incoming-spectrum classification FPRD-SH-T05. FPRD-SH-X01 For distinct letters a ≠ b a\ne b a = b a ∗ ⨿ b ∗ a^*\amalg b^* a ∗ ⨿ b ∗ Counterexample · sharp size bound Self-contained proof and exact verifier reproduction Evidence and limits → Automata and formal languages Prefix quotients under shuffle Minimal counterexample and transition tables FPRD-SH-T02 FPRD deduction; Broda et al. (2023), Example 13, supplies the four-occurrence comparison Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as the sharp occurrence-count boundary; make no literature-priority claim. FPRD-SH-X02 For a ∗ ⨿ a ∗ a^*\amalg a^* a ∗ ⨿ a ∗ Counterexample · sharp boundary Exact proof and exhaustive partition check Evidence and limits → Automata and formal languages Prefix quotients under shuffle Unary control and predecessor defect FPRD-SH-T03 FPRD Lab deduction using the 2023 shuffle location/prefix constructions Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain this as the smallest exceptional case in the all-length proof FPRD-SH-T06. FPRD-SH-T03 A state partition π \pi π q , q ′ q,q' q , q ′ { π ( r ) : r → σ q } \{\pi(r):r\xrightarrow{\sigma}q\} { π ( r ) : r σ q } σ \sigma σ Theorem · exact criterion Self-contained reformulation of the standard definition Evidence and limits → Automata and formal languages Prefix quotients under shuffle Predecessor criterion Left invariance on the reversed automaton 2019 left-quotient architecture; FPRD predecessor-profile reformulation Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Combine this criterion with Boolean block equations for larger SAT-checkable quotient certificates. FPRD-SH-C01 For ( ( a b ) ∗ ) ⨿ ( ( b c ) ∗ ) ((ab)^*)\amalg((bc)^*) (( ab ) ∗ ) ⨿ (( b c ) ∗ ) Computational finding · source reproduction Independently reproduced with an exact structural checker Evidence and limits → Automata and formal languages Prefix quotients under shuffle Published example reconstruction Broda et al., “Location based automata for expressions with shuffle and intersection” (2023), Section 6 Broda, Machiavelo, Moreira, and Reis, “Location based automata for expressions with shuffle and intersection” (2023), Example 13 Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use the incoming-spectrum witness from FPRD-SH-T04 as the direct explanation of this example. FPRD-SH-C02 Among all 306 expressions x ∗ ⨿ y ∗ x^*\amalg y^* x ∗ ⨿ y ∗ { a , b , c } \{a,b,c\} { a , b , c } ∣ x ∣ + ∣ y ∣ ≤ 4 |x|+|y|\le4 ∣ x ∣ + ∣ y ∣ ≤ 4 Computational finding · bounded census Exhaustive within the stated finite domain; its pattern is now proved by FPRD-SH-T05 Evidence and limits → Automata and formal languages Prefix quotients under shuffle Census table and scope Exact automaton constructor; Exhaustive set-partition search FPRD Lab bounded starred-word shuffle census Reviewed 2026-08-31 No documented external or specialist review of these FPRD results is recorded. Retain this census as the discovery record and finite cross-check for FPRD-SH-T05. FPRD-SH-T04 For a letter-labelled NFA A A A I A ( q ) = { σ : ∃ p ( p → σ q ) } I_A(q)=\{\sigma:\exists p\;(p\xrightarrow{\sigma}q)\} I A ( q ) = { σ : ∃ p ( p σ q )} π : A ↠ B \pi:A\twoheadrightarrow B π : A ↠ B I A ( q ) ⊆ I B ( π ( q ) ) I_A(q)\subseteq I_B(\pi(q)) I A ( q ) ⊆ I B ( π ( q )) q q q Theorem · local quotient invariant Self-contained proof; strictly strengthens the loop-spectrum test Evidence and limits → Automata and formal languages Prefix quotients under shuffle Incoming-spectrum theorem Existential block-transition convention Elementary labelled-graph fact; FPRD application to shuffle locations Reviewed 2026-08-31 No documented external or specialist review of these FPRD results is recorded. Test the invariant on broader non-starred shuffle syntax. FPRD-SH-T05 For nonempty words x , y x,y x , y A P r e ( x ∗ ⨿ y ∗ ) A_{\mathrm{Pre}}(x^*\amalg y^*) A Pre ( x ∗ ⨿ y ∗ ) A P O S ( x ∗ ⨿ y ∗ ) A_{\mathrm{POS}}(x^*\amalg y^*) A POS ( x ∗ ⨿ y ∗ ) x = a m x=a^m x = a m y = a n y=a^n y = a n a a a m , n ≥ 1 m,n\ge1 m , n ≥ 1 Theorem · exact classification Self-contained proof with a closed-form quotient certificate and executable audit Evidence and limits → Automata and formal languages Prefix quotients under shuffle Exact dichotomy and constructive proof FPRD-SH-L01; FPRD-SH-T04; Broda et al., “Location based automata for expressions with shuffle and intersection” (2023) FPRD Lab classification using the shuffle location/prefix constructions of Broda et al. (2023) Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use FPRD-SH-T06 for the stronger left-invariant classification. FPRD-SH-T06 For all nonempty words x , y x,y x , y A P r e ( x ∗ ⨿ y ∗ ) A_{\mathrm{Pre}}(x^*\amalg y^*) A Pre ( x ∗ ⨿ y ∗ ) A P O S ( x ∗ ⨿ y ∗ ) A_{\mathrm{POS}}(x^*\amalg y^*) A POS ( x ∗ ⨿ y ∗ ) Theorem · exact classification Self-contained all-length proof with exact boundary and parameter audits Evidence and limits → Automata and formal languages Prefix quotients under shuffle Complete left-quotient obstruction FPRD-SH-T03; FPRD-SH-T05; Broda et al., “Location based automata for expressions with shuffle and intersection” (2023) FPRD Lab deduction using the shuffle location/prefix constructions of Broda et al. (2023) Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Test whether an analogous predecessor obstruction classifies broader non-starred shuffle syntax. FPRD-SH-C03 For 1 ≤ m , n ≤ 16 1\le m,n\le16 1 ≤ m , n ≤ 16 ( a m ) ∗ ⨿ ( a n ) ∗ (a^m)^*\amalg(a^n)^* ( a m ) ∗ ⨿ ( a n ) ∗ Computational finding · theorem audit Exact equality checks pass at all nine selected parameter pairs Evidence and limits → Automata and formal languages Prefix quotients under shuffle Executable audit FPRD-SH-T05; Exact automaton constructor FPRD Lab parameterized certificate verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Keep the finite audit synchronized with any proof or implementation revision. FPRD-SH-D02 For strong synchronization, solo terminal events are allowed only outside Γ \Gamma Γ Γ \Gamma Γ R ε R_\varepsilon R ε Definition · FPRD extension of the cited location framework Precisely stated for strong and arbitrary synchronization; the weak operator uses a separate backward-memory definition Evidence and limits → Automata and formal languages Prefix quotients under shuffle Synchronized prefix convention Broda et al., “The Prefix Automaton” (2021); Broda et al., “Location automata for synchronised shuffle expressions” (2023) FPRD prefix extension of Broda et al., “The Prefix Automaton” (2021), and Broda et al., “Location automata for synchronised shuffle expressions” (2023) Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Keep the strong/arbitrary convention separate from the proved weak backward receipt. FPRD-SH-T07 For m , n ≥ 1 m,n\ge1 m , n ≥ 1 Γ = { a } \Gamma=\{a\} Γ = { a } ( a m ) ∗ ⨿ s Γ ( a n ) ∗ (a^m)^*\mathbin{\amalg^{\Gamma}_{s}}(a^n)^* ( a m ) ∗ ⨿ s Γ ( a n ) ∗ lcm ( m , n ) \operatorname{lcm}(m,n) lcm ( m , n ) Theorem · exact all-parameter classification Self-contained orbit proof with parameterized executable audit Evidence and limits → Automata and formal languages Prefix quotients under shuffle Mandatory-synchronization theorem FPRD-SH-D02; Broda et al., “Location automata for synchronised shuffle expressions” (2023), strong synchronized-shuffle construction FPRD deduction from the Broda–Machiavelo–Moreira–Reis strong synchronized-shuffle construction (2023) Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Determine which non-unary strong synchronized families retain the same accessible-orbit quotient. FPRD-SH-T08 For m , n ≥ 1 m,n\ge1 m , n ≥ 1 Γ = { a } \Gamma=\{a\} Γ = { a } ( a m ) ∗ ⨿ a Γ ( a n ) ∗ (a^m)^*\mathbin{\amalg^{\Gamma}_{a}}(a^n)^* ( a m ) ∗ ⨿ a Γ ( a n ) ∗ min ( m , n ) = 1 \min(m,n)=1 min ( m , n ) = 1 m = n = 1 m=n=1 m = n = 1 Theorem · exact all-parameter classification Self-contained necessity and constructive sufficiency proofs with exhaustive boundary audit Evidence and limits → Automata and formal languages Prefix quotients under shuffle Arbitrary-synchronization classification FPRD-SH-D02; FPRD-SH-T03; Broda et al., “Location automata for synchronised shuffle expressions” (2023), arbitrary synchronized-shuffle construction FPRD deduction from the Broda–Machiavelo–Moreira–Reis arbitrary synchronized-shuffle construction (2023) Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Test whether the forced-initial-block obstruction extends to non-unary arbitrary synchronization. FPRD-SH-B01 The published weak synchronized location construction records forward memory Δ , Λ \Delta,\Lambda Δ , Λ Boundary · resolved definition gate Requirement discharged by the proved reversal-dual construction Evidence and limits → Automata and formal languages Prefix quotients under shuffle Weak-synchronization boundary Broda et al., “Location automata for synchronised shuffle expressions” (2023), weak synchronized-shuffle construction; Broda et al., “The Prefix Automaton” (2021) FPRD analysis of the directionality mismatch in the cited constructions Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain the directionality distinction when extending the receipt beyond the unary family. FPRD-SH-D03 Define u ⋈ ← Γ , D , E v = { z R : z ∈ u R ⋈ Γ , D , E v R } u\overleftarrow{\bowtie}_{\Gamma,D,E}v=\{z^R:z\in u^R\bowtie_{\Gamma,D,E}v^R\} u ⋈ Γ , D , E v = { z R : z ∈ u R ⋈ Γ , D , E v R } R ε R_\varepsilon R ε Definition theorem · backward-memory construction Self-contained reversal proof with exact unary graph audit Evidence and limits → Automata and formal languages Prefix quotients under shuffle Backward-receipt definition and proof FPRD-SH-B01; Broda et al., “The Prefix Automaton” (2021); Broda et al., “Location automata for synchronised shuffle expressions” (2023), weak synchronized-shuffle operator FPRD reversal-dual extension of the cited weak synchronized framework Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Test whether the receipt remains finite and useful for non-unary or nested weak shuffles. FPRD-SH-T09 For every m , n ≥ 1 m,n\ge1 m , n ≥ 1 ( a m ) ∗ ⨿ { a } w ( a n ) ∗ (a^m)^*\mathbin{\amalg^w_{\{a\}}}(a^n)^* ( a m ) ∗ ⨿ { a } w ( a n ) ∗ Theorem · exact constructive quotient All-length proof with closed-form quotient and exact parameter audit Evidence and limits → Automata and formal languages Prefix quotients under shuffle Weak ordinary-quotient theorem FPRD-SH-D03; Broda et al., “Location automata for synchronised shuffle expressions” (2023), weak synchronized-shuffle construction FPRD deduction from the Broda–Machiavelo–Moreira–Reis weak synchronized-shuffle construction (2023) and the FPRD reversal-dual receipt Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Search for a non-unary family in which the shifted receipt projection remains exact. FPRD-SH-T10 For every m , n ≥ 1 m,n\ge1 m , n ≥ 1 ( a m ) ∗ ⨿ { a } w ( a n ) ∗ (a^m)^*\mathbin{\amalg^w_{\{a\}}}(a^n)^* ( a m ) ∗ ⨿ { a } w ( a n ) ∗ Theorem · exact impossibility classification All-length determinization-orbit proof with exceptional-case audit Evidence and limits → Automata and formal languages Prefix quotients under shuffle Weak left-quotient obstruction FPRD-SH-D03; Determinization preservation under left quotients FPRD determinization-orbit consequence for the Broda–Machiavelo–Moreira–Reis weak location construction and the FPRD prefix receipt Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Test eventual subset-period mismatch as an obstruction for non-unary synchronized products. FPRD-SH-C05 Exact construction verifies the weak ordinary quotient for 1,024 pairs with 1 ≤ m , n ≤ 32 1\le m,n\le32 1 ≤ m , n ≤ 32 1 ≤ m , n ≤ 16 1\le m,n\le16 1 ≤ m , n ≤ 16 ( 1 , 1 ) , ( 1 , 2 ) , ( 2 , 1 ) (1,1),(1,2),(2,1) ( 1 , 1 ) , ( 1 , 2 ) , ( 2 , 1 ) Computational finding · theorem audit All exact structural, orbit, and boundary checks pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Weak synchronized audit FPRD-SH-T09; FPRD-SH-T10; Exact automaton constructor FPRD Lab weak-synchronization verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Keep the verifier synchronized with any extension beyond the unary family. FPRD-SH-C04 Exact construction checks 576 strong and 576 arbitrary synchronized pairs for 1 ≤ m , n ≤ 24 1\le m,n\le24 1 ≤ m , n ≤ 24 Computational finding · theorem audit Exact structural and exhaustive boundary checks pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Synchronized threshold audit FPRD-SH-T07; FPRD-SH-T08; Exact automaton constructor FPRD Lab synchronized-shuffle verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Extend the exact checker to a non-unary synchronized family only after its prefix receipt is stated precisely. FPRD-SH-T11 Let ∥ ψ \Vert_\psi ∥ ψ E i E_i E i A i A_i A i E = ∏ i E i E=\prod_iE_i E = ∏ i E i ∥ ψ ( A 1 , … , A n ) \Vert_\psi(A_1,\ldots,A_n) ∥ ψ ( A 1 , … , A n ) ∥ ψ ( A 1 , … , A n ) / E ≅ ∥ ψ ( A 1 / E 1 , … , A n / E n ) \Vert_\psi(A_1,\ldots,A_n)/E\cong\Vert_\psi(A_1/E_1,\ldots,A_n/E_n) ∥ ψ ( A 1 , … , A n ) / E ≅ ∥ ψ ( A 1 / E 1 , … , A n / E n ) Theorem · arbitrary-arity quotient transfer Self-contained predecessor proof with strengthened independent boundary audit Evidence and limits → Automata and formal languages Prefix quotients under shuffle Boolean-product transfer theorem FPRD-SH-T03; The 2026 Boolean-product automaton construction Broda–Machiavelo–Moreira–Reis (2026) product construction; FPRD left-handed consequence using the Broda–Holzer–Maia–Moreira–Reis (2019) definition of left invariance Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Compare the canonical product of component prefix quotients with the natural prefix automaton of one Boolean-product expression. FPRD-SH-B02 For ordinary component expressions, FPRD-SH-T11 gives a canonical left quotient from the Boolean product of their position automata to the Boolean product of their prefix automata. This target need not equal the natural prefix automaton of the combined Boolean-product expression: pure shuffle a ∗ ⨿ b ∗ a^*\amalg b^* a ∗ ⨿ b ∗ Boundary · exact construction separation Exact boundary, now explained by the event-signature expansion theorem Evidence and limits → Automata and formal languages Prefix quotients under shuffle Two prefix constructions FPRD-SH-T11; FPRD-SH-X01; The classical position-to-prefix left quotient FPRD comparison of the 2026 Boolean-product automaton with the 2021/2023 prefix constructions Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use FPRD-SH-T12 through FPRD-SH-T14 for the exact construction and policy criteria. FPRD-SH-T12 For a flat Boolean-product expression with marked ordinary components, the natural backward prefix automaton is isomorphic to the useful canonical product of the component prefix automata after splitting every noninitial product state q q q ( a , S ) ∈ Sig ( q ) (a,S)\in\operatorname{Sig}(q) ( a , S ) ∈ Sig ( q ) ∣ Q P r e ∣ = 1 + ∑ q ≠ q 0 ∣ Sig ( q ) ∣ |Q_{\mathrm{Pre}}|=1+\sum_{q\ne q_0}|\operatorname{Sig}(q)| ∣ Q Pre ∣ = 1 + ∑ q = q 0 ∣ Sig ( q ) ∣ Theorem · exact construction identification Self-contained structural proof with exact projection audit Evidence and limits → Automata and formal languages Prefix quotients under shuffle Event-signature expansion theorem FPRD-SH-T11; The 2021 prefix recursion; The 2026 Boolean-product support policy FPRD extension of the 2021 prefix and 2026 Boolean-product constructions Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Compare the event-signature expansion directly with the 2026 paper's Glushkov and follow constructions. FPRD-SH-T13 For a fixed flat Boolean-product expression with marked ordinary components, the natural prefix automaton is isomorphic to the useful canonical component-prefix product if and only if every noninitial useful product state q q q q q q Corollary · expression-specific iff criterion Immediate exact consequence of the event-signature expansion Evidence and limits → Automata and formal languages Prefix quotients under shuffle Unique-signature criterion FPRD-SH-T12 FPRD event-signature analysis Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use the signature count as the exact state-overhead statistic for algorithmic bounds. FPRD-SH-T14 A memoryless Boolean policy makes the natural prefix automaton isomorphic to the useful canonical component-prefix product for every tuple of ordinary component expressions if and only if every active letter a a a S a S_a S a S a ∩ S b ≠ ∅ S_a\cap S_b\ne\varnothing S a ∩ S b = ∅ Theorem · sharp universal policy classification Self-contained necessity and sufficiency proof with independent complete small-policy audit Evidence and limits → Automata and formal languages Prefix quotients under shuffle Signature-rigidity classification FPRD-SH-T12; FPRD-SH-T13; Homogeneity of component prefix automata FPRD deduction from Broda–Maia–Moreira–Reis (2021) and Broda–Machiavelo–Moreira–Reis (2026) Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use FPRD-SH-T15 and FPRD-SH-T16 for the exact local bound and its policy-only complexity boundary. FPRD-SH-T15 Let C ψ C_\psi C ψ ( a , S ) (a,S) ( a , S ) ω ( C ψ ) \omega(C_\psi) ω ( C ψ ) ∣ Sig ( q ) ∣ ≤ ω ( C ψ ) |\operatorname{Sig}(q)|\le\omega(C_\psi) ∣ Sig ( q ) ∣ ≤ ω ( C ψ ) Δ ( E ) ≤ ( ω ( C ψ ) − 1 ) ( ∣ Q ( P ) ∣ − 1 ) \Delta(E)\le(\omega(C_\psi)-1)(|Q(P)|-1) Δ ( E ) ≤ ( ω ( C ψ ) − 1 ) ( ∣ Q ( P ) ∣ − 1 ) Theorem · exact support-graph state-complexity bound Self-contained upper bound and exact starred realization; finite audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle Compatibility-graph theorem FPRD-SH-T12; Homogeneity of component prefix states; Graph clique number FPRD support-graph consequence of the Boolean-product event-signature expansion Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use FPRD-SH-T17 and FPRD-SH-T18 for the exact global collision receipt and disjoint-support count. FPRD-SH-T16 Given an explicitly listed memoryless support policy ψ \psi ψ k k k k k k Theorem · computational complexity classification Self-contained reduction from three-dimensional matching; exact finite reduction audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle NP-completeness proof FPRD-SH-T15; Karp's NP-completeness of three-dimensional matching FPRD reduction from the classical three-dimensional matching problem Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Identify tractable policy classes and parameterizations for the compatibility clique number. FPRD-SH-T17 For a fixed flat memoryless Boolean-product expression, let T σ T_\sigma T σ σ \sigma σ Δ ( E ) = ∑ σ ∣ T σ ∣ − ∣ ⋃ σ T σ ∣ \Delta(E)=\sum_\sigma|T_\sigma|-|\bigcup_\sigma T_\sigma| Δ ( E ) = ∑ σ ∣ T σ ∣ − ∣ ⋃ σ T σ ∣ Theorem · exact global state-count identity Self-contained double-counting and inclusion–exclusion proof; complete finite audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle Global collision calculus FPRD-SH-T12; FPRD-SH-T15; Finite inclusion–exclusion FPRD global consequence of the Boolean-product event-signature expansion Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Optimize the matching-indexed target intersections for overlapping one-support policies. FPRD-SH-T18 For a one-support-per-letter policy with pairwise-disjoint active supports, let N a N_a N a a a a r r r M = ∏ a N a M=\prod_aN_a M = ∏ a N a Δ ( E ) = ∑ a ( N a − 1 ) ∏ b ≠ a N b − ( M − 1 ) = ( r − 1 ) M − M ∑ a N a − 1 + 1 \Delta(E)=\sum_a(N_a-1)\prod_{b\ne a}N_b-(M-1)=(r-1)M-M\sum_aN_a^{-1}+1 Δ ( E ) = ∑ a ( N a − 1 ) ∏ b = a N b − ( M − 1 ) = ( r − 1 ) M − M ∑ a N a − 1 + 1 Theorem · exact prescribed-size global overhead Self-contained Cartesian-factorization proof; strict-gap scope corrected and independently audited Evidence and limits → Automata and formal languages Prefix quotients under shuffle Disjoint-support overhead theorem FPRD-SH-T17; Pairwise-disjoint event supports; Useful synchronous block products FPRD extension of the shuffle and Boolean-product automata frameworks Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Determine the exact prescribed-size maximum when one-support events overlap. FPRD-SH-T19 Create one primary selector item for every policy signature σ = ( a , S ) \sigma=(a,S) σ = ( a , S ) S S S a a a Theorem · exact sparse constraint compilation Self-contained bijection proof; exhaustive color-consistency audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle Exact-cover-with-colors compilation FPRD-SH-T15; Knuth's exact covering with colors FPRD compilation into Knuth's XCC model Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use FPRD-SH-T20 and FPRD-SH-T21 for the exact one-shot algorithm and its counting boundary. FPRD-SH-T20 For a graph G G G a e a_e a e e e e v v v ε + ∑ e ∋ v a e \varepsilon+\sum_{e\ni v}a_e ε + ∑ e ∋ v a e M M M M M M ∣ M ∣ |M| ∣ M ∣ Δ ( G ) = ∑ M ( ∣ M ∣ − 1 ) + \Delta(G)=\sum_M(|M|-1)_+ Δ ( G ) = ∑ M ( ∣ M ∣ − 1 ) + Theorem · exact automata-to-matching correspondence Self-contained all-graph proof; exact product exploration audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle One-shot matching model FPRD-SH-T12; FPRD-SH-T19; Finite graph matchings FPRD one-shot specialization of the Boolean-product framework Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use the XCC compilation to enumerate matching receipts without constructing the canonical product. FPRD-SH-T21 Computing the one-shot overhead Δ ( G ) = ∑ M ( ∣ M ∣ − 1 ) + \Delta(G)=\sum_M(|M|-1)_+ Δ ( G ) = ∑ M ( ∣ M ∣ − 1 ) + Z ( G ) Z(G) Z ( G ) Z ( G ) = 1 + Δ ( G ⊔ K 2 ) − 2 Δ ( G ) Z(G)=1+\Delta(G\sqcup K_2)-2\Delta(G) Z ( G ) = 1 + Δ ( G ⊔ K 2 ) − 2Δ ( G ) Theorem · exact counting-complexity classification Self-contained membership and isolated-edge reduction; exact finite audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle Counting-hardness boundary FPRD-SH-T20; Valiant's #P-completeness of counting matchings FPRD reduction from Valiant's classical matching-count problem Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Study sparse, bounded-width, and structurally restricted policy classes where XCC enumeration is effective. FPRD-SH-T22 For a one-support-per-letter policy with support family F ⊆ ( [ n ] r ) \mathcal F\subseteq\binom{[n]}r F ⊆ ( r [ n ] ) F \mathcal F F K G n , r KG_{n,r} K G n , r n < 2 r n<2r n < 2 r n ≥ 2 r n\geq2r n ≥ 2 r ∣ F ∣ ≤ ( n − 1 r − 1 ) |\mathcal F|\leq\binom{n-1}{r-1} ∣ F ∣ ≤ ( r − 1 n − 1 ) n > 2 r n>2r n > 2 r r ≥ 2 r\geq2 r ≥ 2 n > 2 r n>2r n > 2 r ( n − 1 r − 1 ) − ( n − r − 1 r − 1 ) + 1 \binom{n-1}{r-1}-\binom{n-r-1}{r-1}+1 ( r − 1 n − 1 ) − ( r − 1 n − r − 1 ) + 1 n = 2 r n=2r n = 2 r r ≥ 2 r\geq2 r ≥ 2 Theorem · classical extremal transfer and sharp boundary Exact automata reduction with classical EKR and Hilton–Milner inputs; equality cases audited Evidence and limits → Automata and formal languages Prefix quotients under shuffle Uniform-support trichotomy FPRD-SH-T14; Erdős–Ko–Rado theorem; Hilton–Milner theorem FPRD automata transfer of the Erdős–Ko–Rado and Hilton–Milner theorems Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use FPRD-SH-T23 for the quantitative receipt once the EKR ceiling is crossed. FPRD-SH-T23 Assume 1 ≤ r ≤ n / 2 1\leq r\leq n/2 1 ≤ r ≤ n /2 N = ( n r ) N=\binom nr N = ( r n ) d = ( n − r r ) d=\binom{n-r}r d = ( r n − r ) τ = ( n − r − 1 r − 1 ) \tau=\binom{n-r-1}{r-1} τ = ( r − 1 n − r − 1 ) α = ( n − 1 r − 1 ) \alpha=\binom{n-1}{r-1} α = ( r − 1 n − 1 ) r r r m > α m>\alpha m > α ⌈ d + τ 2 N m ( m − α ) ⌉ \left\lceil\frac{d+\tau}{2N}m(m-\alpha)\right\rceil ⌈ 2 N d + τ m ( m − α ) ⌉ Theorem · spectral collision and overhead lower bound Self-contained spectral derivation from the known Kneser spectrum; exact finite audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle Spectral collision receipt FPRD-SH-T20; Kneser graph spectrum; Rayleigh quotient FPRD composition of the classical Kneser spectrum with the one-shot matching theorem Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Replace the general spectral receipt with the exact diversity and supersaturation hierarchy in its valid parameter ranges. FPRD-SH-T24 For an r r r F \mathcal F F m = ∣ F ∣ m=|\mathcal F| m = ∣ F ∣ d d d γ = m − d \gamma=m-d γ = m − d q ( F ) q(\mathcal F) q ( F ) q ( F ) ≥ γ max { 0 , d − [ ( n − 1 r − 1 ) − ( n − r − 1 r − 1 ) ] } q(\mathcal F)\geq\gamma\max\{0,d-[{n-1\choose r-1}-{n-r-1\choose r-1}]\} q ( F ) ≥ γ max { 0 , d − [ ( r − 1 n − 1 ) − ( r − 1 n − r − 1 ) ]} Theorem · quantitative obstruction certificate Self-contained all-length counting proof; complete small-family audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle Diversity obstruction receipt FPRD-SH-T14; FPRD-SH-T15; Uniform support counting FPRD translation of an elementary extremal-set count Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Test sharpness at the first positive-overhead layer and determine how pair receipts aggregate into total prefix-state overhead. FPRD-SH-T31 Let x x x A \mathcal A A x x x B \mathcal B B γ \gamma γ x x x N ⊆ B N\subseteq\mathcal B N ⊆ B N ∪ { A } N\cup\{A\} N ∪ { A } A ∈ A A\in\mathcal A A ∈ A O ( ∣ F ∣ 2 γ ) O(|\mathcal F|2^\gamma) O ( ∣ F ∣ 2 γ ) Theorem · exact fixed-parameter target factorization Self-contained proof; exact policy-valid target audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle Diversity factorization theorem FPRD-SH-T17; FPRD-SH-T19; Support-family diversity Kupavskii (2018) supplies the diversity parameter; the target factorization is an FPRD deduction Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Test the factorization against an externally posed problem before extending the framework further. FPRD-SH-T32 Group each hub support A A A μ ( A ) = { j : A ∩ B j ≠ ∅ } ⊆ [ γ ] \mu(A)=\{j:A\cap B_j\ne\varnothing\}\subseteq[\gamma] μ ( A ) = { j : A ∩ B j = ∅ } ⊆ [ γ ] O ( ∣ F ∣ r γ + γ 2 γ ) O(|\mathcal F|r\gamma+\gamma2^\gamma) O ( ∣ F ∣ r γ + γ 2 γ ) O ( 2 γ ) O(2^\gamma) O ( 2 γ ) Theorem · fixed-parameter algorithm and canonical quotient Self-contained proof; complete small-domain and sharpness audits pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Conflict-mask quotient and zeta algorithm FPRD-SH-T20; FPRD-SH-T31; Subset zeta transform FPRD automata specialization using the classical subset-zeta transform of Björklund et al. Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Seek an independently motivated application; do not optimize the same kernel in isolation. FPRD-SH-T33 Let C ⊆ F \mathcal C\subseteq\mathcal F C ⊆ F B = F ∖ C \mathcal B=\mathcal F\setminus\mathcal C B = F ∖ C ∣ B ∣ = k |\mathcal B|=k ∣ B ∣ = k B \mathcal B B C \mathcal C C k k k κ ( F ) = τ ( D F ) \kappa(\mathcal F)=\tau(D_{\mathcal F}) κ ( F ) = τ ( D F ) κ ≤ γ \kappa\le\gamma κ ≤ γ Theorem · optimal intersecting-core decomposition Self-contained proof; exact minimum-cover and target audits pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Intersecting-core factorization FPRD-SH-T17; FPRD-SH-T31; Minimum vertex cover FPRD correction using an elementary disjointness-graph decomposition; Harris–Narayanaswamy (2024) is the algorithmic comparator Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use kappa only as the optimum of this supplied-core decomposition; do not infer a general arithmetic lower bound. FPRD-SH-B10 For every prime power q q q P G ( 2 , q ) PG(2,q) PG ( 2 , q ) κ = 0 \kappa=0 κ = 0 q 2 + q + 1 q^2+q+1 q 2 + q + 1 q + 1 q+1 q + 1 γ = q 2 \gamma=q^2 γ = q 2 γ − κ \gamma-\kappa γ − κ Boundary result · unbounded parameter gap Self-contained finite-geometry proof; exact q=2,3,5 controls pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Unbounded diversity gap FPRD-SH-T33; Dembowski, Finite Geometries Dembowski (1968) supplies the projective-plane incidence facts; the kernel comparison is an FPRD boundary control Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Do not describe diversity as a complete or optimal search kernel. FPRD-SH-C18 Exact checks cover 1,088 complete support families, 31,377 matching states across complete and larger controls, 1,200 policy-valid target systems with 7,281 useful states, and projective planes of orders 2, 3, and 5. Direct enumeration and the minimum-cover kernel agree in every case. Computational finding · corrected-kernel audit All exact checks pass; deterministic rerun is byte-identical Evidence and limits → Automata and formal languages Prefix quotients under shuffle Intersecting-core audit FPRD-SH-T33; FPRD-SH-B10; Exact enumeration FPRD Lab intersecting-core verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as supporting evidence; arbitrary-size conclusions come from the proofs. FPRD-SH-B11 With the slice length encoded in unary, exact counting of the Mazurkiewicz traces meeting a length slice of a DFA language is # P \#\mathrm P # P a I b a\mathrel{\mathbb I}b a I b Boundary theorem · published-hardness parameter extraction Published parsimonious reduction; parameter corollary checked directly Evidence and limits → Automata and formal languages Prefix quotients under shuffle Trace-cover hardness boundary de Colnet–Meel–Mathur Theorem 3.2; Polynomial DFA word counting de Colnet, Meel, and Mathur (POPL 2026), Theorem 3.2; FPRD parameter extraction Reviewed 2026-09-01 The underlying parsimonious reduction was peer reviewed at POPL 2026; the vertex-cover extraction has no separate external review. Do not seek an FPT algorithm from an alphabet-only cover; also control the sequential presentation orbit exposed to the DFA. FPRD-SH-T34 Given an m m m B B B ∣ B ∣ = κ |B|=\kappa ∣ B ∣ = κ O ( ∣ Σ ∣ κ 2 κ m ) O(|\Sigma|\kappa 2^\kappa m) O ( ∣Σ∣ κ 2 κ m ) O ( 2 κ m ) O(2^\kappa m) O ( 2 κ m ) Theorem · exact fixed-parameter algorithm Self-contained proof; exhaustive and randomized exact audits pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle One-step cover dynamic program FPRD-SH-T33; DFA subset dynamic programming; Foata steps FPRD trace specialization of the intersecting-core decomposition Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use this as the exact scope boundary; any lift to full traces must add a parameter controlling sequential residual amplification. FPRD-SH-C19 Direct trace-step enumeration and the cover dynamic program agree on all 64 four-letter independence graphs, all 65,536 complete two-state DFA instances and final sets, 2,500 larger deterministic controls, and 4,000 DNF reduction-pattern controls. Two complete runs are byte-identical. Computational finding · algorithm and boundary audit All exact checks pass; deterministic rerun is byte-identical Evidence and limits → Automata and formal languages Prefix quotients under shuffle Trace-cover exact audit FPRD-SH-B11; FPRD-SH-T34; Exact enumeration FPRD Lab trace-cover verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as supporting evidence; the arbitrary-size conclusions come from the proof and the published reduction. FPRD-SH-B09 The canonical hub quotient can have all 2 γ 2^\gamma 2 γ γ + 1 \gamma+1 γ + 1 2 γ + 1 2^{\gamma+1} 2 γ + 1 2 Ω ( γ ) 2^{\Omega(\gamma)} 2 Ω ( γ ) Boundary result · sharp representation and output costs Explicit constructions and exact formulas proved Evidence and limits → Automata and formal languages Prefix quotients under shuffle Sharpness and scope boundary FPRD-SH-T31; FPRD-SH-T32; FPRD-SH-T21 FPRD explicit construction and scope analysis Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Do not claim an arithmetic lower bound without a separate parameterized reduction. FPRD-SH-C17 Exact checks cover 33,856 complete support families, 738,063 matching states, 2,000 policy-valid target systems with 24,636 useful states, both small-diversity boundaries, and both sharpness constructions. All checks pass; a complete rerun is byte-identical. Computational finding · exact algorithm and boundary audit All exact checks pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Diversity-kernel audit FPRD-SH-T31; FPRD-SH-T32; FPRD-SH-B09; Exact enumeration FPRD Lab diversity-kernel verifier and independent result review Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as evidence; arbitrary-size conclusions come from the proofs. FPRD-SH-C11 Exact enumeration checks 1,082,432 support families in four complete small domains, all 182 maximal intersecting families at ( n , r ) = ( 7 , 3 ) (n,r)=(7,3) ( n , r ) = ( 7 , 3 ) ( 7 , 3 ) (7,3) ( 7 , 3 ) Computational finding · extremal and spectral audit Source replay and independent boundary audit pass; T22/T23 hypotheses corrected Evidence and limits → Automata and formal languages Prefix quotients under shuffle Uniform-support exact audit FPRD-SH-T22; FPRD-SH-T23; FPRD-SH-T24; Exact enumeration FPRD Lab uniform-support verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as implementation evidence; use the classical theorems and spectral proof for arbitrary parameters. FPRD-SH-T25 Let J ψ J_\psi J ψ ψ ⊗ k \psi^{\otimes k} ψ ⊗ k U k U^k U k S ( a 1 , … , a k ) = S a 1 × ⋯ × S a k S_{(a_1,\ldots,a_k)}=S_{a_1}\times\cdots\times S_{a_k} S ( a 1 , … , a k ) = S a 1 × ⋯ × S a k J ψ ⊗ k = J ψ ⊠ k J_{\psi^{\otimes k}}=J_\psi^{\boxtimes k} J ψ ⊗ k = J ψ ⊠ k Theorem · exact policy-to-graph-product correspondence Self-contained all-length proof; exhaustive finite tensor audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle Support-tensor theorem FPRD-SH-T15; Strong graph product; Cartesian products of finite supports FPRD deduction in the strong-product framework of Lovász (1979) Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use FPRD-SH-T26 as a policy-level capacity dictionary; keep expression reachability as a separate proof obligation. FPRD-SH-T26 With Ω ( ψ ) = α ( J ψ ) \Omega(\psi)=\alpha(J_\psi) Ω ( ψ ) = α ( J ψ ) Ω ∞ ( ψ ) = sup k ≥ 1 Ω ( ψ ⊗ k ) 1 / k \Omega_\infty(\psi)=\sup_{k\ge1}\Omega(\psi^{\otimes k})^{1/k} Ω ∞ ( ψ ) = sup k ≥ 1 Ω ( ψ ⊗ k ) 1/ k Ω ∞ ( ψ ) = Θ ( J ψ ) \Omega_\infty(\psi)=\Theta(J_\psi) Ω ∞ ( ψ ) = Θ ( J ψ ) J ψ J_\psi J ψ Theorem · exact asymptotic-capacity identity Self-contained corollary and constructive graph-representation proof; exact audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle Shannon-capacity identity FPRD-SH-T25; FPRD-SH-T15; Definition of Shannon capacity FPRD automata interpretation of classical Shannon capacity Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Compile structured graph codes into reachable expression automata without treating tensor vertices as already-reachable letters. FPRD-SH-B03 For the complete r r r J ψ = K G n , r ‾ J_\psi=\overline{KG_{n,r}} J ψ = K G n , r r ∣ n r\mid n r ∣ n n / r n/r n / r r ∤ n r\nmid n r ∤ n ⌊ n / r ⌋ \lfloor n/r\rfloor ⌊ n / r ⌋ n / r n/r n / r T 5 = K G 5 , 2 ‾ T_5=\overline{KG_{5,2}} T 5 = K G 5 , 2 α ( T 5 ⊠ d ) = 2 , 5 , 12 , 27 \alpha(T_5^{\boxtimes d})=2,5,12,27 α ( T 5 ⊠ d ) = 2 , 5 , 12 , 27 d = 1 , 2 , 3 , 4 d=1,2,3,4 d = 1 , 2 , 3 , 4 Boundary result · reduction to a published graph-capacity problem Exact reduction to the published triangular-graph capacity problem; no new capacity bound claimed Evidence and limits → Automata and formal languages Prefix quotients under shuffle Complement-of-Kneser boundary FPRD-SH-T26; Kneser graphs; Triangular-graph capacity results Kizhakkepallathu, Östergård, and Popa (2013) Reviewed 2026-09-01 The triangular-graph bounds are published; the FPRD policy translation has no external review. Determine or tighten 60 <= alpha(T5 strong-power 5) <= 67 with symmetry-reduced XCC/DLX. FPRD-SH-C12 Exact enumeration checks 39,693 tensor vertex pairs, uniform policy representations of all 1,099 graphs through five vertices, tensor identities for every graph through four vertices, the complete two-support realization of T 5 T_5 T 5 C 9 C_9 C 9 Computational finding · Shannon bridge audit All exact checks pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Support-tensor exact audit FPRD-SH-T25; FPRD-SH-T26; FPRD-SH-B03; Exact enumeration FPRD Lab support-tensor verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use the verified policy dictionary as a gate before claiming any expression-level realization. FPRD-SH-T27 If the support-overlap graph J ψ J_\psi J ψ Ω ∞ ( ψ ) = Ω ( ψ ) = α ( J ψ ) \Omega_\infty(\psi)=\Omega(\psi)=\alpha(J_\psi) Ω ∞ ( ψ ) = Ω ( ψ ) = α ( J ψ ) Corollary · exact no-amplification criterion Self-contained sandwich proof from classical perfect-graph and Lovász-theta facts Evidence and limits → Automata and formal languages Prefix quotients under shuffle Perfect-policy criterion FPRD-SH-T26; Perfect graph theorem; Lovász theta sandwich FPRD corollary from Lovász's perfect-graph theorem (1972) and theta sandwich (1979) Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use perfect-graph recognition as a policy compiler gate before finite-power XCC search. FPRD-SH-X03 Give letter a i a_i a i { i , i + 1 } \{i,i+1\} { i , i + 1 } J ψ = C 5 J_\psi=C_5 J ψ = C 5 Ω ( ψ ) = 2 \Omega(\psi)=2 Ω ( ψ ) = 2 { ( i , 2 i m o d 5 ) : i ∈ Z 5 } \{(i,2i\bmod5):i\in\mathbb Z_5\} {( i , 2 i mod 5 ) : i ∈ Z 5 } Ω ( ψ ⊗ 2 ) = 5 > 4 = Ω ( ψ ) 2 \Omega(\psi^{\otimes2})=5>4=\Omega(\psi)^2 Ω ( ψ ⊗ 2 ) = 5 > 4 = Ω ( ψ ) 2 Ω ∞ ( ψ ) = 5 \Omega_\infty(\psi)=\sqrt5 Ω ∞ ( ψ ) = 5 Exact example · strict support-tensor amplification Explicit five-signature certificate; exact Lovász upper bound Evidence and limits → Automata and formal languages Prefix quotients under shuffle Pentagon policy split FPRD-SH-T25; FPRD-SH-T26; Lovász's pentagon capacity theorem FPRD cyclic-policy translation of Lovász's classical C5 code Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use FPRD-SH-X04 for the expression-level realization; next compile the typed recursive C7 gadget rather than enumerating its output. FPRD-SH-B04 For adjacent-pair supports on seven participants, J ψ = C 7 J_\psi=C_7 J ψ = C 7 Ω ∞ ( ψ ) = Θ ( C 7 ) \Omega_\infty(\psi)=\Theta(C_7) Ω ∞ ( ψ ) = Θ ( C 7 ) C 7 ⊠ 200 C_7^{\boxtimes200} C 7 ⊠ 200 Ω ∞ ( ψ ) ≥ 3.258805369885 … \Omega_\infty(\psi)\ge3.258805369885\ldots Ω ∞ ( ψ ) ≥ 3.258805369885 … 3.3177 3.3177 3.3177 Boundary result · externally anchored support-policy rate Exact policy reduction; current graph-capacity bounds imported from primary sources Evidence and limits → Automata and formal languages Prefix quotients under shuffle Seven-cycle policy boundary FPRD-SH-T26; C7 Shannon-capacity bounds Buys, Polak, and Zuiddam (2026), using Gao's product method Reviewed 2026-09-01 The lower bound is a current preprint; the FPRD automata translation has no external review. Use FPRD-SH-X06/T30 as the compiled five-dimensional base; next test whether residual quotients compose across Gao's typed product DAG without expanding its output. FPRD-SH-T28 Let G = J ψ G=J_\psi G = J ψ π : G → G ‾ \pi:G\to\overline G π : G → G π \pi π 1 + ∣ V ( G ) ∣ 1+|V(G)| 1 + ∣ V ( G ) ∣ { ( v , π ( v ) ) : v ∈ V ( G ) } \{(v,\pi(v)):v\in V(G)\} {( v , π ( v )) : v ∈ V ( G )} G ⊠ 2 G^{\boxtimes2} G ⊠ 2 Theorem · reachable expression compiler Self-contained all-length proof; exhaustive complementing-permutation audit passes Evidence and limits → Automata and formal languages Prefix quotients under shuffle Twisted-section compiler FPRD-SH-T12; FPRD-SH-T14; Self-complementary graphs FPRD expression-level compiler for the classical self-complementary square code Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use self-complementary Paley graphs as further square calibrations; use the separate path compiler FPRD-SH-X06 for C7. FPRD-SH-X04 For the optional-once five-cycle expression, the useful component-prefix product has 11 states and the natural prefix automaton has 16. Synchronizing it with the copy relabelled by i ↦ 2 i ( m o d 5 ) i\mapsto2i\pmod5 i ↦ 2 i ( mod 5 ) { ( i , 2 i ) : i ∈ Z 5 } \{(i,2i):i\in\mathbb Z_5\} {( i , 2 i ) : i ∈ Z 5 } C 5 ⊠ 2 C_5^{\boxtimes2} C 5 ⊠ 2 Exact example · reachable expression-level twisted section Explicit expression, exact state/transition counts, and executable audit Evidence and limits → Automata and formal languages Prefix quotients under shuffle Reachable pentagon twist FPRD-SH-T28; FPRD-SH-X03; FPRD-SH-T12 FPRD reachable realization of Lovász's classical pentagon code Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use this as calibration while defining a nonvacuous succinct-generator resource. FPRD-SH-T29 For D ⊆ A 2 D\subseteq A^2 D ⊆ A 2 D x = { y : ( x , y ) ∈ D } D_x=\{y:(x,y)\in D\} D x = { y : ( x , y ) ∈ D } R ∈ { D x } R\in\{D_x\} R ∈ { D x } r → x p D x r\xrightarrow{x}p_{D_x} r x p D x p R → y r p_R\xrightarrow{y}r p R y r D ∗ D^* D ∗ G G G D D D G ⊠ 2 G^{\boxtimes2} G ⊠ 2 Compiler lemma · exact residual quotient, reversibility, and validity criteria Self-contained proof; exhaustive small-relation audit and corrected standard-alphabet C7 regression pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Reversible two-block compiler FPRD-SH-X04; Partial reversible DFAs; Strong-product independence FPRD compiler lemma calibrated against Meiburg's reversible-capacity construction Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Generalize the distinct-successor-set quotient to the typed five-block compiler and test compositional residual minimization across Gao's product nodes. FPRD-SH-B05 If a classical graph-language L ⊆ V ( G ) ∗ L\subseteq V(G)^* L ⊆ V ( G ) ∗ ρ \rho ρ L ∩ V ( G ) n L\cap V(G)^n L ∩ V ( G ) n G ⊠ n G^{\boxtimes n} G ⊠ n ε > 0 \varepsilon>0 ε > 0 ρ − ε \rho-\varepsilon ρ − ε Calibration boundary · exact slice factorization Definition-level proof; consistent with the primary regular-language capacity framework Evidence and limits → Automata and formal languages Prefix quotients under shuffle No-free-capacity boundary Definition of graph-language growth; Definition of Shannon capacity Direct consequence of Meiburg's graph-language formulation Reviewed 2026-09-01 Meiburg's regular-language framework is peer-reviewed; the FPRD methodological boundary has no documented specialist review. Measure succinctness and verification cost separately from code size; call a capacity result new only when an emitted finite slice improves a published bound. FPRD-SH-C13 The exact audit verifies the one-layer 11/16-state construction, the six-state reachable synchronized square, its five nonrectangular pentagon signatures, the six-state reversible lowering, both compiler criteria over all 530 two-block relations through three symbols, the corrected standard-alphabet six-state C7 residual quotient, 4,130 graph-language checks, and 265 complementing-permutation certificates through five vertices. All checks pass. Computational finding · expression and reversible compiler audit All exact checks pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Expression-twist exact audit FPRD-SH-T28; FPRD-SH-X04; FPRD-SH-T29; Exact enumeration FPRD Lab expression-twist verifier, corrected by the independent result review Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as implementation evidence; use the symbolic proofs for arbitrary graphs and code relations. FPRD-SH-B06 The reachable six-state construction of FPRD-SH-X04 presents each pair ( i , 2 i ) (i,2i) ( i , 2 i ) R 5 = ( a 0 a 0 + a 1 a 2 + a 2 a 4 + a 3 a 1 + a 4 a 3 ) ∗ R_5=(a_0a_0+a_1a_2+a_2a_4+a_3a_1+a_4a_3)^* R 5 = ( a 0 a 0 + a 1 a 2 + a 2 a 4 + a 3 a 1 + a 4 a 3 ) ∗ 2 m 2m 2 m C m C^m C m C = { 00 , 12 , 24 , 31 , 43 } C=\{00,12,24,31,43\} C = { 00 , 12 , 24 , 31 , 43 } Boundary · exact separation of macro-event and path-language realizations Self-contained comparison; the graph language is explicit in the primary automata-capacity literature Evidence and limits → Automata and formal languages Prefix quotients under shuffle Macro-event versus path compiler FPRD-SH-X04; FPRD-SH-T29; Graph languages Meiburg (2025); FPRD comparison with the prefix construction of Broda et al. (2021) Reviewed 2026-09-01 The graph-language construction is peer reviewed; the FPRD prefix comparison has no external review. Fix a resource measure that does not count a hard-coded block expression as an automata-specific capacity improvement. FPRD-SH-X05 For R 5 = ( a 0 a 0 + a 1 a 2 + a 2 a 4 + a 3 a 1 + a 4 a 3 ) ∗ R_5=(a_0a_0+a_1a_2+a_2a_4+a_3a_1+a_4a_3)^* R 5 = ( a 0 a 0 + a 1 a 2 + a 2 a 4 + a 3 a 1 + a 4 a 3 ) ∗ ε \varepsilon ε R 5 a i R_5a_i R 5 a i R 5 a i a 2 i R_5a_i a_{2i} R 5 a i a 2 i ε \varepsilon ε Exact example · natural-prefix-to-reversible-quotient calibration Exact symbolic derivation and independent automaton audit Evidence and limits → Automata and formal languages Prefix quotients under shuffle Eleven-to-six direct block compiler FPRD-SH-B06; The prefix-automaton backward recursion FPRD calculation from Broda et al.'s prefix construction Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Compare natural-prefix and compact-generator size only after fixing a uniform resource model. FPRD-SH-C14 An independent verifier checks all 488,281 alphabet words of lengths zero through eight, all ten pentagon-code pairs, the eleven-state natural prefix automaton, and its minimal six-state reversible quotient. Exactly 781 tested words are accepted. All checks pass. Computational finding · direct-expression audit All exact checks pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Independent direct-expression audit certificate FPRD-SH-B06; FPRD-SH-X05; Exact enumeration FPRD Lab independent direct-block verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as regression evidence for the semantic separation; use symbolic proofs for all lengths. FPRD-SH-X06 The published 367-word independent set in C 7 ⊠ 5 C_7^{\boxtimes5} C 7 ⊠ 5 Exact computational theorem · table-free code compiler Independent reconstruction and exact maximum-set enumeration pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Table-free 367-code compiler Polak--Schrijver cyclic construction; Strong-product independence; Exact maximum-clique search Polak and Schrijver (2019); FPRD reconstruction and extension-graph decomposition Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Treat the generated typed package, rather than a 367-vector input file, as the leaf of Gao's recursive compiler. FPRD-SH-T30 For coordinate order ( 0 , 2 , 3 , 4 , 1 ) (0,2,3,4,1) ( 0 , 2 , 3 , 4 , 1 ) ( 1 , 7 , 49 , 61 , 9 , 1 ) (1,7,49,61,9,1) ( 1 , 7 , 49 , 61 , 9 , 1 ) Theorem · exact residual quotient and finite optimality Myhill--Nerode proof for each order; all 960 extension/order pairs checked exactly Evidence and limits → Automata and formal languages Prefix quotients under shuffle Residual-optimal published extension FPRD-SH-X06; Myhill--Nerode right residuals; Finite coordinate-order exhaustion FPRD residual compiler for the Polak--Schrijver code Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Determine whether Gao's typed product operation admits a residual quotient computed compositionally from child packages. FPRD-SH-C15 A standard-library exact verifier reconstructs the published 367-code without an input table, enumerates all eight maximum 40-word extensions, checks 960 residual compilers, verifies Gao's eight private pairs, complementary transversals, and ( 321 , 26 , 20 ) (321,26,20) ( 321 , 26 , 20 ) M 40 M_{40} M 40 Computational finding · C7 base compiler and recursive-interface audit All exact checks pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle C7 base-compiler audit FPRD-SH-X06; FPRD-SH-T30; Gao's private-pair product lemma; Exact integer arithmetic FPRD C7 compiler audit; Gao (2026), arXiv:2607.27869v1 Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Use the 204-node typed syntax DAG as the next compiler input; do not enumerate its 200-dimensional output. FPRD-SH-X08 Retain the ten fixed-length languages I , B , R , Q , P H , P V , X , O , H , V I,B,R,Q,P^{\mathrm H},P^{\mathrm V},X,O,H,V I , B , R , Q , P H , P V , X , O , H , V M 40 M_{40} M 40 Exact example · resource-preserving typed-language translation Structural induction proved; exact cardinality audit reproduces Gao's M40 Evidence and limits → Automata and formal languages Prefix quotients under shuffle Typed product language compiler FPRD-SH-X06; FPRD-SH-C15; Gao's product lemma; Fixed-length regular-language concatenation FPRD translation of Gao (2026) Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain this resource-preserving translation as the input for any later semantic minimization or comparison. FPRD-SH-C16 Exact Brzozowski-derivative closure of the 204-node typed expression DAG yields a deterministic partial path compiler with 192,771 192{,}771 192 , 771 618,415 618{,}415 618 , 415 M 40 M_{40} M 40 C 7 ⊠ 200 C_7^{\boxtimes200} C 7 ⊠ 200 Computational finding · exact canonical syntax-compiler profile Complete canonical syntactic derivative closure; deterministic rerun and independent two-block semantic audit pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Two-hundred-dimensional symbolic compiler audit FPRD-SH-X08; Brzozowski derivatives; Hash-consed regular-expression DAGs FPRD typed-language compiler and independent semantic audit Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as exact implementation evidence; do not spend another run minimizing a presentation of the known Gao code. FPRD-SH-B08 The table-free base reconstruction, constant-template product DAG, and 192,771-state canonical symbolic lowering give a complete path-language presentation of Gao's known 200-dimensional code. They do not improve Θ ( C 7 ) \Theta(C_7) Θ ( C 7 ) Boundary result · research-line closure Exact scope boundary recorded Evidence and limits → Automata and formal languages Prefix quotients under shuffle C7 compiler stopping boundary FPRD-SH-X08; FPRD-SH-C16; Current C7 capacity bounds FPRD scope audit against Gao and Buys--Polak--Zuiddam Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Study exact XCC algorithms parameterized by support-family diversity. FPRD-SH-C10 Exact enumeration checks 16,384 signature subsets for XCC compatibility and 1,355 graphs for the one-shot product correspondence, weighted matching formula, and isolated-edge recovery identity. All 21,152 matching receipts and useful product states agree with the theorems. Computational finding · compiler and reduction audit Source replay and independent implementation pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Dancing Links and matching audit FPRD-SH-T19; FPRD-SH-T20; FPRD-SH-T21; Exact enumeration FPRD Lab XCC and one-shot matching verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as implementation evidence; use the symbolic proofs for arbitrary policies and graphs. FPRD-SH-C09 Exact enumeration checks 65,536 target-set families, 2,924 one-support policies with 28,856 signature intersections, and 3,905 pure-shuffle state-count vectors comprising 809,710 noninitial product states. All collision identities, matching boundaries, closed formulas, and clique-bound gaps agree. Computational finding · theorem and boundary audit Source audit and independent complete-domain replay pass; strict-gap scope corrected Evidence and limits → Automata and formal languages Prefix quotients under shuffle Global-overhead exact audit FPRD-SH-T17; FPRD-SH-T18; Exact finite enumeration FPRD Lab global-overhead verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as implementation evidence; use the symbolic proofs for arbitrary sizes. FPRD-SH-C08 Exact enumeration checks 16,452 two-letter support policies through arity three against every homogeneous unused, a ∗ a^* a ∗ b ∗ b^* b ∗ 2 × 2 × 2 2\times2\times2 2 × 2 × 2 Computational finding · theorem and reduction audit Source audit and independent complete-domain replay pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Compatibility and matching audit FPRD-SH-T15; FPRD-SH-T16; Exact clique and matching enumeration FPRD Lab signature-compatibility verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as an implementation audit; use the symbolic proofs for arbitrary arity. FPRD-SH-C07 The source enumeration checks 16,448 two-letter support policies at arities two and three, 11,736 rigid-policy/component combinations, 16,382 non-rigid starred witnesses, and 16,448 signature-expansion projections. An independent review covers all 16,452 policies at arities one through three and checks 172,128 same-letter support-pair occurrences at the unmarked boundary. Full synchronization and the pairwise-intersecting support triangle pass; pure shuffle fails uniqueness. Computational finding · theorem audit Source audit and independent complete small-policy review pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Prefix-rigidity exact audit FPRD-SH-T12; FPRD-SH-T14; Exact homogeneous product constructor FPRD Lab Boolean-product prefix-rigidity verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain as an implementation audit; use the symbolic proof for arbitrary arity. FPRD-SH-C06 Exact enumeration checks 8,192 combinations of two-state one-letter transition structures, all eight Boolean policies on the supports { 1 } , { 2 } , { 1 , 2 } \{1\},\{2\},\{1,2\} { 1 } , { 2 } , { 1 , 2 } Computational finding · theorem audit Source transition audit and independent initial/final boundary audit pass Evidence and limits → Automata and formal languages Prefix quotients under shuffle Boolean-product exact audit FPRD-SH-T11; Exact Boolean-product constructor FPRD Lab Boolean-product quotient verifier Reviewed 2026-09-01 No documented external or specialist review of these FPRD results is recorded. Retain this as an implementation audit; use the all-arity proof for the theorem. FPRD-RE-D01 For a regular expression B B B Q B Q_B Q B B B B Definition · finite construction Classical construction stated for the quotient proof Evidence and limits → Automata and formal languages Regular expressions and quotients Finite derivative carrier Antimirov partial derivatives Antimirov (1996) finiteness theorem; FPRD construction for Zhuchko's problem Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Make the carrier construction fully explicit in a mechanized implementation. FPRD-RE-L01 Interpreting 0 , 1 0,1 0 , 1 Q B Q_B Q B ( P , Q ) ∈ ⟦ A ⟧ B (P,Q)\in\llbracket A\rrbracket_B ( P , Q ) ∈ [ [ A ] ] B u ∈ L ( A ) u\in L(A) u ∈ L ( A ) Q ∈ ∂ u ( P ) Q\in\partial_u(P) Q ∈ ∂ u ( P ) Lemma Proved by structural induction Evidence and limits → Automata and formal languages Regular expressions and quotients Relational semantics lemma FPRD-RE-D01 Problem proposed by Ekaterina Zhuchko; FPRD Lab construction Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Obtain an independent check of the star case and its finite path bound. FPRD-RE-T01 For regular expressions A , B A,B A , B Q ∈ Q B Q\in Q_B Q ∈ Q B B B B ⟦ A ⟧ B \llbracket A\rrbracket_B [ [ A ] ] B f ( A , B ) f(A,B) f ( A , B ) L ( f ( A , B ) ) = L ( A ) − 1 L ( B ) = { v : ∃ u ∈ L ( A ) , u v ∈ L ( B ) } L(f(A,B))=L(A)^{-1}L(B)=\{v:\exists u\in L(A),\ uv\in L(B)\} L ( f ( A , B )) = L ( A ) − 1 L ( B ) = { v : ∃ u ∈ L ( A ) , uv ∈ L ( B )} Theorem · constructive solution Proved under the finite-derivative interpretation of the requested construction Evidence and limits → Automata and formal languages Regular expressions and quotients Construction and correctness proof FPRD-RE-D01; FPRD-RE-L01 Problem proposed by Ekaterina Zhuchko; FPRD Lab construction Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Determine whether the finite carrier and relation saturation can be compiled away under the pinned model FPRD-RE-D02. FPRD-RE-C01 On 405 selected binary regular-expression pairs and all 31 suffixes of length at most four, three saved automata formulations agree in all 12,555 12{,}555 12 , 555 Computational finding · reproducible finite audit Reproduced by three saved checks; zero ordinary mismatches, identical semantic transcripts, four named negative controls detected, and 65 hostile star cases confirmed Evidence and limits → Automata and formal languages Regular expressions and quotients Finite audit and downloadable evidence FPRD-RE-D01; FPRD-RE-L01; FPRD-RE-T01 FPRD Lab replacement finite audit Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Use the exact unbounded star family as the next adversary rather than continuing to enlarge this bounded corpus. FPRD-RE-D02 A carrier-free constructor-only quotient compiler recurses on ordinary regular-expression constructors and returns an ordinary regular expression, without enumerating a residual carrier, saturating a finite relation, or adding an explicit least-fixed-point constructor. Definition attempt · strengthened construction discipline Informal exclusion-based discipline; a formal compiler class is still missing Evidence and limits → Automata and formal languages Regular expressions and quotients Constructor-only formulation boundary FPRD-RE-T01 FPRD Lab formulation attempt for a stricter construction discipline Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Specify an admissible compiler grammar, auxiliary-state policy, and equivalence/cost model before testing general existence or impossibility. FPRD-RE-T02 For languages K , L K,L K , L Q ( K ∗ , L ) Q(K^*,L) Q ( K ∗ , L ) Φ K , L ( X ) = L ∪ Q ( K , X ) \Phi_{K,L}(X)=L\cup Q(K,X) Φ K , L ( X ) = L ∪ Q ( K , X ) Q ( K ∗ , L ) = ⋃ n ≥ 0 Q ( K n , L ) Q(K^*,L)=\bigcup_{n\ge0}Q(K^n,L) Q ( K ∗ , L ) = ⋃ n ≥ 0 Q ( K n , L ) L L L Theorem · presentation-dynamics decomposition Proved directly from left-quotient composition Evidence and limits → Automata and formal languages Regular expressions and quotients Fixed-point theorem and proof FPRD-RE-L01; FPRD-RE-T01 Elementary language-theoretic deduction; FPRD presentation-dynamics formulation Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Determine whether the finite star-orbit closure can be compiled uniformly into the stricter model FPRD-RE-D02. FPRD-RE-X01 For every k ≥ 0 k\ge0 k ≥ 0 ε ∈ ( a ∗ ) − 1 { a k + 1 } \varepsilon\in(a^*)^{-1}\{a^{k+1}\} ε ∈ ( a ∗ ) − 1 { a k + 1 } ε ∉ ⋃ i = 0 k { a i } − 1 { a k + 1 } \varepsilon\notin\bigcup_{i=0}^{k}\{a^i\}^{-1}\{a^{k+1}\} ε ∈ / ⋃ i = 0 k { a i } − 1 { a k + 1 } Negative theorem · counterexample family Proved by an explicit unary family Evidence and limits → Automata and formal languages Regular expressions and quotients Unbounded-unfolding proof FPRD-RE-T02 FPRD Lab direct counterexample family Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Use this family as the first adversary for any proposed carrier-free star compiler; seek a broader lower bound only after its formal interface is pinned. FPRD-RE-B01 Uniformly bounded star unfolding is impossible and finite derivative saturation is sufficient. A broader carrier-free existence question has not yet been posed as a formal mathematical problem because FPRD-RE-D02 does not define a quantified compiler class. Unresolved formalization boundary Not yet a well-posed existence or impossibility problem Evidence and limits → Automata and formal languages Regular expressions and quotients Interpretation boundary FPRD-RE-D02; FPRD-RE-T02; FPRD-RE-X01 FPRD Lab strengthened formulation boundary, motivated by the Automata Exchange question Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Specify an admissible compiler grammar, auxiliary-state policy, and equivalence/cost model before seeking a carrier-elimination theorem or lower bound. FPRD-LT-D01 Given a minimal DFA whose transition monoid M ≤ T Q M\le T_Q M ≤ T Q L \mathcal L L f : Q → Q f:Q\to Q f : Q → Q f ∈ M f\in M f ∈ M Definition · decision problem Precisely stated; exact complexity remains open here Evidence and limits → Automata and formal languages L-trivial transformation membership Problem statement and conventions No recorded dependencies Problem proposed by Andrew Ryzhikov; FPRD Lab analysis Reviewed 2026-08-25 No documented external or specialist review of this FPRD result is recorded. Determine whether positive instances always admit polynomial-length word witnesses in the supplied transformation action. FPRD-LT-L01 For M = ⟨ τ a : a ∈ Σ ⟩ M=\langle\tau_a:a\in\Sigma\rangle M = ⟨ τ a : a ∈ Σ ⟩ f f f M M M M o p M^{\mathrm{op}} M op L \mathcal L L M M M R \mathcal R R M o p M^{\mathrm{op}} M op Lemma · algebraic duality Proved directly from opposite multiplication Evidence and limits → Automata and formal languages L-trivial transformation membership Opposite multiplication and proof FPRD-LT-D01 Problem proposed by Andrew Ryzhikov; FPRD Lab analysis Reviewed 2026-08-25 No documented external or specialist review of this FPRD result is recorded. Use the duality only together with an explicit size analysis of any representation of the opposite monoid. FPRD-LT-T01 If an n n n ρ : M o p ↪ T P \rho:M^{\mathrm{op}}\hookrightarrow T_P ρ : M op ↪ T P t f t_f t f ρ ( f ) \rho(f) ρ ( f ) ρ ( M ) \rho(M) ρ ( M ) ∣ P ∣ ( ∣ P ∣ + 1 ) / 2 |P|(|P|+1)/2 ∣ P ∣ ( ∣ P ∣ + 1 ) /2 Theorem · conditional complexity transfer Proved conditionally; the compact dual representation is not known in general Evidence and limits → Automata and formal languages L-trivial transformation membership Conditional NP theorem FPRD-LT-L01; Ryzhikov–Wolf 2024, Proposition 9 FPRD Lab conditional transfer using Ryzhikov–Wolf 2024, Proposition 9 Reviewed 2026-08-25 The poDFA representative bound is a published MFCS 2024 result; no external review of this conditional FPRD transfer is recorded. Construct a polynomial-degree faithful action of the opposite monoid or prove that no uniform construction exists. FPRD-LT-T02 Let M = ⟨ S ⟩ M=\langle S\rangle M = ⟨ S ⟩ f : Q → Q f:Q\to Q f : Q → Q ρ : M o p → T P \rho:M^{\mathrm{op}}\to T_P ρ : M op → T P t f ∈ T P t_f\in T_P t f ∈ T P g ∈ M g\in M g ∈ M ρ ( g ) = t f \rho(g)=t_f ρ ( g ) = t f g = f g=f g = f ρ \rho ρ Theorem · conditional quotient transfer Proved conditionally; a uniform compact target-isolating construction remains open Evidence and limits → Automata and formal languages L-trivial transformation membership Target-fibre theorem and proof FPRD-LT-L01; Ryzhikov–Wolf 2024, Proposition 9 FPRD Lab conditional theorem using Ryzhikov–Wolf 2024, Proposition 9 Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Construct target-isolating poDFA observations directly from the supplied L-trivial action, beginning with fixed alphabets and principal-left-ideal features. FPRD-LT-X01 For the L-trivial monoid M = { 1 , a , 0 } M=\{1,a,0\} M = { 1 , a , 0 } a 2 = 0 a^2=0 a 2 = 0 f = 1 f=1 f = 1 a a a 0 0 0 Example · strict quotient compression Proved by a complete multiplication-table and action check Evidence and limits → Automata and formal languages L-trivial transformation membership Three-element monoid example FPRD-LT-T02 FPRD Lab exact example Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Search for canonical target-isolating congruences that retain poDFA order while collapsing large non-target regions. FPRD-LT-C01 The minimal two-state DFA for words ending in a a a { 1 , c 0 , c 1 } \{1,c_0,c_1\} { 1 , c 0 , c 1 } Counterexample · failed reduction Proved by an explicit two-state example Evidence and limits → Automata and formal languages L-trivial transformation membership Two-state reversal counterexample FPRD-LT-D01 Problem proposed by Andrew Ryzhikov; FPRD Lab counterexample Reviewed 2026-08-25 No documented external or specialist review of this FPRD result is recorded. Exclude graph reversal and matrix transposition from future dual-representation arguments unless functionality and order are proved. FPRD-LT-E01 Exhaustive enumeration of unordered pairs of distinct transformations on n = 2 , 3 , 4 n=2,3,4 n = 2 , 3 , 4 1 , 2 , 3 1,2,3 1 , 2 , 3 Computational finding Finite exhaustive evidence through four states; the inferred pattern is refuted at five states Evidence and limits → Automata and formal languages L-trivial transformation membership Enumeration method and results FPRD-LT-D01 FPRD Lab finite enumeration Reviewed 2026-08-25 No documented external or specialist review of this FPRD result is recorded. Retain these counts as the completed four-state baseline; use FPRD-LT-E02 for the five-state classification. FPRD-LT-T03 For every n ≥ 5, there is a minimal binary n-state DFA with J-trivial transition monoid and a target transformation whose shortest representative has length exactly n. Thus the conjectured n − 1 bound for binary L-trivial inputs is false already inside the J-trivial subclass. Theorem · exact witness family Self-contained construction and proof; no external review Evidence and limits → Automata and formal languages L-trivial transformation membership Binary family and exact lower bound Masopust–Krötzsch 2021, confluent-poDFA characterization; Simon 1975, piecewise testability iff J-trivial syntactic monoid FPRD Lab construction using the Masopust–Krötzsch and Simon characterizations Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Seek a polynomial upper bound for fixed binary alphabets or a family with superpolynomial shortest representatives; the linear lower bound alone does not settle complexity. FPRD-LT-E02 Among binary five-state semiautomata with L-trivial transition monoid that admit a minimal-DFA final set, exhaustive enumeration finds maximum shortest-word diameter 5. Up to state relabelling fixing the initial state and interchange of the two letters, there are 1,148 retained generator-pair classes and exactly three extremal classes. Computational finding · exhaustive classification Exact finite computation with an independent extremal audit Evidence and limits → Automata and formal languages L-trivial transformation membership Five-state exhaustive classification FPRD-LT-D01 FPRD Lab exact enumeration Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Use the explicit family in FPRD-LT-T03 as the corrected lower-bound baseline; do not infer a general upper bound from five states. FPRD-LT-X02 For the 14-element five-state extremal generated by a=(2,1,2,3,1) and b=(0,1,3,4,4), minimizing the left-Cayley poDFA with sole accepting element f=(4,1,1,1,1) gives a nine-state poDFA action whose transformation fibre over f is exactly {f}. Example · exact target-isolating quotient Proved by exact partition refinement and fibre audit Evidence and limits → Automata and formal languages L-trivial transformation membership Nine-state extremal quotient FPRD-LT-T02; FPRD-LT-E02 FPRD Lab exact extremal analysis Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Find a quotient construction whose state space and fibre proof are obtained directly from the supplied n-state action rather than from the enumerated monoid. FPRD-LT-T04 For f ∈ M = η ( Σ ∗ ) f\in M=\eta(\Sigma^*) f ∈ M = η ( Σ ∗ ) P f ( x ) = { z ∈ M : z x = f } P_f(x)=\{z\in M:zx=f\} P f ( x ) = { z ∈ M : z x = f } d f = ∣ { P f ( x ) : x ∈ M } ∣ d_f=|\{P_f(x):x\in M\}| d f = ∣ { P f ( x ) : x ∈ M } ∣ K f = { w R : η ( w ) = f } K_f=\{w^R:\eta(w)=f\} K f = { w R : η ( w ) = f } d f d_f d f M M M d f − 1 d_f-1 d f − 1 Theorem · canonical target observer Self-contained Myhill–Nerode proof; no external review Evidence and limits → Automata and formal languages L-trivial transformation membership Canonical observer and path bound FPRD-LT-L01; Myhill–Nerode theorem; R-trivial language characterization FPRD Lab target-specific synthesis using classical automata theory Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Determine whether target-residual degree is polynomially bounded in the degree of every supplied L-trivial transformation action. FPRD-LT-T05 For the binary J-trivial family of FPRD-LT-T03, the source transition monoid has exactly ∣ M n ∣ = ( n 3 ) + n − 1 |M_n|=\binom n3+n-1 ∣ M n ∣ = ( 3 n ) + n − 1 f n = ( n − 1 , 1 , … , 1 ) f_n=(n-1,1,\ldots,1) f n = ( n − 1 , 1 , … , 1 ) d f n = ( n 2 ) − 1 d_{f_n}=\binom n2-1 d f n = ( 2 n ) − 1 Theorem · exact quotient family Self-contained normal-form and residual proof with exact computational audits Evidence and limits → Automata and formal languages L-trivial transformation membership Exact monoid and observer formulas FPRD-LT-T03; FPRD-LT-T04 FPRD Lab exact analysis of the binary lower-bound family Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Generalize the fibre classification or construct an L-trivial family with superpolynomially many target profiles. FPRD-LT-C02 Among all 32,896 unordered transformation-generator pairs on four states, 4,473 generate L-trivial monoids. Their maximum left-Cayley height is 6, while the maximum shortest right-Cayley distance of any target across the same search is 3; ideal height is therefore a strict overestimate of target certificate length. Counterexample · complexity proxy Exact finite computation; semigroup control rather than a minimal-DFA classification Evidence and limits → Automata and formal languages L-trivial transformation membership Four-state Green-height control FPRD-LT-D01 FPRD Lab exhaustive four-state semigroup computation Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Use extension-distinguishable target profiles or actual target geodesics rather than principal-ideal height as the obstruction measure. FPRD-LT-B01 It remains open whether every positive L-trivial transformation-membership instance has a polynomial-length word witness in the degree of the supplied action. The canonical target-residual degree d_f gives a witness of length at most d_f−1; whether d_f is always polynomial is the current sufficient-bound question. Open problem · representation boundary Unresolved; the n-minus-one conjecture is refuted, but neither NP membership nor PSPACE hardness is established Evidence and limits → Automata and formal languages L-trivial transformation membership What remains open FPRD-LT-T04; FPRD-LT-T05; FPRD-LT-C02; FPRD-LT-T03; FPRD-LT-E02 Problem proposed by Andrew Ryzhikov; FPRD Lab boundary analysis Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Prove a polynomial upper bound on target-residual degree from L-trivial fibre evolution, or construct a structured superpolynomial target-profile or geodesic family. FPRD-LRN-D01 For F ( q ) = ∑ n ≥ 0 a n q n ∈ Q [ [ q ] ] F(q)=\sum_{n\ge0}a_nq^n\in\mathbb Q[[q]] F ( q ) = ∑ n ≥ 0 a n q n ∈ Q [[ q ]] a 0 , … , a N − 1 a_0,\ldots,a_{N-1} a 0 , … , a N − 1 P t P_t P t ∀ n ∃ T n ∀ t ≥ T n : [ q n ] P t = a n \forall n\,\exists T_n\,\forall t\ge T_n:[q^n]P_t=a_n ∀ n ∃ T n ∀ t ≥ T n : [ q n ] P t = a n Definition · observation models Precisely stated; the two models have different learnability Evidence and limits → Automata and formal languages Learning rational sequences Observation models No recorded dependencies Problem proposed by Benjamin Kaminski; FPRD Lab model analysis Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Determine which observation model is supplied by the probabilistic-program application motivating the revisable examples. FPRD-LRN-T01 A rational series of positive Hankel rank r r r 2 r 2r 2 r R ≥ r R\ge r R ≥ r 2 R 2R 2 R Theorem · exact learning Classical recurrence reconstruction, restated and proved for this model Evidence and limits → Automata and formal languages Learning rational sequences Exact-prefix theorem FPRD-LRN-D01; Massey 1969 shift-register synthesis; Berstel–Reutenauer 2010 Hankel minimization James L. Massey (1969); Jean Berstel and Christophe Reutenauer (2010); FPRD sharpness proof Reviewed 2026-09-01 The recurrence-reconstruction theorem is classical; no external review of this FPRD exposition is recorded. Quantify coefficient bit growth for the intended application and add a certified-prefix extractor if its approximants provide one. FPRD-LRN-C01 After any prefix through degree N − 1 N-1 N − 1 F ( q ) F(q) F ( q ) F ( q ) + c q N / ( 1 − λ q ) F(q)+cq^N/(1-\lambda q) F ( q ) + c q N / ( 1 − λ q ) c ≠ 0 c\ne0 c = 0 Counterexample · finite identifiability Proved by an explicit rational tail Evidence and limits → Automata and formal languages Learning rational sequences Rational-tail indistinguishability FPRD-LRN-D01 Problem proposed by Benjamin Kaminski; FPRD Lab boundary proof Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Identify a usable rank bound, equivalence query, or finality certificate in the intended application. FPRD-LRN-T02 No learner identifies every rational target in the limit from arbitrary polynomial snapshots P t P_t P t q k q^k q k Theorem · impossibility Proved by a diagonal presentation Evidence and limits → Automata and formal languages Learning rational sequences Diagonal impossibility theorem FPRD-LRN-D01 Problem proposed by Benjamin Kaminski; FPRD Lab diagonal argument Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Test the intended approximation semantics for a computable stabilization modulus, finality markers, monotone bounds, or active validation. FPRD-LRN-B01 A positive exact-learning theorem for revisable polynomial approximants requires more than pointwise stabilization, such as a computable stabilization modulus, finality markers, certified monotone bounds with an effective gap test, a detectable revision bound, or active coefficient and equivalence queries. Research boundary Necessary direction isolated; application semantics remain unknown Evidence and limits → Automata and formal languages Learning rational sequences What would make learning possible FPRD-LRN-T02 Problem proposed by Benjamin Kaminski; FPRD Lab boundary analysis Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Recover the semantics of the probabilistic-program approximants and state the strongest available certificate before designing a learner. FPRD-T96 A causal resolver emits one call, return, or local tag in the same round as each observed input letter. Its one-stack product with a deterministic visible-stack machine has exactly the resolver state and tagged-machine configuration after every prefix. A fixed finite family of such products executes on parallel stacks and accepts exactly their finite disjunction. If the family is complete for every accepted tagged lift, its executor and the scaffold produced by the verified compiler decide exactly the forgotten-action projection, including at epsilon. Mechanically checked result mechanically checked Evidence and limits → Automata and formal languages Formal languages and scaffolding automata formalizations/frontier-derivative/FrontierDerivative/ResolverCover.lean FPRD-T89 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Expose the formal/checker scope, reproducibility instructions, and the gap to a complete mathematical proof. FPRD-T98 A finalizable delayed resolver emits append-only online tagged batches and an explicit finish batch at end of word. Its semantic visible-stack evaluator has exactly the resolver state and direct visible run on the online output after every prefix, and after finish it has exactly the direct run on the completed annotation. A lawful fixed finite Complete Cover therefore recognizes exactly the forgotten-action projection, including at epsilon. This theorem does not invoke the strict compiler. Mechanically checked result mechanically checked Evidence and limits → Automata and formal languages Formal languages and scaffolding automata formalizations/frontier-derivative/FrontierDerivative/DelayedResolver.lean FPRD-T96 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Expose the formal/checker scope, reproducibility instructions, and the gap to a complete mathematical proof. FPRD-T18 For every finite conventional context-free grammar G, nonterminal A, and input word w, the least relational suffix behavior of the canonical translation returns exactly the suffixes v for which A derives a terminal prefix x with w=xv; consequently complete-match observation of the translated start variable is exactly the classical language of G. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D07; FPRD-D09; FPRD-T14; FPRD-T15 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T19 The canonical labeled translation of every finite conventional context-free grammar generates an M12 compact relational recognition dynamic reconstructed from its finite reachable graph shadows, and the complete-match call observation at its distinguished initial state is exactly the grammar's classical language. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D08; FPRD-D09; FPRD-T16; FPRD-T17; FPRD-T18 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T20 Every finite positive relational presentation has a finite conventional CFG word normal form whose translated equation operator agrees in every environment, hence whose finite stages, exact and bounded least suffix solutions, and complete-match language agree exactly; together with the M13 lift, the complete-match languages of finite positive relational presentations are exactly the context-free languages. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D07; FPRD-D09; FPRD-D10; FPRD-T14; FPRD-T15; FPRD-T18 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T21 For every labeled positive relational presentation, distributive CFG normalization induces a finite origin relation on call occurrences, and at every exact and bounded observation level each normalization-surviving source right-success frame behavior is the relational union of the frame behaviors of its normalized call clones; split, merge, and elimination witnesses show that raw presentation dynamics need not be invariant. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D03; FPRD-D08; FPRD-D10; FPRD-T15; FPRD-T16; FPRD-T20 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T22 A language is regular exactly when its residual recognition dynamic is finite; in that case residual actions and empty-word output recognize it exactly, every reachable deterministic recognizer maps uniquely and surjectively onto the residual dynamic by accepted-future language, and the residual dynamic is the unique minimal exact recognizer up to labeled isomorphism, recovered after finite bounded observational refinement. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D02; FPRD-D12 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T23 For languages A and B with positive minimum word length m in A, the operator F(X)=AX union B is at most 2-to-the-minus-m contractive in the shortest-distinguishing-word ultrametric, has the unique fixed point A-star B, and its finite unfoldings become exact on bounded words; under the suffix-recognition lift the same fixed point solves the corresponding relational composition-and-union equation with exact remaining-suffix and complete-match readout. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D06; FPRD-D11; FPRD-T13 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T24 Every finite Greibach recognition presentation induces one-half contractive operators on the finite products of exact language behaviors and full set-valued suffix behaviors; both have unique fixed points, bottom unfoldings at depth N plus one are exact on words and input rows through length N, the vector suffix lift identifies the two solutions, and their readout equals ordinary finite CFG derivability. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D02; FPRD-D06; FPRD-D11; FPRD-D13; FPRD-T13; FPRD-T14; FPRD-T15; FPRD-T18; FPRD-T23 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T25 A language is context-free exactly when it is the complete-match observation of the unique suffix fixed point of a finite Greibach recognition presentation; thus every context-free language has a finite terminal-delayed presentation with coherent exact bounded observations and uniform remaining-suffix readout. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D09; FPRD-D13; FPRD-T18; FPRD-T24 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T26 For a finite cycle-guarded positive relational presentation with r variables, the occurrence-delay matrix bounds componentwise semantic first differences by min-plus multiplication, some power p at most r of the exact suffix operator is one-half contractive, the original operator has a unique fixed point, and bottom depth p times N plus one is exact on all input rows through length N with coherent inverse-limit recovery. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D02; FPRD-D06; FPRD-D14; FPRD-T13 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T27 For every finite cycle-guarded positive relational presentation, the unique contractive-iterate fixed point is its M11 least fixed point and finite-derivation semantics, its bounded suffix and complete-match readouts are exact by the certified block depth, and its labeled M12 continuation actions are evaluated in that same uniquely determined behavior vector. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D07; FPRD-D08; FPRD-D14; FPRD-T14; FPRD-T15; FPRD-T16; FPRD-T26 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T28 Every finite generalized Dyck-control presentation has a finite positive state-pair suffix equation system whose components recognize exactly the well-nested traces carrying the selected DFA between their endpoint states; every recursive dependency has positive delay, so the system has one exact suffix solution recovered at depth N plus one through trace length N, and letter-to-letter decoding gives exact remaining-suffix behavior on the output alphabet with the same bounded observation index. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D15; FPRD-T18; FPRD-T22; FPRD-T26; FPRD-T27 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T29 For every nonempty finite output alphabet Sigma there are one finite generalized Dyck alphabet and one fixed letter-to-letter readout, depending only on Sigma, such that the exact suffix behaviors of context-free languages over Sigma are precisely the decoded observations obtained by varying a finite regular controller; every such observation is coherently reconstructed from the controller-product's finite shadows. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D15; FPRD-T25; FPRD-T28 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T30 Every capacity-witnessed fixed-envelope recoding induces a constant length injective homomorphism tau that sends each matching source pair to reversed matching envelope blocks, preserves and reflects Dyck membership on encoded words, and commutes with the fixed projection readout; for every source trace language K, direct block readout of K and fixed projection readout of tau of K have identical exact suffix behaviors, and whenever source languages K and H agree through floor of N over m, their decoded output suffix behaviors agree through length N. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D16 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T31 For every finite complete source controller, the fixed-envelope recoder constructs a finite complete deterministic trie controller recognizing exactly its tau image, sending malformed blocks and unused envelope symbols to a rejecting sink; intersection with envelope Dyck geometry then equals the tau image of the source Dyck-control intersection, so the abstract M18 theorem supplies one exact decoded suffix dynamic with same-index envelope reconstruction and the block-scaled source observation modulus, while every instance admitted by an explicit finite one-character codec is conjugately realized by the executable M18 implementation. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D16; FPRD-T28; FPRD-T30 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T32 For every injective width-m block code and finite complete source controller, the compiled boundary macro-actions are conjugate to the source actions, the right language at each boundary is exactly the code image of the corresponding source right language, and source residual equality is equivalent to boundary residual equality; bounded future-language and full suffix-lift partitions correspond exactly by N maps to floor of N over m, shortest distinguishing lengths multiply by m, and the source residual dynamic embeds into the image residual dynamic under the encoded macro-actions. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D17; FPRD-T22; FPRD-T31 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T33 The fixed-block compiler allocates exactly one sink plus one boundary and one state for every distinct nonempty proper code prefix at every source state, has the corresponding exact reachable-state and transition counts, transports every surjective source-controller quotient functorially, and preserves source residual count as a lower bound on image residual count; for the fixed envelope, q at most j to the m is exactly the positional-code capacity condition, yielding explicit minimal width or base, envelope-size, trie-overhead, residual, and observation-lag coordinates. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata OPEN_PROBLEMS.md FPRD-D17; FPRD-T22; FPRD-T31; FPRD-T32 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T95 If the source and cover carriers of an FPRD-T94 stationary principal derivative cover are finite and its frontier language is X, then X reversed belongs to PEL. Equivalently, to obtain a PEG for L by this route, construct the finite stationary cover for L reversed. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/notes/stationary-principal-derivative-cover-proof.md FPRD-T94 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T97 Let a deterministic visible-stack language have a complete family of a fixed positive finite number of causal resolvers. If the input, visible control, stack alphabet, resolver control, and family are finite, and X is the resulting forgotten-action projection, then X reversed belongs to PEL. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/notes/finite-causal-resolver-cover-proof.md FPRD-T96 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-T99 Let a deterministic visible-stack language have a complete family of a fixed positive finite number of lawful finalizable delayed resolvers, with finite input, visible-control, stack, resolver-control, and family carriers. Each branch has a deterministic PDA realization: a right endmarker may drain finish explicitly, and a finite augmented top-window construction eliminates that marker by predicting the same final readout. The projected language is therefore a finite union of DCFLs and belongs to PEL by Rubtsov--Chudinov Theorem 10, with complete-match semantics and no reversal. Written-proof claim informal proof Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/notes/finalizable-delayed-resolver-cover-proof.md FPRD-T98 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Audit the proof against its dependencies and publish a self-contained evidence summary before increasing maturity. FPRD-D09 A finite conventional context-free grammar has finite disjoint terminal and nonterminal sets, finitely many productions, and a distinguished start nonterminal; its canonical relational translation maps terminals to relational terminal actions, nonterminal occurrences to uniquely labeled calls, concatenation to sequence, alternatives to commutative union, epsilon to identity, and an absent production set to failure. Definition definition Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/specs/m13-cfg-relational-lift.md FPRD-D03; FPRD-D07; FPRD-D08 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Add a self-contained definition page with examples, nonexamples, and dependency boundaries. FPRD-D10 The finite distributive word normal form of a positive relational term maps failure to no words, identity to the empty word, terminals and calls to singleton words, union to finite set union, and sequence to finite word concatenation; for labeled presentations, an annotated enrichment records the finite origin relation from canonical normalized call occurrences to source call labels. Definition definition Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/specs/m14-cfg-normal-form.md FPRD-D03; FPRD-D07; FPRD-D08; FPRD-D09 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Add a self-contained definition page with examples, nonexamples, and dependency boundaries. FPRD-D11 The suffix-recognition lift Lambda maps a language L to the set-valued suffix behavior that returns every v for which the input factors as xv with x in L; complete-match readout recovers L, and the lift is intended to preserve empty language, epsilon, union, and language concatenation as relational failure, identity, union, and composition. Definition definition Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/specs/m15-classical-regular-dynamics.md FPRD-D01; FPRD-D02; FPRD-D06 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Add a self-contained definition page with examples, nonexamples, and dependency boundaries. FPRD-D12 The residual recognition dynamic of a language L has the left residuals u-inverse L as states, one-letter left differentiation as its named input actions, L as its distinguished state, empty-word membership as output, and agreement on continuations of length at most N as its bounded observational equivalence. Definition definition Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/specs/m15-classical-regular-dynamics.md FPRD-D01; FPRD-D02; FPRD-D11 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Add a self-contained definition page with examples, nonexamples, and dependency boundaries. FPRD-D13 A finite Greibach recognition presentation is the canonical labeled relational translation of a finite context-free grammar whose productions have the form A to terminal-a followed by a finite word of nonterminals, or A to epsilon; it retains the finite language and suffix equation operators, labeled call-context actions, bounded restrictions, and remaining-suffix and complete-match readouts. Definition definition Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/specs/m16-greibach-recognition-dynamics.md FPRD-D06; FPRD-D07; FPRD-D08; FPRD-D09; FPRD-D11 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Add a self-contained definition page with examples, nonexamples, and dependency boundaries. FPRD-D14 The delay profile of a finite positive relational recognition presentation assigns each variable occurrence its guaranteed consumed prefix length, collects the minima in a min-plus dependency matrix, and calls the presentation cycle-guarded when its zero-delay dependency graph is acyclic, equivalently when every dependency cycle has positive total delay. Definition definition Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/specs/m17-delay-graph-guardedness.md FPRD-D02; FPRD-D06; FPRD-D07 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Add a self-contained definition page with examples, nonexamples, and dependency boundaries. FPRD-D15 A generalized Dyck-control recognition presentation consists of a finite alphabet of matching brackets and neutral symbols, a finite complete DFA on that alphabet, the finite state-pair equation system recognizing well-nested DFA runs, a distinguished union over final states, and a total letter-to-letter map whose decoded observation returns every suffix remaining after an encoded trace prefix. Definition definition Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/specs/m18-universal-dyck-control.md FPRD-D06; FPRD-D09; FPRD-D11; FPRD-D12; FPRD-D14 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Add a self-contained definition page with examples, nonexamples, and dependency boundaries. FPRD-D16 A capacity-witnessed fixed-envelope recoding consists of a nonempty finite output alphabet Sigma, a positive block width m, a base j at least two, a finite matched source-bracket alphabet with at most j to the m pair types, one m-letter output block for each source bracket, and one distinct m-digit code for each matched pair; its envelope alphabet has symbols (polarity, current output, mate output, digit), matches by reversing polarity and the two output fields, reads the current output field, and replaces each source bracket by one length-m envelope block. Definition definition Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/specs/m19-fixed-envelope-recoding.md FPRD-D15 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Add a self-contained definition page with examples, nonexamples, and dependency boundaries. FPRD-D17 The fixed-block boundary residual profile of an injective uniform code tau and a finite complete source controller records each source-state right language and its compiled boundary right language, their exact and bounded suffix-lift observations, shortest separation depths, the distinct proper code-prefix counts, raw and reachable compiled-control sizes, and, for a fixed-envelope witness, the digit capacity, envelope size, and block-width observation lag. Definition definition Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/specs/m20-fixed-block-residual-profile.md FPRD-D11; FPRD-D12; FPRD-D16 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Add a self-contained definition page with examples, nonexamples, and dependency boundaries. FPRD-C02 There exists a deterministic visibly pushdown language whose call, return, and local annotations forget to a language outside PEL. Forgotten-action deterministic visible projections are exactly CFL by FPRD-T91, while Kim and Park exhibit a linear context-free language outside PEG. The universal question is therefore resolved negatively. Source verification source verified Evidence and limits → Automata and formal languages Formal languages and scaffolding automata docs/specs/post-m33-dyck-annotation-forgetting.md FPRD-T91; FPRD-T92; FPRD-T93; FPRD-T94; FPRD-T95; FPRD-T96; FPRD-T97; FPRD-T98; FPRD-T99; FPRD-T88; FPRD-T100; FPRD-T101; FPRD-T102; FPRD-T103; FPRD-T104; FPRD-T105; FPRD-T106; FPRD-T107; FPRD-T108; FPRD-T109; FPRD-T112; FPRD-T164; FPRD-T165; Kim-Park 2026, Theorem 4.19 FPRD governed claims ledger Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Add the exact primary-source locator and keep source verification separate from proof of the FPRD consequence. PUB-persistent-stacks-scaffolding--thm-transfer-intro Theorem 1.1 (Real-time transfer). Let L L L L R ∈ P E G . L^R\in\mathsf{PEG}. L R ∈ PEG . theorem released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Theorem 1.1 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--cor-epal-intro Corollary 1.2 . E P A L 2 ∈ P E G \mathsf{EPAL}_2\in\mathsf{PEG} EPAL 2 ∈ PEG corollary released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Corollary 1.2 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--thm-lmr Theorem 2.1 (Loff–Moreira–Reis). For every language K K K K ∈ P E G ⟺ K R is decided by a scaffolding automaton . K\in\mathsf{PEG} \quad\Longleftrightarrow\quad K^R\text{ is decided by a scaffolding automaton}. K ∈ PEG ⟺ K R is decided by a scaffolding automaton . theorem released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Theorem 2.1 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--lem-fresh-initial Lemma 2.2 (Fresh initial state). Every finite scaffolding automaton A A A A ⋆ A^\star A ⋆ lemma released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Lemma 2.2 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--lem-stack-update Lemma 3.1 (Persistent-stack update). Suppose the old scaffold is strictly backward and satisfies C l e a n E m p t y \mathsf{CleanEmpty} CleanEmpty v + v^+ v + C l e a n E m p t y \mathsf{CleanEmpty} CleanEmpty lemma released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Lemma 3.1 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--thm-parallel-stacks Theorem 3.2 (Parallel persistent stacks). Every deterministic letter-synchronous finite-control machine with a fixed positive number s s s s s s theorem released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Theorem 3.2 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--lem-zipper Lemma 4.1 (Tape zipper). Every strict real-time m m m 2 m 2m 2 m lemma released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Lemma 4.1 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--thm-machine-scaffold Theorem 4.2 (Strict machine-to-scaffold simulation). Let M M M m m m m ≥ 1 m\geq 1 m ≥ 1 A M A_M A M 2 m 2m 2 m L ( A M ) = L ( M ) . L(A_M)=L(M). L ( A M ) = L ( M ) . theorem released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Theorem 4.2 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--thm-transfer Theorem 5.1 . If L L L L R ∈ P E G . L^R\in\mathsf{PEG}. L R ∈ PEG . r e v ( R T - M T T M ) ⊆ P E G . \mathsf{rev}(\mathsf{RT\text{-}MTTM})\subseteq\mathsf{PEG}. rev ( RT - MTTM ) ⊆ PEG . theorem released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Theorem 5.1 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--lem-strict-online Lemma 5.2 (Strict real time is online constant time). Every language recognized by a strict real-time multitape machine belongs to O n l i n e ( O ( 1 ) ) \mathsf{Online}(O(1)) Online ( O ( 1 )) lemma released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Lemma 5.2 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--cor-proper Corollary 5.3 (Proper class containment). r e v ( R T - M T T M ) ⊊ P E G . \mathsf{rev}(\mathsf{RT\text{-}MTTM})\subsetneq\mathsf{PEG}. rev ( RT - MTTM ) ⊊ PEG . corollary released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Corollary 5.3 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--thm-classical-pal-interface Theorem 6.1 (Classical palindrome interface (classical, imported)). There are finite m , Q , T m,Q,T m , Q , T m m m P P P x ∈ { 0 , 1 } ∗ x\in\{0,1\}^* x ∈ { 0 , 1 } ∗ ∣ x ∣ |x| ∣ x ∣ x = x R x=x^R x = x R x = ε x=\varepsilon x = ε theorem released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Theorem 6.1 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--lem-epal-identity Lemma 6.2 (Even-palindrome identity). For every binary word x x x x ∈ { w w R : w ∈ { 0 , 1 } ∗ } ⟺ x = x R and ∣ x ∣ is even . x\in\{ww^R:w\in\{0,1\}^*\} \quad\Longleftrightarrow\quad x=x^R\ \text{ and }\ |x|\text{ is even}. x ∈ { w w R : w ∈ { 0 , 1 } ∗ } ⟺ x = x R and ∣ x ∣ is even . x = ε x=\varepsilon x = ε lemma released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Lemma 6.2 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--lem-epal-reversal Lemma 6.3 (Reversal invariance). ( E P A L 2 ) R = E P A L 2 . (\mathsf{EPAL}_2)^R=\mathsf{EPAL}_2. ( EPAL 2 ) R = EPAL 2 . lemma released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Lemma 6.3 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--lem-parity-product Lemma 6.4 (Parity product). Suppose a strict real-time machine P P P x x x x = x R x=x^R x = x R P e v e n P_{\mathrm{even}} P even E P A L 2 \mathsf{EPAL}_2 EPAL 2 lemma released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Lemma 6.4 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--thm-epal Theorem 6.5 . The even-length binary palindrome language has a parsing expression grammar: E P A L 2 = { w w R : w ∈ { 0 , 1 } ∗ } ∈ P E G . \boxed{\mathsf{EPAL}_2=\{ww^R:w\in\{0,1\}^*\}\in\mathsf{PEG}.} EPAL 2 = { w w R : w ∈ { 0 , 1 } ∗ } ∈ PEG . theorem released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Theorem 6.5 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-persistent-stacks-scaffolding--siteauto-main-tex-19 Corollary 6.6 . Conjecture 7 of Loff, Moreira, and Reis [4] is false. corollary released publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Real-time multitape languages transfer to parsing expression grammars, Corollary 6.6 Theorem-level dependency graph not yet atomized Real-time multitape languages transfer to parsing expression grammars Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--thm-lmr Theorem 2.7 (Loff–Moreira–Reis [7, Theorem 16, p. 21] ). A language L ⊆ Σ ∗ L\subseteq\Sigma^* L ⊆ Σ ∗ P E G \mathsf{PEG} PEG L R L^R L R L L L L R L^R L R theorem review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Theorem 2.7 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--thm-context Theorem 5.4 (Occurrence-context factorization). After reading a a a P ′ P' P ′ ℓ ′ \ell' ℓ ′ ( P ′ , ℓ ′ ) = { ( a P a , ℓ 0 ) , ℓ = a ℓ 0 , ( a D a ( P ) a , ω a ( P ) ℓ ) , ℓ ∉ a Σ ∗ , D a ( P ) defined , ( ϵ , a P ℓ ) , ℓ ∉ a Σ ∗ , D a ( P ) undefined . (P',\ell')= \begin{cases} (aPa,\ell_0), &\ell=a\ell_0,\\[1mm] (aD_a(P)a,\omega_a(P)\ell), &\ell\notin a\Sigma^*,\ D_a(P)\text{ defined},\\[1mm] (\epsilon,aP\ell), &\ell\notin a\Sigma^*,\ D_a(P)\text{ undefined}. \end{cases} ( P ′ , ℓ ′ ) = ⎩ ⎨ ⎧ ( a P a , ℓ 0 ) , ( a D a ( P ) a , ω a ( P ) ℓ ) , ( ϵ , a P ℓ ) , ℓ = a ℓ 0 , ℓ ∈ / a Σ ∗ , D a ( P ) defined , ℓ ∈ / a Σ ∗ , D a ( P ) undefined . S ∈ E P A L 2 ⟺ ℓ = ϵ . S\in\mathsf{EPAL}_2\quad\Longleftrightarrow\quad \ell=\epsilon. S ∈ EPAL 2 ⟺ ℓ = ϵ . theorem review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Theorem 5.4 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--lem-chunk Lemma 5.6 (chunk recursion). Let P P P L = λ ( P ) L=\lambda(P) L = λ ( P ) b b b B P B_P B P D b ( P ) = L , ω b ( P ) = B P , D_b(P)=L,\qquad \omega_b(P)=B_P, D b ( P ) = L , ω b ( P ) = B P , a ≠ b a\ne b a = b D a ( P ) = D a ( L ) , ω a ( P ) = ω a ( L ) b B P , D_a(P)=D_a(L),\qquad \omega_a(P)=\omega_a(L)\,b\,B_P, D a ( P ) = D a ( L ) , ω a ( P ) = ω a ( L ) b B P , L = ϵ L=\epsilon L = ϵ lemma review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Lemma 5.6 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--thm-mirror Theorem 6.1 (Typed mirror receipt). Suppose an update selects a longest suffix occurrence Q Q Q a a a Y = a Q a Y=aQa Y = a Q a λ ( Y ) = { a D a ( Q ) a , D a ( Q ) defined , ϵ , D a ( Q ) undefined . \lambda(Y)= \begin{cases} aD_a(Q)a,&D_a(Q)\text{ defined},\\ \epsilon,&D_a(Q)\text{ undefined}. \end{cases} λ ( Y ) = { a D a ( Q ) a , ϵ , D a ( Q ) defined , D a ( Q ) undefined . λ ( Y ) \lambda(Y) λ ( Y ) Y Y Y theorem review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Theorem 6.1 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--prop-endpoint Proposition 6.2 (Endpoint-only escape). For m ≥ 2 m\ge2 m ≥ 2 S m = 0 2 m 1100 S_m=0^{2m}1100 S m = 0 2 m 1100 001100 001100 001100 00 00 00 00 00 00 0 2 m 0^{2m} 0 2 m 0 2 m , 0 2 m − 2 , … , 00 , ϵ . 0^{2m},0^{2m-2},\ldots,00,\epsilon. 0 2 m , 0 2 m − 2 , … , 00 , ϵ . 00 00 00 m − 1 m-1 m − 1 proposition review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Proposition 6.2 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--prop-type-birth Proposition 7.1 (Future transition after type birth). For r ≥ 1 r\geq1 r ≥ 1 A r = 0 2 r A_r=0^{2r} A r = 0 2 r P r = A r 11 A r , T r = 1 A r 1. P_r=A_r11A_r, \qquad T_r=1A_r1. P r = A r 11 A r , T r = 1 A r 1. D 1 ( P r ) = A r D_1(P_r)=A_r D 1 ( P r ) = A r 1 1 1 T r = 1 D 1 ( P r ) 1 T_r=1D_1(P_r)1 T r = 1 D 1 ( P r ) 1 P r P_r P r P r P_r P r T r T_r T r P r 1 P r P_r1P_r P r 1 P r P r P_r P r P r P_r P r proposition review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Proposition 7.1 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--prop-anchor-dependence Proposition 7.2 (Anchor dependence). For the fixed one-letter block w = 0 w=0 w = 0 A r = 0 2 r A_r=0^{2r} A r = 0 2 r λ ( 0 A r 0 ) = A r . \lambda(0A_r0)=A_r. λ ( 0 A r 0 ) = A r . 0 0 0 proposition review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Proposition 7.2 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--prop-bridge-chase Proposition 7.3 (Bridge-chasing escape). For r ≥ 1 r\geq1 r ≥ 1 d ≥ 0 d\geq0 d ≥ 0 P r , d = A r ( 11 A r ) d , A r = 0 2 r . P_{r,d}=A_r(11A_r)^d, \qquad A_r=0^{2r}. P r , d = A r ( 11 A r ) d , A r = 0 2 r . d > 0 d>0 d > 0 λ ( P r , d ) = P r , d − 1 and b P r , d = 1 , \lambda(P_{r,d})=P_{r,d-1} \quad\text{and}\quad b_{P_{r,d}}=1, λ ( P r , d ) = P r , d − 1 and b P r , d = 1 , A r A_r A r 0 0 0 0 0 0 P r , d P_{r,d} P r , d d d d A r A_r A r proposition review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Proposition 7.3 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--lem-shadow Lemma 8.3 (Bridge-shadow identity). Suppose H = R b P H=RbP H = R b P λ ( H ) = P \lambda(H)=P λ ( H ) = P P P P w R P w^RP w R P w = ϵ w=\epsilon w = ϵ w w w b b b Λ ( H , w ) = Λ ( P , w ) . \Lambda(H,w)=\Lambda(P,w). Λ ( H , w ) = Λ ( P , w ) . lemma review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Lemma 8.3 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--lem-mirror-prefix Lemma 8.5 (Mirror-prefix lemma). Let Y Y Y c c c D c ( Y ) D_c(Y) D c ( Y ) Π ( c D c ( Y ) c , ω c ( Y ) ) \Pi(cD_c(Y)c,\omega_c(Y)) Π ( c D c ( Y ) c , ω c ( Y )) F = Y c ω c ( Y ) F=Yc\,\omega_c(Y) F = Y c ω c ( Y ) λ ( F ) = Y \lambda(F)=Y λ ( F ) = Y D c ( Y ) D_c(Y) D c ( Y ) Π ( ϵ , c Y ) \Pi(\epsilon,cY) Π ( ϵ , c Y ) F = Y c c Y F=YccY F = Y cc Y λ ( F ) = Y \lambda(F)=Y λ ( F ) = Y Y Y Y lemma review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Lemma 8.5 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--cor-anchor-links Corollary 8.6 . With Y = L b B Y=LbB Y = L b B c ≠ b c\ne b c = b D c ( Y ) D_c(Y) D c ( Y ) L = Z c D c ( L ) L=ZcD_c(L) L = Z c D c ( L ) λ ( Z c L ) = L \lambda(ZcL)=L λ ( Z c L ) = L D c ( Y ) D_c(Y) D c ( Y ) λ ( L c c L ) = L \lambda(LccL)=L λ ( L cc L ) = L corollary review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Corollary 8.6 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--thm-ropes Theorem 8.7 (Receipt-rope recurrence). Let ρ b \rho_b ρ b Ω b ( Y ) \Omega_b(Y) Ω b ( Y ) c ≠ b c\ne b c = b Ω c ( Y ) = { undefined , Ω c ( L ) undefined , Ω c ( L ) ⋅ ( b , ρ b ) ⋅ body Ω b ( Y ) , otherwise , \Omega_c(Y)= \begin{cases} \text{undefined},&\Omega_c(L)\text{ undefined},\\ \Omega_c(L)\cdot(b,\rho_b)\cdot\operatorname{body}\Omega_b(Y),&\text{otherwise}, \end{cases} Ω c ( Y ) = { undefined , Ω c ( L ) ⋅ ( b , ρ b ) ⋅ body Ω b ( Y ) , Ω c ( L ) undefined , otherwise , Z c ( Y ) Z_c(Y) Z c ( Y ) Z c ( Y ) = Z c ( L ) ⋅ ( b , ρ b ) ⋅ body Ω b ( Y ) . Z_c(Y)=Z_c(L)\cdot(b,\rho_b)\cdot\operatorname{body}\Omega_b(Y). Z c ( Y ) = Z c ( L ) ⋅ ( b , ρ b ) ⋅ body Ω b ( Y ) . theorem review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Theorem 8.7 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--thm-closure Theorem 8.9 (Full abstract receipt closure). Over a fixed alphabet, a fresh occurrence record, its complete direct/reset rope table, and the updated live context are obtained from old receipts by a fixed number of head, tail, singleton, inject, and catenation operations. theorem review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Theorem 8.9 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--thm-compiler Theorem 10.2 (Simultaneous batch compiler). Every transducer of Definition 10.1 whose initial record graph is fixed, finite, immutable, and pointer-closed compiles exactly and letter-synchronously into a finite scaffolding automaton of degree d = max { 1 , s + A q } d=\max\{1,s+Aq\} d = max { 1 , s + A q } r + 1 r+1 r + 1 theorem review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Theorem 10.2 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--thm-kt Theorem 11.1 (Kaplan–Tarjan [6, Theorem 5.1, p. 592] ). There is a purely functional regular catenable steque whose push, pop, inject, and catenation operations take worst-case constant time and preserve the representation. theorem review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Theorem 11.1 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--thm-staging Theorem 11.2 (Opaque-atom staging). Let a strict purely functional sequence operation, parameterized by a base element type A A A c a r \mathsf{car} car c o n s \mathsf{cons} cons c d r \mathsf{cdr} cdr A A A theorem review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Theorem 11.2 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--thm-whole-client-normalization Theorem 11.3 (Whole-client bounded symbolic normalization). Fix a finite immutable record signature. Let one deterministic strict client transition have a uniform bound on calls, constructor tests, loops, recursion, and retained fresh records. Suppose it observes only finite tags, finite nonpointer data, old records reached by bounded rooted addresses, and constructors of ordinary fresh structural records already known to its symbolic evaluation. It neither observes pointer identity or allocation state nor inspects an unresolved opaque atom, designated fresh payload, or designated fresh owner. Suppose also that every old pointer later read or retained has a bounded rooted provenance, temporary control packages do not escape, and unreachable failure leaves are completed by a fixed finite plan. Then the whole client normalizes to one bounded simultaneous record-transducer plan determined only by finite control, the input letter, and a bounded labelled unfolding of the old roots. theorem review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Theorem 11.3 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--thm-direct Theorem 12.2 (Direct palindrome construction). For a persistent sequence implementation satisfying the contract of Section 11.1, the receipt construction recognizes the binary even-palindrome language with a finite scaffolding automaton. If the complete client has source-record bounds ( A ∗ , q , R ∗ ) (A_*,q,R_*) ( A ∗ , q , R ∗ ) max { 1 , 2 + A ∗ q } \max\{1,2+A_*q\} max { 1 , 2 + A ∗ q } R ∗ + 1 R_*+1 R ∗ + 1 theorem review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Theorem 12.2 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists. PUB-direct-palindrome-scaffolding--cor-peg Corollary 12.3 (Direct PEG route). Under the sequence contract in Theorem 12.2, the construction yields a PEG for E P A L 2 \mathsf{EPAL}_2 EPAL 2 corollary review publication statement; not independently promoted by this index Evidence and limits → Automata and formal languages Scaffolding automata and PEGs Persistent receipts and simultaneous records: a direct scaffold for even palindromes, Corollary 12.3 Theorem-level dependency graph not yet atomized Persistent receipts and simultaneous records: a direct scaffold for even palindromes Reviewed 2026-09-01 No documented external or specialist review of this FPRD result is recorded. Map this publication statement to any governed claim, verify its hypotheses and proof dependencies, and remove duplicate inventory rows only after an exact mapping exists.