FPRD LabShare an approach

← Claims

Definition

FPRD-D22

Fixed-length recognition cuts

Exact statement

A fixed-length recognition-cut datum consists of a finite nonempty alphabet, a total input length, a Boolean function on words of that length, the exact prefix-to-suffix future rows at every cut, strict reachable deterministic layered recognizers, deterministic one-way protocols across a cut, and fixed-length binary message cost.

StatusPrecisely stated with reachability and fixed-length conventions
External reviewNo documented external or specialist review of this FPRD result is recorded.

Context

The definition isolates the information that a prefix must preserve when every legal suffix has a fixed remaining length. It is the common interface behind the layered-state, one-way communication, and one-pass memory results below.

Definitions

  • For f:ΣT→{0,1}f:\Sigma^T\to\{0,1\}, a prefix u∈Σiu\in\Sigma^i has future row ru:ΣT−i→{0,1}r_u:\Sigma^{T-i}\to\{0,1\} given by ru(v)=f(uv)r_u(v)=f(uv).
  • Two prefixes at the same cut are equivalent exactly when their future rows agree on every suffix of the required length. Write RT,iR_{T,i} for the set of distinct reachable rows and rf(T,i)=∣RT,i∣r_f(T,i)=|R_{T,i}|.
  • A strict layered recognizer advances through disjoint grades in the fixed symbol order; only states reached by prefixes count.
  • A deterministic one-way protocol sends one prefix-dependent message to a suffix reader. Message names not produced by any prefix are discarded.

Hypotheses and scope

  • The alphabet is finite and nonempty.
  • The total length and cut position are fixed.
  • Recognition is deterministic and exact on every word of the selected length.
  • Binary message cost uses one fixed number of bits for every reachable message at that cut.

Proof or evidence

The specification separates literal matrices from their quotient by equal rows and fixes the categories in which minimum and uniqueness are later asserted. The proof record uses these conventions without changing them at boundary cases such as total length zero or a constant recognition slice.

Recognition-cut definitions →

Verification notes

The definition was checked against the M25 proof, every Boolean function on binary words through length four, and the endpoint and constant-slice boundaries. Reachability, strict grades, exact remaining length, complete mutable configurations, and fixed-length rather than prefix-free message coding are all explicit.

Limitations

  • The per-length canonical recognizer is not by itself one uniform streaming algorithm across all lengths.
  • Row cardinality is distinct from matrix rank.
  • The definition does not cover randomized, nondeterministic, interactive, or variable-length protocols.

Open work

Add a two-cut worked example showing literal rows, the row quotient, the canonical layered states, and the corresponding messages.

Notes

Exact-length rows, reachable states and messages, strict fixed-order layers, and fixed-length codes are part of the category. Row cardinality is distinct from matrix rank, and the per-total-length canonical program is not by itself a uniform streaming algorithm.