Scaffold proof review: Run 01
23 September 2026. Scope: edition inventory, shared model interfaces, and a finite native-model audit. This is not a complete reproof of the four papers.
Contents
Baseline
baseline.json pins the current article bodies and PDF files for:
- Real-time multitape transfer via persistent stacks;
- Direct palindrome scaffolding, Draft 5;
- Persistent scaffold causal algebra;
- Unary scaffold coherence.
These are the current Site editions. The snapshot does not identify which historical files individual reviewers received. No manuscript, paper PDF, theorem status, or existing research note is revised by this run.
The direct paper’s source, PDF, figures, and generated HTML pass scripts/check-direct-palindrome-edition.mjs. The other three routes use expanded HTML paired with explicitly labelled earlier PDFs. Their next revisions need matching numbered editions from one maintained manuscript.
Verified example: base versus missing
LMR Definition 11 sets the radius-zero view of a node to its label and the view of a missing endpoint to the empty symbol. Thus the unlabelled base and a missing endpoint agree at radius zero. At radius one the base is a tuple containing its empty label and missing children, and is distinguishable.
Take degree one, distance two, an unlabelled base 0, and a labelled top 1. In graph A, top port 0 targets the base. In graph B it is missing. Under shortcut closure for source words 0 and 00, the two port rows are:
| Graph | Shortcut 0 |
Shortcut 00 |
|---|---|---|
| A | base | missing |
| B | missing | missing |
The compiled radius-one views coincide. The source radius-two views differ. The compiled radius-two views distinguish the graphs and reconstruct both source views exactly. This refutes the stronger radius-one reconstruction sentence in T160, while supporting its stated radius-two construction.
The causal paper’s Section 3.2 defines a port-word observation with distinct UNLABELLED and missing values. Its proof of Theorem 3.6 identifies a native depth-m neighbourhood with the restriction through words of length m. The example shows why that exact finite-depth identification needs attention. It does not refute equality of observations at every depth. R02 must state the precise comparison and inspect every use of a fixed numerical radius.
Executable evidence
verify_native_structural_normal_form.py has a graph interpreter, but its compiled transition core receives only an unfolded radius-two tree. It does not read node identities or test pointer equality. The base is an actual unlabelled node with all ports missing.
The recorded output verifies:
- 24 source machines, with all binary inputs through length seven;
- 6,120 runs and 36,912 transitions for each of the T160/T161 constructions;
- 86,064 native-view reconstructions and 43,032 prefix-acceptance checks;
- 2,263 source-path visits to the base;
- 1,130 legal small backward graphs, yielding 38,316 further reconstruction checks across historical control assignments and distances;
- 1,296 ordinary label/control code round trips;
- the radius-one collision above and detection of an empty-graph substitution.
These are finite checks. The generic proof and the impact on companion arguments remain separately reviewable obligations. The earlier T161 checker reserved code space for the base but executed an empty-graph variant; its reported base-code count is not evidence of native initial-node execution.
Cross-paper dependency notes
| Interface | Observation in Run 01 | Next obligation |
|---|---|---|
| Persistent-stack decoder | Base and missing both decode to the empty stack; the update uses the CleanEmpty invariant and distance two. | Check the invariant at every boundary; no counterexample to this compiler was found in this run. |
| Finite view / full unfolding | Causal Section 3.2 distinguishes base and missing in its endpoint alphabet. | Prove the exact finite-depth comparison and trace resource-sensitive uses. |
| Simultaneous-record initialization | Direct Theorem 10.2 explicitly handles a fixed immutable pointer-closed initial graph through virtual records; causal Theorem 9.2 presents the dynamic packing argument. | Compare the declared source models and initial configurations before deciding whether text must change. |
| Direct application | Draft 5 states a sequence contract; causal Example 9.6 describes the companion application as supplied. | Match the exact hypotheses and evidence in those editions. |
| Unary coherence | Its unary restriction is one port and distance one. | Keep this distinct from T161’s one working label with potentially many ports; inspect inherited observation and guard assumptions. |
| PEG transfer | The classical transfer and direct receipt routes have different premises. | Preserve the reversal direction and trace a finding only along actual dependencies. |
The Lab’s T90 remains recorded as a source-verified proof with mechanized compiler composition. This run makes no new certification or status change to that proof, and an unfinished direct-route audit does not reopen it.
Source attribution
Loff, Moreira, and Reis, The computational power of parsing expression grammars, arXiv:1902.08272, Definitions 10–15 and Theorem 16. Their PEG-to-scaffold construction already specifies one working label and two controls. A quantitative direct compiler should be compared against that construction, rather than credited with discovering the qualitative alphabet/control reduction.
Handoff
Next: R02, the exact finite-observation comparison. Record the lemma, its boundary cases, each affected citation or radius calculation, and the scope of any necessary change. Then continue with initialization and the sequence contract. Paper revisions follow a completed impact assessment and produce matching numbered PDF and HTML editions with a short change history at the end.