promoted from data/fprd-lab/fold-look/fold-palindrome-restricted-frontier.md on 2026-07-28 — status: unverified

Bounded-fold incidence run, palindrome frontier. After repair and independent re-audit of the incidence normal form, the midpoint construction is optimal in four pinned coordinates: layer depth, effective fibres, potential sites, and folds. The moved-material proposal remains withdrawn.

The palindrome construction is optimal in four coordinates

Status: the prime-implicant calculation and construction are proved here; the normal-form dependency was independently re-audited for the repaired doctrine. Gate B of the bounded-fold incidence run. The predecessor probe (docs/probes/fold-look-palindrome-probe.md) is closed and unmodified; this memo adds a lower-bound side it did not have. The named predecessor and audit files are not included in this archive.

1. The exact prime-implicant structure

$$\operatorname{MISMATCH}_{2n}(w)=\bigvee_{i=1}^{n}\bigl[w_i\ne w_{2n+1-i}\bigr].$$

Lemma 13. The prime implicants of $\operatorname{MISMATCH}_{2n}$ are exactly the $2n$ width-two terms $$(w_i=0\wedge w_{\bar i}=1),\qquad (w_i=1\wedge w_{\bar i}=0), \qquad 1\le i\le n,\ \bar i=2n+1-i,$$ and every one of them is essential.

Proof. Each listed term is an implicant, and dropping either literal leaves a width-one term consistent with a palindrome, so each is prime.

Conversely let $T$ be an implicant that fixes no pair oppositely. Extend $T$ to a full word: for each pair, if both coordinates are fixed they agree by assumption; if one is fixed, set the other equal to it; if neither, set both to 0. The result is a palindrome consistent with $T$, so $T$ is not an implicant. Hence every implicant fixes some pair oppositely, and by primality is exactly that pair.

Essentiality: the word with a single mismatch at pair $i$, with $w_i=0$, is covered only by $(w_i=0\wedge w_{\bar i}=1)$. $\square$

Consequently, exactly

$$w_{\mathrm{DNF}}=2,\qquad s_{\mathrm{DNF}}=2n,\qquad \ell_{\mathrm{DNF}}=4n .$$

(The value of $s_{\mathrm{DNF}}$ is exact, not merely an upper bound, because all prime implicants are essential and so appear in every exact DNF.)

Machine-checked for $n\le4$: count $2n$, all width 2, all essential, and the computed set equals the closed form above.

2. The restricted frontier

Theorem 14 (corrected after re-audit). Within the literal-local, one-Look strip doctrine $\mathsf{LLFL}$, under the standing hypotheses (GP), (NC), (IN), (UF), and $R>0$, every exact presentation of $\operatorname{MISMATCH}_{2n}$ satisfies $$D\ge 2,\qquad S\ge2n,\qquad P_{\mathrm{sites}}\ge 4n,\qquad F\ge 1 .$$

Proof. Three bounds are direct. The fourth uses the repaired normal form.

$F\ge1$. With $F=0$, $\varphi=\mathrm{id}$ and every fiber is a singleton, so Look is an OR of single literals. $\operatorname{MISMATCH}_{2n}$ is 0 on both the all-zero and the all-one word, so it is not such an OR.

$D\ge2$. $D=1$ makes $\varphi$ injective, giving the same contradiction.

$P_{\mathrm{sites}}\ge4n$. By Lemma 13 there are $2n$ essential prime implicants using $4n$ pairwise distinct literals. Every exact DNF contains every essential prime implicant, each term must carry both literals of its implicant, and the doctrine gives each site exactly one control literal.

$S\ge2n$. $\operatorname{MISMATCH}_{2n}$ is nonconstant, so the repaired Theorem 2 gives $s_{\mathrm{DNF}}\le S$. Lemma 13 gives $s_{\mathrm{DNF}}=2n$. $\square$

2.1 Why $S\ge2n$ was withdrawn and then reinstated

The independent audit exhibited a complete $\operatorname{MISMATCH}_2$ presentation with $F=2$, $D=4$ and $S=1$. Its mechanism is the same one that refuted Theorem 1: the layer through the strip endpoint $x=10$ stops inside a punch image, so locations just past that endpoint are see-through and supply a prime implicant that the fiber test never sees. The full witness is recorded in docs/verify/bounded-fold-incidence-audit.md.

Hypothesis (UF), added to the doctrine in response, excludes that witness. The independent re-audit then confirmed the repaired normal form for $R>0$. Therefore the counterexample lies outside the final doctrine and the nonconstant term-count theorem reinstates $S\ge2n$.

The proposed moved-material bound $W\ge n$ remains withdrawn. Its proof used a cell-based convention not defined by the pinned doctrine. It is retained only in the audit history, not restated as a live proposition here.

3. The construction attains all four

Four coordinates, not five. The construction also moves $n$ cells under one historical convention, but no matching lower bound is claimed for that quantity.

Active holes per input are $2n$, which is not a coordinate with a matching lower bound here and is listed only to keep it distinct from $P_{\mathrm{sites}}$.

A structural corollary, found while auditing the checker rather than by design: the midpoint fold leaves no depth-1 fiber. All $4n$ sites occupy $2n$ fibers of size exactly 2. No site is stranded and no material is wasted, which is why the “admit depth-1 fibers” mutation is vacuous against this construction — the vacuity is the tightness.

4. What is not claimed

• Not universal optimality over arbitrary encoders. The bounds hold within $\mathsf{LLFL}$ with one literal per site and one final Look. A doctrine admitting richer site controls, Cut, Unfold, several Looks, or input-dependent folds is not covered.
• Substrate size $\Lambda$ is not proved optimal. Nothing above bounds material length below; the construction’s $16n$ is a choice, and a denser layout trades material for geometric precision.
• Instruction bits $B$ are not proved optimal.
• The four coordinates are reported as a restricted Pareto point, not as a global frontier: no claim is made that they cannot be traded against one another outside the declared conventions.