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

Bounded-fold incidence run, theorem memo. The repaired incidence normal form is independently re-audited for positive punch radius. It yields w_DNF<=D and, for nonconstant functions, s_DNF<=S; a stronger corrected normal form yields l_DNF<=P_sites without (UF). The classical depth bound D<=2^F is retained with its stated all-layers scope.

The Fold-and-Look formula-resource theorem

Status: Theorem 1 was refuted by independent audit and repaired here. The repaired theorem was subsequently independently re-audited and confirmed for $R>0$; that re-audit also corrected the proof’s description of what (UF) holds constant. See docs/verify/bounded-fold-incidence-audit.md and docs/verify/llfl-reaudit-findings.md. Gate A of the bounded-fold incidence run. Starting commit: caffeffe. Predecessor: docs/probes/fold-look-palindrome-probe.md, closed and not modified. These three named files are retained for provenance but are not included in this archive.

This is the secure output of the run. It is a statement about a pinned doctrine, not about paper folding in general.

0. Correction carried from the predecessor

The palindrome probe said one fold gives “exactly one pairing.” That is wrong, and the error was load-bearing rather than cosmetic. One fold gives one reflection, and a single reflection can align linearly many pairs simultaneously — the palindrome construction is exactly that case, where one reflection carries all $n$ pairs at once. After several folds a final location can carry more than two layers. The correct object is therefore a fiber system, or equivalently an incidence hypergraph, not a matching. Everything below is stated for fibers of arbitrary size.

1. The doctrine $\mathsf{LLFL}$

A literal-local Fold-and-Look presentation of a Boolean function $g:\{0,1\}^N\to\{0,1\}$ consists of:

• a connected strip $P=[0,\Lambda]$ of paper, initially flat, depth one;
• a finite set of potential feature sites $p_1,\dots,p_M\in P$, pairwise distinct;
• for each site $p$, a control literal $\ell_p$, one of $x_i$, $\neg x_i$, $\mathsf{TRUE}$, $\mathsf{FALSE}$. Site $p$ is open on input $w$ iff $\ell_p(w)=1$; an open site is punched with a hole $[p-R,p+R]$, a closed site is left solid;
• an input-independent fold program $P^{\mathrm{fold}}$ of $F$ perpendicular all-layers simple folds. The program may depend on $N$. It may not depend on $w$;
• no Cut and no Punch after encoding, and no Unfold;
• exactly one final Look.

Write $\varphi:P\to\mathbb R$ for the address map sending each material point to its final coordinate, and

$$\Phi(y)=\varphi^{-1}(y)$$

for the complete layer fiber over final location $y$.

Four quantities must be kept apart and are not interchangeable:

Dense placement must not silently convert exponentially many logical sites into constant material cost. Any construction claiming small $\Lambda$ with large $M$ is claiming precision, and must say so.

1.1 Standing hypotheses

(GP) Clean alignment. For all sites $p,q$: either $\varphi(p)=\varphi(q)$ or $|\varphi(p)-\varphi(q)|>2R$.

(NC) No crease through a punch. Every interval $[p-R,p+R]$ lies inside a single affine piece of $\varphi$.

(IN) Interiority. Every punch image is strictly interior to the final footprint.

$R>0$. The punch radius is strictly positive. Added after re-audit: with $R=0$ all other hypotheses hold vacuously and Theorem 1 is false — one interior site on a flat strip gives formula $=x_0$ while removing a single point leaves no complementary component of positive length, so Look $\equiv0$. Same species as the $F=0$ degeneracy that refuted $s_{\mathrm{DNF}}\le S$.

(UF) Uniform overlay. No image of a maximal affine-piece endpoint — a crease image or a strip-end image — lies in the open interval $(\varphi(p)-R,\;\varphi(p)+R)$ for any site $p$. Equivalently, the set of pieces covering $z$ is constant throughout each punch image.

Corrected after re-audit. This memo previously said “the layer fiber $\Phi(z)$ is constant throughout each punch image.” That is false in essentially every configuration, including the flat one, where $\Phi(z)=\{z\}$ moves with $z$. What is constant is the set of covering pieces, equivalently $|\Phi(z)|$, with $\Phi(z)$ tracking $z$ by isometry. “Maximal” is also now explicit: under a non-maximal reading (UF) would be strictly stronger than needed and would exclude legal programs.

(UF) was added after an independent audit refuted Theorem 1 without it. The counterexample and the failing line are recorded in docs/verify/bounded-fold-incidence-audit.md. In brief: a second layer’s boundary can land strictly inside a punch image, so the fiber is not constant there, and the see-through set is larger than the fiber test predicts. (GP) constrains pairs of sites, (NC) a punch’s own material, (IN) the overall footprint — none of the three forbids it.

(UF) is exactly the condition An–Demaine–Demaine–Ku’s construction has and this memo originally dropped: their §4 states “Flat-folding $v(P')$ has $m$ layers uniformly at every point.” The generalization of their Lemma 2 discarded the uniformity that made it work. (UF) restores it, localized to the punches rather than imposed globally.

These are the generalizations of §4.3 of the palindrome probe. They are hypotheses, not consequences: a fold program may violate them, and any specific program must be checked. (GP) fails exactly when two sites land near but not at the same place; (IN) fails when a hole degenerates into a bite out of the boundary, which removes material without creating genus.

2. The incidence normal form

Theorem 1 (normal form). Under (GP), (NC), (IN) and (UF), for a fixed fold program, $$\operatorname{Look}(w)\;=\;\bigvee_{y\in Y_{\mathrm{eff}}}\ \bigwedge_{p\in\Phi(y)}\ell_p(w),$$ where $Y_{\mathrm{eff}}$ is the set of $y$ interior to the footprint with $\Phi(y)\ne\varnothing$ and every $x\in\Phi(y)$ a site.

Without (UF) this statement is false, with a one-fold, one-site counterexample. The two additional conditions on $Y_{\mathrm{eff}}$ are also repairs: as originally written, $y$ outside the footprint had $\Phi(y)=\varnothing$, making the membership test vacuously true and the empty conjunction TRUE, so the displayed formula read literally was identically 1. The proof handled that; the statement did not.

Proof. Look returns 1 iff some point of the final footprint is absent from every layer covering it. Fuse touching layers; a point $z$ is absent from the fused object iff every material point over $z$ has been removed.

The set of removed points. Material is removed only inside punches. By (NC) each punch lies in one affine piece, and $\varphi$ restricted to an affine piece is an isometry, so the punch at an open site $p$ maps onto the interval $[\varphi(p)-R,\varphi(p)+R]$, of the same length. By (GP) two such images are either identical or disjoint. Hence the removed set is a disjoint union of intervals $I_y=[y-R,y+R]$, one for each final location $y$ carrying at least one open site.

Which locations are see-through. Fix $z$ in the open punch image $I_y$. Every material point over $z$ must be removed. Here (UF) is required, but it does not say $\Phi(z)=\Phi(y)$. It says that the same set of maximal affine pieces covers every point of $I_y$. On each such piece the inverse point $x_j(z)$ tracks $z$ by isometry, and $x_j(z)$ lies in the punch centred at $x_j(y)$ exactly when that centre is a site whose controlling literal is true. Thus a non-site in $\Phi(y)$ blocks the whole open image; if every element of $\Phi(y)$ is a site, the whole open image is see-through exactly when $\bigwedge_{p\in\Phi(y)}\ell_p(w)$ holds. Taking the disjunction over $y\in Y_{\mathrm{eff}}$ gives the displayed formula. By (IN) each satisfied term opens a genuine bounded complementary component of positive length, so Look reports 1 exactly then. $\square$

Remaining obligations, discharged explicitly.

• Nonuniform fiber sizes. No fiber size is assumed; terms have different widths and the disjunction is over all of $Y_{\mathrm{eff}}$.
• Fixed holes. Sites with $\ell_p\equiv\mathsf{TRUE}$ contribute the constant 1 to their conjunction and may be deleted from the term.
• Contradictory fibers. A fiber containing both $x_i$ and $\neg x_i$, or any $\mathsf{FALSE}$, has conjunction $\equiv0$; the term is vacuous and is deleted. Such a location is never see-through.
• Duplicate literals. A fiber may contain the same literal twice. Conjunction is idempotent, so the term width counts distinct literals, which is at most $|\Phi(y)|$. Every inequality below is stated in the safe direction.
• Continuous punched regions. Reduced to finitely many fibers above, using (GP) and (NC). Without them the reduction is false.

Provenance. This is an extraction of the OR-over-stacks / AND-over-layers semantics already present in An–Demaine–Demaine–Ku, whose Lemma 2 states that a Look restricted to one cell evaluates $\bigwedge_i d(i,j,k)$ “while the entire Look operation performs the same test in parallel for all DNF clauses $j$, over all variable assignments $k$.” The normal form is not claimed as novel. What is done here is to make the fiber the primary object so that resources can be charged against it.

3. Resources

For a program $\mathcal P$ define:

• $D(\mathcal P)$ — maximum relevant layer depth, $\max_y|\Phi(y)|$;
• $S(\mathcal P)$ — number of effective variable-bearing fibers: locations in $Y_{\mathrm{eff}}$ whose term is neither vacuous nor constant;
• $P_{\mathrm{sites}}(\mathcal P)$ — number of potential input-dependent feature sites;
• $F(\mathcal P)$ — number of folds;
• $W(\mathcal P)$ — cumulative moved material under a pinned convention;
• $B(\mathcal P)$ — description length of the fold program and geometry.

For a Boolean function $g$, let $w_{\mathrm{DNF}}(g)$, $s_{\mathrm{DNF}}(g)$, $\ell_{\mathrm{DNF}}(g)$ be the minimum over exact DNFs of, respectively, the maximum term width, the term count, and the total literal occurrences.

Theorem 2 (formula-resource inequalities). If $\mathcal P$ realizes $g$ in $\mathsf{LLFL}$ under the standing hypotheses including (UF), then $$w_{\mathrm{DNF}}(g)\le D(\mathcal P),\qquad \ell_{\mathrm{DNF}}(g)\le P_{\mathrm{sites}}(\mathcal P),$$ and, for non-constant $g$, $s_{\mathrm{DNF}}(g)\le S(\mathcal P)$.

Status of the three, after audit and re-audit. The width and literal-occurrence inequalities were not refuted — 0 violations in 13 639 legal configurations — and the independent re-audit went further: $\ell_{\mathrm{DNF}}\le P_{\mathrm{sites}}$ is provable from (GP), (NC), (IN) alone, with no (UF), via a corrected normal form (Corollary R2) that replaces $\Phi(y)$ by the sub-fiber of pieces full over the punch image and $Y_{\mathrm{eff}}$ by the locations with a live region of positive length. So the inequality holds on weaker hypotheses than this memo claimed, and everything downstream of it — the parity bound, the material–precision coupling — inherits that. The term-count inequality was refuted as originally stated by a degenerate case independent of Theorem 1: $F=0$, one site with control literal $\mathsf{TRUE}$, giving $g\equiv1$, $s_{\mathrm{DNF}}=1$, and $S=0$ under this memo’s own definition. The parenthetical that once dismissed that case was wrong and has been removed; the hypothesis “non-constant $g$” replaces it. Under the full standing hypotheses, the independently re-audited Theorem 1 exhibits the required DNF, so the nonconstant statement is proved. The 1 427 generic violations found before (UF) show only that this term-count bound must not be exported to the weaker pre-(UF) doctrine.

Proof. Theorem 1 exhibits one exact DNF for $g$. Each minimum is over all exact DNFs, hence at most the value attained by this one.

Width. Term $y$ has width the number of distinct non-constant literals in $\Phi(y)$, at most $|\Phi(y)|\le D(\mathcal P)$.

Count. After deleting vacuous and constant terms the number of terms is exactly $S(\mathcal P)$, which bounds $s_{\mathrm{DNF}}$ provided $g$ is not constant — the constant case is precisely where the count definition and $s_{\mathrm{DNF}}$ disagree, and it is excluded by hypothesis rather than waved away.

Literal occurrences. $\varphi$ is a function, so each site has exactly one image and the fibers partition the sites. That is the whole argument, and it needs no (UF).

Corrected after re-audit; the previous version of this paragraph attributed the partition to (UF) and was wrong about the mechanism. The independent re-audit proved Lemma R1: under (GP) and (NC), material of a partial piece — one whose image meets a punch image without containing it — is never removed anywhere in that punch image. So a punch image is never split into terms; it can only be shrunk. Hence a site contributes at most one term under (GP)+(NC) alone.

This also explains something the earlier audit recorded but could not account for: its 803 failures were entirely one-directional (Look$=1$, formula $=0$, never the reverse). Partial pieces shrink the live region rather than fragmenting it, so the formula can only undercount.

(UF)’s real and only job is to make Theorem 1’s displayed formula correct — without it the term over $\Phi(y)$ is too strong and the $Y_{\mathrm{eff}}$ test too strict. It has no separate role in the literal count. Therefore $\sum_y|\Phi(y)\cap\{\text{variable-bearing sites}\}|\le P_{\mathrm{sites}}$, and the total literal occurrences of our DNF are at most the left side, since duplicate literals in one term are removed. $\square$

Theorem 3 (depth doubling). From a flat depth-one substrate, $F$ all-layers simple folds give $D(\mathcal P)\le 2^{F}$.

Proof. An all-layers folding step satisfies $f_1=f_{0\to1}\circ f_0$ (Definition 2.4 of Folding and Punching Paper): the step acts on the coalesced image surface, not on the original paper. In one dimension $f_{0\to1}$ is a simple fold of the current image interval about a point $L$, so $$\varphi_{k+1}=g_L\circ\varphi_k,\qquad g_L(t)=\begin{cases}t,&t\le L\\ 2L-t,&t>L.\end{cases}$$ Hence $\varphi_{k+1}^{-1}(y)=\varphi_k^{-1}(y)\cup\varphi_k^{-1}(2L-y)$ for $y\le L$, so $D_{k+1}\le 2D_k$, and $D_0=1$. $\square$

The hypothesis in the run brief — “each fold combines at most one moving stack and one stationary stack at a final point” — is exactly the two-term union above, and it is a consequence of the all-layers definition rather than an extra assumption. For some-layers folds the identity $\varphi_{k+1}=g_L\circ\varphi_k$ fails, because the moving cluster is selected in the original paper and $\varphi_{k+1}$ is then not a function of $\varphi_k(x)$ alone. Theorem 3 is therefore stated for the all-layers doctrine only; the some-layers case is an open audit target.

Corollary 4 (fold lower bound). $F(\mathcal P)\ \ge\ \bigl\lceil\log_2 w_{\mathrm{DNF}}(g)\bigr\rceil.$

Proof. Theorems 2 and 3: $w_{\mathrm{DNF}}(g)\le D\le 2^F$. $\square$

4. What this does and does not prove

• It is an internal resource lower bound for the pinned $\mathsf{LLFL}$ doctrine, with all-layers folds and one final Look.
• It is not a lower bound for unrestricted paper-folding computation. A model with Cut, Unfold, input-dependent folds, or more than one Look is not covered and the proofs do not extend as written.
• Material lower bounds do not follow. Nothing here bounds $\Lambda$ from below; a construction may trade material for precision. A material bound requires a declared feature-density or precision constraint.
• Potential sites are not active holes. $P_{\mathrm{sites}}$ counts sites; the number of holes open on a given input is a different and smaller quantity, and $\ell_{\mathrm{DNF}}$ is bounded by the former.
• The DNF produced by Theorem 1 need not be minimal; the inequalities are one-directional by construction and no converse is claimed.

5. Machine check

tools/checks/fold_formula_resource_check.py, exact Fraction arithmetic, no floating point. Relevant results:

• an all-layers fold simulator; the DNF extracted from its fibers agrees with direct evaluation of $\mathrm{MISMATCH}_{2n}$ on all 340 words, $n\le4$;
• over 1440 random all-layers programs, no violation of $D\le2^k$ or of the affine-piece bound;
• the accordion (fold repeatedly at the current midpoint) attains $D=2^k$ exactly for $k\le6$, so Theorem 3 is tight;
• mutation battery: reflection composed with a unit translation, depth counted without the reflected layer, unsigned-only cover, depth-1 fibers wrongly admitted as terms, sign-blind piece merging — all break a check.

Two harness findings recorded rather than hidden. First, a random search over a length-16 strip reached only 26 pieces at $k=5$, below $2^5$; the deterministic accordion witness was needed, and absence under random search is not a bound. Second, the mutation “admit depth-1 fibers as terms” is vacuous for the palindrome construction, because that construction leaves no depth-1 fiber at all — all $4n$ sites occupy $2n$ depth-2 fibers. That vacuity is itself the tightness recorded in the frontier memo, and the mutation was re-pointed at a displaced fold to make it fire.

6. Status

Proved here: Theorems 1–3 and Corollary 4, in the all-layers $\mathsf{LLFL}$ doctrine under (GP), (NC), (IN).

Prior art, as returned by the targeted lane:

• Theorem 1 — classical result used. Inherited from An–Demaine–Demaine–Ku, as this memo said from the outset.
• Theorem 3 ($D\le2^F$) — classical result used. It is the ply restatement of the folklore $2^k$ count that Cardinal et al. use inside Algorithmic Folding Complexity (§2 p. 4, Lemma 1 p. 4). See the piecewise-isometry memo for the located sentences. No claim is made to it.
• Theorem 2 (the three inequalities) — not yet found to be prior. The nearest comparator is An et al. themselves, who go in the opposite direction — compiling a formula into a folding — and Eppstein (arXiv:2410.07666), who treats ply as an algorithmic parameter rather than as a bound on formula resources. Bounding Boolean formula complexity by physical folding resources was not found.
• Corollary 4 — inherits Theorem 3’s status for the $2^F$ half and Theorem 2’s for the width half.

So the candidate contribution of this memo is narrow and specific: the direction of Theorem 2. Everything geometric in it is inherited. “Not yet found to be prior” is the strongest label authorized, and it is not a novelty claim.

Open: the some-layers case of Theorem 3, and whether $D\le2^F$ survives it.