FPRD LabShare an approach

← Claims

Theorem

FPRD-T43

Exact one-way information at a recognition cut

Exact statement

At every fixed cut (T,m)(T,m), the distinct future rows are the minimum reachable message alphabet of an exact deterministic prefix-to-suffix one-way protocol. The exact fixed-length binary cost is ⌈log⁡2rf(T,m)⌉\lceil\log_2 r_f(T,m)\rceil. Every deterministic one-pass recognizer has at least rf(T,m)r_f(T,m) reachable complete configurations at that cut and at least the same ceiling-log number of mutable bits.

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

Context

The same future-row coordinate controls three resources: semantic states in a layered recognizer, messages sent across a cut, and complete mutable configurations of a one-pass machine.

Definitions

  • A protocol has an encoder e:Σm→Me:\Sigma^m\to M and decoder d:M×ΣT−m→{0,1}d:M\times\Sigma^{T-m}\to\{0,1\} satisfying d(e(u),v)=f(uv)d(e(u),v)=f(uv).
  • A complete mutable configuration includes every input-dependent datum that can affect subsequent transitions or output.

Hypotheses and scope

  • Only reachable messages and configurations are counted.
  • The protocol is deterministic, one-way, and exact for the selected fixed-length slice.
  • Bit cost uses fixed-length encodings; one reachable message therefore costs zero bits.

Proof or evidence

Send each prefix to its future-row class. Conversely, any correct message or machine configuration shared by two prefixes forces the same answer on every legal suffix, so it determines only one future row. This gives a forced surjection onto the row set. A fixed b-bit code contains at most 2^b messages, and the canonical row protocol meets the ceiling-log lower bound.

Exact one-way cut cost and configuration transfer →

Verification notes

The proof and independent audit check the message factor, decoder preservation, exact bit rounding, complete configurations, all-zero rows, endpoint cuts, and constant slices. The exhaustive binary audit compares 22,369,894 prefix pairs; the theorem's nonbinary proof is the same row-factor argument. The generalized-Dyck and controlled-Dyck bridges were cross-checked against their earlier constructions.

Limitations

  • The matching upper recognizer may depend on the selected total length; it is a nonuniform exact upper bound.
  • The result does not cover randomization, interaction, approximation, variable-length coding, or average-case cost.
  • An all-zero future row still counts as a reachable message or configuration even though it contributes no matrix-rank dimension.

Open work

Separate the exact deterministic theorem from possible randomized, interactive, amortized, and uniform-streaming variants.

Notes

The exact deterministic row/message theorem is classical in shape. The milestone tests its integration with FPRD future coordinates and keeps fixed-length, complete-configuration, and nonuniformity conventions explicit.