Combined proof audit and terminal-marker strengthening
FPRD Lab, 5 September 2026. Internal audit; no external review claimed.
Contents
Continuity
This work continues the initial FPRD-residual-access-attack-2026-09-04.md, run 1’s nonlinearity and residual formulas, and run 2’s guarded-cluster theorem. All three proofs were reread. The new manuscript is self-contained; it does not require those progress reports to understand its definitions.
The language U is unchanged. In particular, the ignored data tail is arbitrary and may be malformed. Canonical complete balanced trees are only the instances used for the reduction and matched profiles.
Audit verdict
No substantive gap was found in the combined grammar, residual, nonlinearity, and direct simulation proofs. The rank identities and reduction stand without a lower-bound premise. The access exclusion continues to use Ko, and the PEG consequence additionally uses Loff–Moreira–Reis.
Ko’s complete communication argument is not independently proved by this audit. Its precise statement and model fit were checked. The needed premise is explicitly named Hypothesis K in the manuscript; its failure would not invalidate the elementary construction or the direct reduction implication.
Kim–Park remain the explicit methodological source. Reproving the simulation does not erase that intellectual debt. No claimed proof of theirs is used as a black-box premise.
New theorem in this run
Run 2 placed a distinguished marker first, using rows (1,A_i). This matches all unconditioned update/query counts, but fixing that first marker to zero can destroy the match. The new construction puts the marker last, using (A_i,1), and correspondingly uses guards (e_c,0).
For a fixed initial update segment v of length j and query cylinder I(r), the number of distinct full residuals induced by completing the updates is
2^rank(M[I(r), j+1:d]).After the cluster index is fixed, every selected cylinder consists of common guards and at most one distinguished row. As long as any coordinate remains, the final marker remains among the suffix columns. That distinguished row therefore contributes exactly one dimension regardless of A_i. Before the cluster index is fixed, the cylinder contains a full cluster and has full suffix-column rank. This proves every conditional profile equality.
The affine-map fibres are uniform and have size 2^(d-j-rank), proving the matching probability-multiset statement. The actual probability measures on named residual sets need not agree.
The hard reduction uses (x,0). Its final marker can be processed with the last coordinate update, so the source problem still has exactly n operations with constant probes per operation. No future query information enters the updates.
Risks checked
| Potential defect | Finding |
|---|---|
| Only promised continuations counted | The paper gives the full residual formula; equal leaf lengths and tree depth exclude other continuations. |
| Malformed tails create multiple parses | The query determines the unique selected path; skipped complete trees are self-delimiting, and R has unique derivations. |
| Reversed address selects a different cluster | Low-order bits encode i, high-order bits encode c; reversed transmission reveals i first. The semantic checker confirms this. |
| Extra marker changes the lower-bound update model | The fixed terminal zero is bundled with the last coordinate update; constant overhead only. |
| Polynomial expansion invalidates word size | m=Theta(n^3), d=n+1, encoding length O(n^4). Addresses remain Theta(log n) bits. |
| Uncharged state carries the whole update history | The simulator stores the header and all persistent state in charged memory. |
| A fixed easy matrix refutes hard-family wording | Hardness is worst-case over arbitrary A for one data-structure algorithm; no assertion that every A is hard. |
| Nonlinearity is merely a grammar property | A regular slice and homomorphism extract aE; the end-pumping argument proves language-level nonlinearity. |
| Identical counts imply identical residuals | Explicitly false: n=1, A=[1], update 10, distinguished query gives different membership answers. |
| Novelty inferred from finite checks | No such inference. A bounded primary-source search found no direct match but is insufficient to establish novelty. |
Corrections to prior reporting
- The run-2 audit text said “all 256 binary 2-by-2 matrices.” The code actually enumerated all binary 4-by-2 matrices (n^2 by n, with n=2). The new paper uses the correct dimensions.
- Prior packets gave pages 58–83 for Loff–Moreira–Reis. The journal metadata gives JCSS 111 (2020), 1–21, DOI 10.1016/j.jcss.2020.01.001. This is corrected in the paper. The author-version reference to Theorem 16 is unchanged.
- “Complete profile” was too easy to read as the complete residual transition system. The new paper defines exactly which counts and conditioning it matches, and explicitly distinguishes residual labels and transition maps.
Finite corroboration
check_conditioned_profiles.py passed on 267 matrices: all 258 matrices for n=1,2 and nine deterministic examples at n=3,4,6. It checked 62,809 pairs of query cylinders and suffix-coordinate ranks. Five representative matrices were also checked using actual semantic acceptance signatures, giving 4,909 conditional histogram checks. These numbers describe scope, not significance.
The original CFG/traversal checker and its earlier 23,720-case result are retained as prior corroboration. It was not expanded or rerun merely to raise the check count. The new checker invokes its semantic recognizer where that provides a distinct check on the altered indexing and marker placement.
Retained failures and open problems
The two literal PEG conversions fail on:
t[1]t[1][1]$1#01
tt[1][1][1]$1#10Their respective outer end-guard variants fail on:
tt[1]t[1][1]$1#010
t[0]tt[1][1][1]$1#101These falsify those grammars, not all PEGs for U. U in PEG remains open. The new construction does not preserve profiles after arbitrary coordinate conditioning; fixing the final marker while varying preceding coordinates is outside its claim. It does not give two CFLs with equal global residual growth, or an intrinsic SCA lower bound independent of the cell-probe literature.
The focused continuation, if research resumes, is a construction for U in PEG or a richer residual classifier retaining transition maps. A linear and unambiguous hard witness requires a different language: U itself is not linear.
Reading-edition revision
Revision 2 expands explanation and examples, with no change to the eight numbered mathematical statements. The new terminal-marker table was checked by the publication example checker; details appear in /reading-editions/publication-audit.md. The original residual-count terminology in the opening is clarified to distinguish one residual from the number of distinct residuals across prefixes.
Research-note status and attribution
Revision 4 retains all eight statements and supporting arguments as research work within FPRD Lab. Kim–Park already provide an explicit grammar and separation. The note follows their lower-bound strategy and adapts the eight recursive parity productions from their equation (3), with a different base case and tree-addressed selection. Novelty of the extensions has not been established. The change in publication status does not change the mathematical statements or their dependencies.