promoted from data/fprd-lab/fold-look/fold-resource-accounting-audit.md on 2026-07-28 — status: unverified

Adversarial audit of this lab’s own fold resource accounting. Proposition R1 couples P_sites, fold count, material and precision. For parity it gives Lambda_fp/delta+1 >= m 2^(m-1-F), exponential under a small-fold budget such as F=O(log m), not unconditionally in F. Records two uncharged resources: Look’s fan-in and encoder work.

Adversarial audit of the fold resource accounting

Status: three findings against this lab’s own resource table. Two are false counts; one is an uncharged primitive. One of them recovers a bound that was over-withdrawn. Scope. Hidden random access and false resource counts only. This memo does not propose a theory and does not select an abstraction.

Finding 1 — the resource coordinates are not independent

The resource table reported $M, I, F, U, C, P, L, D, B, Q, W$ as separate coordinates and stated that “material lower bounds do not follow” and that “a construction may trade material for precision.” Both are true, and both concealed that the trade is constrained. It is not free.

Write $A$ for the number of affine pieces of $\varphi$, $\Lambda_{\mathrm{fp}}$ for the footprint length, and $\delta$ for the minimum separation of sites that share an affine piece.

Proposition R1 (coupling). $\displaystyle P_{\mathrm{sites}}\ \le\ A\left(\frac{\Lambda_{\mathrm{fp}}}{\delta}+1\right)\ \le\ 2^{F}\left(\frac{\Lambda_{\mathrm{fp}}}{\delta}+1\right).$

Proof. Every site lies in exactly one affine piece. On a piece $\varphi$ is an isometry, so sites sharing a piece have images at distance $\ge\delta$, and all images lie in the footprint. Hence a piece carries at most $\Lambda_{\mathrm{fp}}/\delta+1$ sites. Multiply by $A$, and apply $A\le2^F$ (Theorem 5, and the enumerator lane’s Theorem A for the general case). $\square$

Combined with $\ell_{\mathrm{DNF}}(g)\le P_{\mathrm{sites}}$, which the later re-audit proves already under (GP), (NC), and (IN):

Corollary R2 (material–precision lower bound). $\displaystyle 2^{F}\left(\frac{\Lambda_{\mathrm{fp}}}{\delta}+1\right)\ \ge\ \ell_{\mathrm{DNF}}(g).$

Why this matters. It closes the hole the memo itself flagged. One cannot have all three of few folds, short strip, and coarse precision. Verified over 4 000 WFL programs with no violation.

It is not vacuous. For parity, $\ell_{\mathrm{DNF}}=m2^{m-1}$, so with $F=\lceil\log_2 m\rceil$ the required ratio $\Lambda_{\mathrm{fp}}/\delta$ is at least:

Thus at the displayed logarithmic fold budget parity forces an exponential material-to-precision ratio—either an exponentially long strip or exponentially fine features. In general the exact conclusion is $$\frac{\Lambda_{\mathrm{fp}}}{\delta}+1\ge m\,2^{m-1-F};$$ with unrestricted $F$, no unconditional exponential ratio follows.

Finding 2 — a bound was over-withdrawn, and is restored

Responding to the audit, this lab withdrew the parity bound $P_{\mathrm{sites}}\ge m2^{m-1}$ on the grounds that “the literal-counting rescue does not extend to parity.”

That conflated two different things. The audit’s observation was that parity has no proof independent of Theorem 1 — its prime implicants share literals heavily, so the palindrome argument does not transfer. It did not show the bound false. Under (UF), Theorem 2 gives $\ell_{\mathrm{DNF}}\le P_{\mathrm{sites}}$ directly, so the parity bound holds.

Corrected status. $P_{\mathrm{sites}}\ge m2^{m-1}$ for parity: holds under (UF), and unconditionally in WFL. It has no fallback if (UF) is dropped. $S\ge2^{m-1}$ remains withdrawn — that one depends on $s_{\mathrm{DNF}}\le S$, which is genuinely refuted.

Over-withdrawal is a failure mode worth naming alongside overclaiming. Both misreport the state of the work.

Finding 3 — two genuinely uncharged resources

Neither is hidden random access. The doctrine has no random access: the encoder is sequential under supply model S, fold lines are input-independent, and Look is parallel rather than addressed. But two costs are levied nowhere.

(a) Look has unbounded fan-in and nothing lower-bounds it. One Look reads the entire folded state — an OR over every location. $L=1$ charges nothing for the width of that observation. The natural charge is $S$, the number of effective fibers, and $S$ is exactly the coordinate whose lower bound was refuted. So at present the model contains an unbounded-fan-in primitive with no proven lower bound on its width. This is the single largest soft spot in the accounting, and it is where a false hardness claim would most easily hide.

(b) Encoder work is uncharged. The composition $\{0,1\}^{2n}\to\text{punched strip}\to\{0,1\}$ draws $\operatorname{Enc}_n$ as one arrow. Under supply model S the encoder holds $O(\log n)$ bits, which was reported — but it must perform $\Theta(P_{\mathrm{sites}})$ placements, which was not. For palindrome that is $\Theta(n)$ and unremarkable. For parity, Finding 1 forces $P_{\mathrm{sites}}\ge m2^{m-1}$, so the encoder performs exponentially many operations while the post-encoding program still reports $F=O(\log m)$, $L=1$.

Reporting “one fold and one look” for such a construction would be accurate about the protocol and grossly misleading about the computation. The predecessor probe already warned that “input preparation is not free”; Finding 1 turns that from a caveat into a quantity.

Consolidated statement

Adding R1 and the encoder-step count, the honest resource vector for a Fold-and-Look presentation is

$$\bigl(F,\ D,\ S,\ P_{\mathrm{sites}},\ \Lambda_{\mathrm{fp}},\ \delta,\ W,\ B,\ T_{\mathrm{enc}}\bigr),$$

subject to $D\le2^F$, $A\le2^F$, $P_{\mathrm{sites}}\le A(\Lambda_{\mathrm{fp}}/\delta+1)$, and $T_{\mathrm{enc}}=\Theta(P_{\mathrm{sites}})$. The first two are inherited classical bounds; the third is proved above; the fourth is a definition that was previously absent.

What this lane did not do

It did not attempt the activation theorem, propose a PEG–origami correspondence, or select the next abstraction. Those are led elsewhere. The crease/finger results this lane was asked to formalize were not received in a readable form and are not formalized here.