promoted from data/fprd-lab/causal-track/virtual-crease-causal-width-audit.md on 2026-07-28 — status: unverified

Capture and independent audit of the review lane’s virtual-crease causal-track theorem chain (T1-T5). All five confirmed by independent implementation. Audit output is a location of hypotheses: the 2^r selector separation uses pre-query placement and the absence of random-access placement; ordinary birth is not automatically random access. The offline Dilworth theorem tacitly grants free initial positioning, which is exactly what the causal theorem charges; spacing r+1 is load-bearing. Two received statements were garbled and the reconstructions are marked.

Virtual-crease causal-width chain: capture and independent audit

Provenance. The five theorems below were produced by the review lane (ChatGPT), not by this lab. They are captured here so they can be cited and attacked from outside. The audit, the adversarial probes, and every reconstruction note are this lane’s work.

Status. All five statements are confirmed by independent implementation. The audit’s substantive output is not a refutation but a location of hypotheses: §3 identifies which axiom each result actually rests on, and one of them changes how the headline should be read.

Doctrine separation, enforced. This memo concerns the virtual causal-track doctrine only. It makes no contact with the physical-folding doctrine, asserts no claim that PEGs are folding machines, that virtual schedules are physically foldable, or that the selector theorem lower-bounds any PEG recognizer.

1. The chain, as captured

T1 — stationary lineage. For an even-palindrome prefix $x$ of length $T$, $$S_{T+1}(xb)=\{T+1\}\cup\{r-1:r\in S_T(x),\ r\ge1,\ b=x_{r-1}\},$$ and a surviving candidate’s virtual axis $\chi_T(r)=\tfrac{T+r-1}{2}$ is stationary.

T2 — causal order and Dilworth. Query events obey $(t,p)\preceq(t',p')\iff t\le t',\ p'\le p,\ p-p'\le t'-t$. Under $X=(t+p)/2,\ Y=-p/2$ this is ordinary two-dimensional dominance, so minimum offline persistent tracks equal the poset width.

T3 — offline width is not causal demand. An explicit width-two event family forces three tracks online.

T4 — exponential selector separation. With $r$ future bits selecting a leaf $z$, no earlier demand, leaf address $q(z)=(r+1)\,\mathrm{value}_2(z)$, tracks existing before the bits arrive and able only to hold or recede one address per step: every completed path has width $1$, while exact causal demand is $2^r$.

T5 — one formed comb. For $\{U^jV\}$ with $\ell=|U|$, the two discriminating roles use constant old addresses $p^0=2c_0-h$ and $p^1=2c_0-h+\ell$, so one comb reuses two roles and does not realize the balanced late-selector obstruction.

2. Audit results

Independent implementations throughout; the review lane’s checker was not consulted or re-run, since re-running it would establish nothing. tools/checks/audit_causal_track_chain.py.

2.1 Two reconstruction notes

T1’s statement arrived garbled — the candidate set was transmitted as “$r\in\{0,\dots,T\}\equiv T\pmod 2,\ x[r]\in\mathrm{PAL}_{\mathrm{even}}$”, which is not parseable. The reconstruction tested is

$$S_T(x)=\{r: r\equiv T\ (\mathrm{mod}\ 2),\ x[r{:}T]\in\mathrm{PAL}_{\mathrm{even}}\},$$

derived by requiring $x\cdot\mathrm{rev}(x[0{:}r])$ to be an even palindrome: positions inside the completion match automatically, and the residual condition is exactly that the middle segment $x[r{:}T]$ be a palindrome. Under this reading the recurrence is exact. If the intended definition differs, the T1 verdict does not transfer.

T5’s constant $h$ was also garbled (“$h=\max\{r\le|V|=U^\omega[0]\}$”). The constancy conclusion is insensitive to it — $p^0=2c_0-h$ is constant in $j$ for any fixed $h$ — so the verdict stands, but the definition of $h$ is not audited.

2.2 A minor redundancy

In T2 the clause $t\le t'$ is implied by the other two: $p'\le p$ and $p-p'\le t'-t$ give $t'-t\ge0$. Verified exhaustively. Harmless, but the order has two independent constraints, not three, which is what makes the two-coordinate dominance form exact rather than a projection.

3. Where the results actually rest — the audit’s real output

3.1 The exponential uses pre-query placement and no random-access placement

This is the finding that matters for how T4 should be stated.

The theorem’s doctrine places all tracks before the selector is read and forbids teleportation or jump-launch. If a model permits random-access placement directly at $q(z)$ when the leaf is reached, demand collapses from $2^r$ to $1$. Ordinary birth is not, by itself, that operation: a new track whose starting point is still constrained by the same travel cone reaches at most one of the spaced targets. The exact $2^r$ theorem remains stated for pre-placed tracks; variants with birth require a separately pinned placement rule and are not settled here.

That is a legitimate and interesting doctrine — and naming it correctly makes the theorem stronger, not weaker:

Without random access, a late-bound selection over $2^r$ sufficiently separated addresses costs $2^r$ units of standby hardware, even though every completed run needs one.

Stated as “late binding is exponentially expensive” it invites the objection that a real recognizer just allocates a pointer. The precise statement is that random-access placement is the operation excluded by the pinned theorem; a different allocation discipline defines a different doctrine.

This lane notes, without drawing any bridge between the doctrines, that the same axis — what a model gets for free in addressing — was the operative question in the physical-folding audit. The two doctrines remain separate; the methodological point is that “which addressing powers are free” is where these resource claims live.

3.2 T2 and T4 differ precisely over free initial positioning

The offline Dilworth theorem tacitly grants free initial positioning: a chain beginning at $(t,p)$ needs a track that was somewhere legal at time 0, and since a track at $a$ covers $[a-t,a]$, such an $a$ always exists. Verified: the constraint is never binding, so it is invisible offline.

T4 charges exactly that. So the offline/causal gap is not an artifact of online scheduling difficulty in general — it is one specific resource (pre-positioning across counterfactual futures) that the offline formulation silently gives away. That is the cleanest statement of what T3 and T4 jointly establish, and it is stronger than “online is harder than offline.”

3.3 Two hypotheses of T4 are load-bearing, and one is only a hypothesis

Spacing. The separation $r+1$ is not decorative. Reduced to $r$, the capacity lemma fails for every $r\in[2,8]$ — a track’s window then holds two targets and the counting argument collapses. Checked directly.

No demand before the leaf. This licenses free root placement and hence the upper-bound construction. With an earlier demand pinning the tracks, the $2^r$-track policy is not established by the given argument. Recorded as a hypothesis; nothing here shows the theorem fails without it, only that the proof does not cover it.

3.4 The linear-width trap is real

On $w=0^N$ the literal comparison set has width growing linearly (measured: 2, 4, 6, 8 at $N=4,6,8,10$) while the residual is a single trivial periodic family. The review lane flags this itself; the audit confirms it is not hypothetical. Any residual object proposed for the factorization theorem must not inherit this width, and that is the sharpest available test of a candidate object — it is cheap to run and it kills the obvious wrong answers.

4. What is not claimed

• No verdict on the residual–causal-track factorization theorem, which is the review lane’s to attack. This memo does not construct a residual object and does not select an abstraction.
• No claim that any of T1–T5 lower-bounds a PEG recognizer, a palindrome recognizer, or any presentation outside the pinned no-teleport track doctrine. T4 is exact for a specified demand tree; universality is exactly what the missing factorization theorem would supply and does not follow from anything audited here.
• No priority claim. Dilworth’s theorem, two-dimensional dominance, and online chain partition are classical; what is captured is their instantiation in this doctrine.
• Finite-horizon tabular feasibility is kept separate from a single finite, horizon-independent presentation, as the doctrine requires. The scenario-tree assignment used in T4 is a finite tabular object and is not a presentation.