Automata and formal languages · ongoing review

Scaffold proof review

This activity checks four related papers together. It follows the assumptions that pass between constructions, separates verified examples from unresolved proof questions, and prepares consistent editions when a revision is justified.

The papers and their interfaces

Paper	Role	Review focus
Real-time multitape transfer	Parallel stacks, tape simulation, classical palindrome application	Native base, empty stacks, strict timing, and reversal
Direct palindrome scaffolding	Receipt recurrence, simultaneous records, sequence interface	Virtual initialization, pointer origins, and the sequence contract
Causal scaffold algebra	Behavioral observations, history transformations, general batch compiler	Finite views versus full behavior; compiler and companion-paper hypotheses
Unary scaffold coherence	Guarded transformations of degree-one histories	Inherited observation equivalence, base termination, and move guards

The transfer paper supplies the classical-recognizer route to even palindromes. The direct paper develops the receipt route with its stated sequence contract. The causal paper supplies related compiler and observation machinery; the unary paper studies guarded transformations in a restricted history model. These are distinct dependencies, so a finding in one route must be traced before changing conclusions elsewhere.

Run 03: initial records and the compiler contract

The direct paper now keeps fixed initial records in a finite decoder table. The causal compiler still leaves its initial configuration unspecified. Its one-step argument needs an explicit base case before it supports a whole-run application using those records. The transfer and unary papers have separate native-base constructions; this finding alone does not change their conclusions.

Initialization, receipt closure, sequence-contract assurance and history, native observation semantics, transfer composition, unary guard geometry, and their immediate cross-paper dependencies.

INIT-01: Direct palindrome · Definition 10.1 and Theorem 10.2

Classification: Proof construction and resource accounting.

Earlier: Draft 2 says a fixed finite initial object can be materialized in the first batch.

Current: Draft 5 keeps fixed, finite, immutable, pointer-closed initial records in a virtual decoder table from time zero.

The new construction avoids charging initial records against the per-letter fresh-slot bound. It explicitly supplies the initial simulation case.

Retain this change in the cumulative version history; align the causal compiler's initialization contract before its next edition.

Direct Draft 2 source · Direct Draft 5

INIT-02: Direct and causal compilers · Direct Theorem 10.2; causal Theorem 9.2

Classification: Parameter-domain qualification.

Earlier: The causal compiler states degree d=s+Aq without an explicit positive-degree qualification in its batch definition.

Current: The direct compiler now states d=max{1,s+Aq}.

These bounds agree when s+Aq is positive. A permitted all-zero parameter tuple needs a dummy port in the positive-degree scaffold convention.

Make the parameter domain or dummy-port convention explicit in the coordinated edition; this does not change a nondegenerate construction's bound.

Direct Draft 5 · Causal current HTML

INIT-03: Causal scaffold algebra · Definition 9.1, Theorem 9.2, Theorem 9.4, Proposition 9.5

Classification: Unstated initial-state contract.

Earlier: The preserved Draft 3 compiler describes dynamic node-slot pointers and proves the step assuming the old heap already decodes correctly.

Current: The current HTML retains that proof without specifying the source initial roots or a virtual initial-record case.

The local batch argument does not itself choose an initial source configuration. With missing initial roots it has the usual base case; an application using a fixed initial graph needs the explicit virtual-table contract.

State the intended initial model and trace it through staging and feedback. This is an initialization obligation, not a counterexample to the local simultaneous-batch step.

Causal Draft 3 source · Causal current HTML

INIT-04: Real-time multitape transfer · Parallel-stack compiler and tape reconstruction

Classification: Separate base-case dependency.

Earlier: The synchronized source interprets the native base as empty stacks; tape reconstruction starts with empty left/right lists and a blank scanned symbol.

Current: The current HTML retains that explicit base case.

This route does not invoke the direct paper's fixed-heap batch initialization. No transfer-theorem change follows from INIT-01 or INIT-03 alone.

Preserve the separate proof route. Its other timing and observation obligations remain in their own review packages.

Transfer synchronized source · Transfer current HTML

INIT-05: Unary scaffold coherence · History model and coherence theorem

Classification: Separate history-model dependency.

Earlier: Draft 1 studies degree-one histories beginning at the distinguished unlabelled base.

Current: The current HTML retains that history model rather than invoking a source-record batch initializer.

The fixed-initial-heap change does not directly alter the objects of the unary theorem. Its inherited observation and guard assumptions are separate obligations.

Do not transfer the direct compiler's initialization issue to unary coherence without a dependency; continue the observation/guard review separately.

Unary Draft 1 source · Unary current HTML

A finite audit checked 143,325 two-step plans with virtual initial records. It supports the initialization construction, not a complete proof of the compiler or its sequence client. The table avoids extra physical allocation, but its size still contributes to the finite description of the compiled machine.

Argument, scope, and next comparison · Initialization checker · Recorded output

Run 04: what Draft 2 repaired

Draft 2 made two mathematical changes to the direct palindrome paper. It repaired the last cell of the receipt-rope proof with a separate mirror-prefix lemma. It also added a transition receipt to each direct record entry, turning a potentially unbounded suffix-link search into one stored lookup.

RCPT-01: Direct palindrome · Receipt-rope recurrence and mirror-prefix lemma

Classification: Proof repair.

Earlier: The expanded Draft 1 applies the bridge-shadow lemma to every cell of the retained bridge-block tail.

Current: Draft 2 applies bridge shadow only through the proper prefix of that tail and proves the last receipt separately with the mirror-prefix lemma.

At the last cell, the strict proper-suffix condition used by bridge shadow has reached its boundary. The added endpoint lemma proves the needed equality without that hypothesis. The recurrence itself survives with a repaired proof.

Record this as a substantive proof repair in the cumulative edition history, with the earlier Draft 1 argument preserved as superseded.

Direct expanded Draft 1 · Direct Draft 2 · Direct Draft 5

RCPT-02: Direct palindrome · Occurrence-record layout and internal update

Classification: Representation and bounded-access repair.

Earlier: Expanded Draft 1 gives each letter entry a direct/reset rope root but does not give the internal update a bounded pointer to the selected D_c record.

Current: Draft 2 adds an occurrence-indexed transition receipt to every direct entry. The bridge entry points to the suffix-link record; every other entry copies the corresponding receipt from that record.

Without this field, an internal update may require an unbounded suffix-link chase. The added receipt materializes that recursion when the record is created and makes the target one entry lookup away.

Treat the record-layout change as part of the mathematical construction, not as an explanatory addition. Keep the transition receipt in every future edition and theorem invariant.

Direct expanded Draft 1 · Direct Draft 2 · Direct Draft 5

RCPT-03: Causal scaffold algebra · Receipt knot, Theorems 9.2 and 9.4, Proposition 9.5, Example 9.6

Classification: Companion dependency.

Earlier: The causal paper uses the palindrome receipt knot as motivation for its simultaneous finite-batch compiler.

Current: Its current Example 9.6 explicitly assigns the receipt recurrence, source implementation, resource certificate, and whole-client normalization to the companion paper.

The corrected endpoint receipt supplies the concrete owner-cycle witness, and the transition receipt is needed by the companion client's bounded access. The generic simultaneous-batch and opaque-staging theorems do not depend on those palindrome facts; the application does.

Keep the generic theorem and companion application separated. In the eventual causal edition, cite the numbered companion edition whose receipt proof and source contract are actually being used.

Causal Draft 3 source · Causal current HTML · Direct Draft 5

RCPT-04: Transfer and unary coherence · Dependency boundary

Classification: No direct dependency found.

Earlier: The transfer theorem derives EPAL through the classical real-time recognizer; unary coherence studies guarded moves on scaffold histories.

Current: Those proof routes remain structurally separate from the direct receipt recurrence and occurrence-record layout.

The Draft 1 receipt gaps and their Draft 2 repairs do not propagate into the transfer compiler or unary coherence theorem. This does not certify their other proof obligations.

Do not attach receipt-repair conclusions to these papers. Continue their timing, observation, and guard audits in the corresponding work packages.

Transfer current HTML · Unary current HTML

The causal paper uses these facts only in its palindrome application. Its generic finite-batch compiler remains separate. The transfer and unary papers do not use the direct receipt recurrence. These dependency findings do not certify their other proof obligations.

Detailed comparison and dependency trace · Targeted checker · Recorded output

Run 05: contract, implementation, and certificate

The direct paper's recognition theorem is conditional on the sequence contract in Section 11.1. Its whole-client normalization theorem closes the composition step for any client meeting those hypotheses. Appendix D separately presents the pinned OCaml work as informal source-level evidence, not as a complete automated source-to-scaffold certificate.

The source analysis is substantial: its checkers cover three typed units, 3,912 expressions, 454 direct calls, 81 bindings in the cat closure, and all 952 constructor slots. But 474 polymorphic source sites still require contextual specialization. No old/fresh interpretation has executed, and the numerical access radius remains withdrawn.

SEQ-01: Direct palindrome · Section 11.1, Theorem 12.2, and Corollary 12.3

Classification: Explicit theorem hypothesis.

Earlier: Earlier source audits sometimes described a particular catenable-deque variant and numerical resource bounds as the implementation bridge.

Current: Draft 5 states the recognition theorem for any persistent sequence implementation satisfying the Section 11.1 contract and uses symbolic resource bounds.

The proved construction is conditional on a sequence contract. It is not stated as an unconditional source-to-scaffold theorem about the pinned OCaml program.

Preserve the condition in every abstract, result page, citation, and companion application. Do not reintroduce withdrawn numerical radii without a provenance proof.

Direct Draft 5

SEQ-02: Direct palindrome · Theorem 11.3 and Appendix D

Classification: Assurance boundary.

Earlier: The whole-client normalization repair closed the composition gap isolated by the earlier end-to-end audit, conditional on source-resource premises.

Current: Draft 5 retains the generic normalization theorem and separately calls the pinned OCaml analysis informal source-level evidence.

Whole-client normalization is no longer the open seam. Complete old/fresh pointer provenance for the concrete implementation remains below a complete automated source certificate, while qualitative finite access is argued informally.

Describe the theorem and implementation evidence as distinct. Continue the provenance work as assurance strengthening, not as if the normalization theorem itself were missing.

Direct Draft 5

SEQ-03: Causal scaffold algebra · Example 9.6 and companion discussion

Classification: Cross-paper assurance mismatch.

Earlier: The causal application says the companion supplies an explicit strict source-record implementation, its resource certificate, and whole-client normalization.

Current: The linked current companion distinguishes a conditional abstract theorem from informal source evidence and withdraws its numerical access certificate.

The causal wording is stronger than the companion's current assurance language, although the example also limits its conclusion to the companion's stated abstract model.

In the next coordinated causal edition, refer to the sequence contract, symbolic resource existence, and informal implementation evidence at their stated levels. This does not alter the causal paper's generic compiler.

Causal current HTML · Direct Draft 5

SEQ-04: Causal scaffold algebra · Reference [9]

Classification: Edition-reference mismatch.

Earlier: The bibliography identifies the direct companion as Draft 4 corrected, dated 10 September 2026.

Current: The link now resolves to the maintained Draft 5 paper dated 21 September 2026.

A reader cannot tell from the reference whether the application relies on Draft 4 or Draft 5, whose theorem hypotheses and evidence boundary differ.

Pin the exact companion edition in the next matching causal PDF/HTML release and preserve the earlier reference in the cumulative history.

Causal current HTML · Direct Draft 5

SEQ-05: Transfer and unary coherence · Dependency boundary

Classification: No direct dependency found.

Earlier: The transfer proof uses a classical real-time palindrome recognizer; unary coherence concerns guarded transformations of degree-one histories.

Current: Neither proof route invokes the direct paper's catenable-sequence implementation evidence.

The source-certificate assurance issue does not propagate into these two proofs. Their separate timing, observation, and guard obligations remain open to their own review packages.

Keep the direct sequence-contract review scoped to the direct and causal palindrome application unless a new dependency is found.

Transfer current HTML · Unary current HTML

The causal paper's generic compiler is unaffected. Its palindrome example is limited to the companion's abstract model, but its phrase “explicit strict source-record implementation” is stronger than the companion's current evidence description. Its reference also still names Draft 4 while the link resolves to Draft 5. Those are coordinated-edition issues, not newly found counterexamples.

Detailed assurance and dependency comparison · Statement checker · Recorded output

Run 06: how the sequence claim changed

The history is not one uninterrupted theorem claim. The direct paper first claimed the result, then withdrew it after a source audit, kept it withdrawn while the implementation bridge was narrowed, and restored it only after proving whole-client normalization in an abstract source-record model.

The causal paper changed from an open companion application to stronger implementation-and-certificate language at the same source change that restored the direct theorem. The direct paper later withdrew its numerical radius after a mutation attack and Draft 5 separated the conditional theorem from informal source evidence more sharply. The causal wording did not absorb those later assurance changes.

SHIST-01: Direct palindrome · Expanded reading edition at source commit 473e2ff4

Classification: Earlier theorem claim.

Earlier: The paper claimed Theorem 12.2 while treating the modern deque implementation as comparison evidence rather than a proof premise.

Later: Later source audits separated the abstract sequence contract from evidence about a particular implementation.

The early proof crossed from Kaplan-Tarjan's worst-case sequence theorem to the stronger finite-record, opacity, and bounded-address interface without a complete explicit bridge.

Preserve this snapshot as a superseded theorem claim and include it in the cumulative version history. Do not describe the later conditional formulation as if it had always been present.

Direct expanded edition before source audit

SHIST-02: Direct palindrome · Source-audit changes bdf02f42 and 3002d210

Classification: Transitional qualification followed by theorem withdrawal.

Earlier: The first source-audit edit qualified the opening but temporarily retained the old Theorem 12.2 label in the body.

Later: The next source change explicitly marked the theorem and corollary withdrawn pending the sequence bridge and complete client audit.

The first edit was an internally inconsistent transitional snapshot. The second edit completed the status correction. Both exact artifacts are retained.

Treat 3002d210 as the completed withdrawal point. Do not collapse the transitional and completed edits into one undocumented revision.

Transitional qualified snapshot · Explicit withdrawal snapshot

SHIST-03: Direct palindrome · Fixed-layout and end-to-end audit changes b6fc2e74 and 9a5ba94f

Classification: Bridge narrowing while theorem remained withdrawn.

Earlier: The theorem was withdrawn with both implementation and client-resource obligations open.

Later: A fixed record layout and resource analysis narrowed the remaining gap to whole-client source-to-plan normalization.

These changes supplied real construction evidence, but the paper correctly kept the assembled theorem withdrawn until the identified composition step was proved.

Record the source-resource work and the normalization gap separately; neither should be erased by the later restoration.

Fixed-layout resource snapshot · End-to-end audit snapshot

SHIST-04: Direct and causal palindrome application · Whole-client normalization change a53006fa

Classification: Conditional theorem restoration and companion update.

Earlier: The direct theorem and causal application were both presented as open at the whole-client normalization seam.

Later: The direct theorem was restored in a stated abstract source-record model, and the causal paper simultaneously changed to say that implementation, resource, and normalization obligations had been supplied.

The current causal wording originated at the direct theorem's restoration stage. At that point the direct paper still displayed numerical bounds whose weakest premises were manual address arguments.

When citing this stage, state the abstract-model and manual-premise qualifications. Preserve the causal update as historically contemporaneous, not an independent certification.

Direct restoration snapshot · Causal companion update

SHIST-05: Direct and causal palindrome application · Radius-certificate withdrawal cef6bbd7 and later direct checks

Classification: Assurance rollback not propagated to companion wording.

Earlier: The restored direct edition advertised concrete operation radii and scaffold distance; the causal companion referred to a supplied resource certificate.

Later: A mutation attack invalidated the path checker as a proof of source coverage and old/fresh provenance. The direct paper withdrew the numerical radius but retained a qualitative conditional theorem; the causal wording stayed unchanged.

This is the historical source of the current cross-paper assurance mismatch. It narrows numerical and implementation certification, not the direct paper's abstract conditional theorem or the causal generic compiler.

Align the causal wording in its next numbered edition and do not restore numerical bounds without a complete provenance argument.

Direct radius-withdrawal snapshot · Causal text retained from restoration stage

SHIST-06: Direct and causal palindrome application · Direct Draft 5 and current causal reference

Classification: Current edition alignment.

Earlier: Several September source snapshots alternated among theorem claim, withdrawal, abstract-model restoration, and numerical-certificate rollback.

Later: Draft 5 consolidates the direct theorem as conditional on Section 11.1 and labels concrete source evidence informal. The causal paper retains restoration-stage wording and a Draft 4 citation whose link resolves to Draft 5.

The current direct theorem status is not withdrawn. The current mismatch is that the causal companion description and edition reference do not match Draft 5's assurance boundary.

Use matching numbered PDF and HTML editions for the future repair, with a concise cumulative history at the end. Leave all current paper files unchanged during review.

Direct Draft 5 · Causal current HTML

The withdrawal is part of the historical record, not the current theorem status. The current direct theorem is conditional on its sequence contract. The unresolved stronger claim concerns a complete concrete old/fresh provenance and numerical access certificate. No paper or PDF was changed in this review run.

Chronology, interpretation, and scope · History checker · Recorded output

Run 07: native views and port-word observations

Let $P_m$ record the endpoint of every port word through length $m$ , distinguishing a working-labelled node, the unlabelled base, and a missing endpoint. Let $N_m$ be LMR's native radius- $m$ neighbourhood. The exact relation is

N_m=\tau_m(P_m),\qquad P_m=P'_m\Rightarrow N_m=N'_m,\qquad N_{m+1}=N'_{m+1}\Rightarrow P_m=P'_m.

The truncation $\tau_m$ is recursive. At the outer frontier it keeps only the endpoint label, so a path reaching the unlabelled base exactly at depth $m$ and a path becoming missing there have the same native leaf. One additional native layer distinguishes them.

\forall m\;N_m=N'_m \quad\Longleftrightarrow\quad \mathcal U=\mathcal U'.

Therefore causal Theorem 3.6's all-depth equivalence, bisimulation characterization, continuation stability, and distance-two separator remain valid. Two explanatory proof sentences identify the observations at the same radius and need the truncation statement above instead.

OBS-01: Causal scaffold algebra · Sections 2.3 and 3.2; proof of Theorem 3.6(1)

Classification: Finite-depth model alignment.

Earlier: The paper says that the native depth-m neighbourhood is exactly the unfolding restricted to port words of length at most m.

Exact result: The native view is the recursive truncation of that port-word table. At the outer frontier it identifies an unlabelled-base endpoint with a missing endpoint; one additional native layer recovers the distinction.

At fixed equal depth the two observations are not identical. Port-word equality through m implies native depth-m equality, while native depth-(m+1) equality implies port-word equality through m.

Replace the same-radius identification with the recursive truncation and one-layer comparison in the next coordinated edition.

Causal current HTML

OBS-02: Causal scaffold algebra · Theorem 3.6 and dependent behavioral results

Classification: Theorem survives with proof repair.

Earlier: The proof derives the all-depth equivalence from the false same-depth identity.

Exact result: Equality at every native depth is equivalent to equality of full unfoldings: a base-versus-missing difference reached by a word of length r appears natively at depth r+1.

The theorem statement, bisimulation equivalence, continuation stability, distance-two separator, minimal figures, and later full-behavior results remain valid. The required repair is local to the finite-depth comparison.

Preserve the theorem and supply the corrected two-implication proof in the next numbered edition; do not describe this as a retraction.

Causal current HTML

OBS-03: Unary scaffold coherence · Behavioral figures, terminal cases, and Theorem 8.1

Classification: No theorem dependency on same-radius identity.

Earlier: The unary paper inherits full behavioral figures from the causal paper and separately fixes degree one and distance one.

Exact result: Its arguments continue to use full residual behavior, physical endpoint guards, and distinct missing, base, and recursive terminal cases.

No use of the false claim that native radius one equals the port-word endpoint table through length one was found. The all-depth behavioral equivalence it inherits remains valid.

Make no unary theorem change from this finding. Keep the observation clarification in the causal dependency chain.

Unary current HTML · Causal current HTML

Dependent result	Impact
Causal results after Theorem 3.6	Survive; they use full behavior, bisimulation, or physical endpoints.
Unary coherence	Survives; its missing, base, and recursive terminal cases remain distinct.
FPRD-T153 through T159	Survive; the radius-sensitive claims use native recursive views.
FPRD-T160	The theorem survives, but reconstruction requires its existing radius two, not radius one.
FPRD-T161	Survives unchanged; it already uses one shortcut hop plus one marker hop.

The finite audit checked 27,560 recursive truncations across 6,890 chronological scaffolds, stable behavioral partitions on 32,644 states, and explicit frontier witnesses through depth four. The recursive proof supplies the unbounded statement. No paper or PDF was changed.

Proof and dependency trace · Finite checker · Recorded output

Run 08: the exact simultaneous-record compiler interface

A bounded simultaneous record transducer compiles exactly when its initial data and per-letter plan meet one explicit contract: fixed finite pointer-closed initial records, bounded labelled rooted observations, no branch on pointer identity, and bounded simultaneous targets.

d=\max\{1,s+Aq\},\qquad k\le r+1.

The direct paper's Theorem 10.2 already states this form. The causal paper's Theorem 9.2 has the correct tuple-packing step, but a future edition should add the fixed virtual initial-table base case and either use the maximum above or assume $s+Aq>0$ .

The identity restriction is exact. A scaffold transition factors through finite control, the input letter, and its native finite view. One old node shared by two ports and two distinct but behaviorally identical old nodes can have the same view at every depth, so unencoded alias identity is unavailable to the transition. A fixed plan still preserves the alias: copied paths converge in the shared case and remain separate in the split case.

COMP-01: Direct palindrome · Definition 10.1 and Theorem 10.2

Classification: Complete compiler interface.

Before: The review had separately identified the virtual initialization and positive-degree repairs without closing the whole interface comparison.

Exact result: The theorem uses fixed finite immutable pointer-closed initial data, degree max{1,s+Aq}, distance r+1, bounded labelled rooted observations, and no pointer-identity branch.

These clauses give the virtual base case and one-step commuting square needed for exact whole-run simulation. The current direct theorem already states them.

Use the direct theorem as the aligned reference statement. Make no paper change from this finding.

Direct Draft 5

COMP-02: Causal scaffold algebra · Definition 9.1, Theorem 9.2, and Proposition 9.5

Classification: Theorem survives with two boundary clauses.

Before: The compiler states d=s+Aq and begins its induction by assuming that the old physical heap already decodes correctly.

Exact result: The exact whole-run form either restricts initial roots to missing or adds the fixed virtual initial table, and uses max{1,s+Aq} unless s+Aq>0 is assumed.

The dynamic tuple-packing and same-step feedback arguments are correct. The missing items are a base case and a degenerate-parameter convention, not a counterexample to the compiler.

Add the two clauses in the next coordinated numbered edition and propagate the chosen initial convention to Proposition 9.5.

Causal current HTML · Direct Draft 5

COMP-03: Direct and causal compilers · Source-to-scaffold observation boundary

Classification: Exact alias-observability boundary.

Before: Pointer identity was excluded as a hypothesis, but the operational reason and preservation distinction were not isolated in the review.

Exact result: A scaffold action factors through finite control, the input letter, and its native finite view. Shared and duplicated bisimilar targets have identical native views, so alias identity is not observable unless explicitly encoded.

The compiler cannot branch on unencoded pointer equality, but it does preserve aliases when a fixed source plan copies the corresponding old addresses. Observation and preservation are different claims.

Retain the no-identity hypothesis. If a future source program needs equality, encode the required distinction in finite labels or another observable coordinate.

Direct Draft 5 · Causal current HTML

COMP-04: Transfer and unary coherence · Initialization dependency boundary

Classification: No direct dependency.

Before: The transfer and unary papers were included in the cross-paper compiler audit.

Exact result: The transfer compiler initializes empty stacks from the native base, while unary coherence starts from native base histories; neither invokes a fixed virtual record heap.

The record-compiler initialization clauses do not change either theorem. Their timing, reversal, observation, and guard obligations remain separate.

Carry no compiler correction into these papers; continue with R05's independent checks.

Transfer current HTML · Unary current HTML

The alias witness was checked through native depth eight, and the earlier virtual-initialization audit contributes 4,095 first-step and 143,325 two-step checks. The general result is the factorization and compiler proof, not the finite test. Transfer and unary results are unaffected. No paper or PDF was changed.

Proof and cross-paper disposition · Finite checker · Recorded output

Run 09: timing, reversal, and the empty word

The transfer route is an exact composition of two different steps. The machine-to-scaffold compiler reads the same word and performs one source transition and one scaffold append per input symbol. The scaffold-to-PEG theorem then introduces one reversal.

A_M(w)=M(w),\qquad G_M(x)=A_M(x^R)=M(x^R).

Therefore the PEG language is exactly the reverse of the source machine language. The reversal is not hidden in the tape zipper or stack compiler. For even palindromes it disappears because $\mathsf{EPAL}_2^R=\mathsf{EPAL}_2$ .

The timing boundary is equally exact. The compiler preserves a source machine that already makes one global transition per input symbol. It does not compress a slower controller into strict real time. Empty input is preserved throughout: zero source steps, zero scaffold appends, the copied initial acceptance bit, and $\varepsilon^R=\varepsilon$ .

TRANS-01: Real-time multitape transfer · Definitions 2.3 and 4.1; Theorem 4.2; Lean realtime_transfer_decides

Classification: Exact timing interface.

Before: The review package still listed strict timing as an unchecked boundary of the transfer route.

Exact result: One source transition, one zipper update on each fixed stack pair, and one scaffold append occur for each input symbol. No post-input step is inserted.

The compiler preserves strict real time letter for letter. It does not compress a slower or growing-microtime source computation into one scaffold transition.

Close the compiler timing obligation. Keep source-machine strictification as a separate premise in each application.

Transfer current HTML

TRANS-02: Real-time multitape transfer · Theorem 5.1; Lean scaffold_to_peg and revRT_multitape_subset_PEG

Classification: Exact reversal orientation.

Before: The machine-to-scaffold and scaffold-to-PEG directions had not been isolated in the cross-paper review.

Exact result: The machine-to-scaffold compiler decides the same word, while the scaffold-to-PEG theorem recognizes x exactly when the scaffold accepts reverse(x).

Exactly one reversal enters the composition, at the LMR sufficient direction. Thus the PEG language is the reverse of the source-machine language.

Retain the current theorem orientation. For reversal-invariant applications such as even palindromes, state explicitly that this one reversal fixes the language.

Transfer current HTML

TRANS-03: Real-time multitape transfer · Lemma 2.2; Theorems 4.2 and 5.1; Section 6

Classification: Empty-input preservation.

Before: Empty-input handling appeared in several local statements but had not been followed through the full composition.

Exact result: The source machine and scaffold perform zero steps, normalization copies initial acceptance, reversal fixes the empty word, and the PEG theorem covers all finite words.

The empty word is preserved without an endmarker, cleanup phase, or artificial first transition. The even-palindrome application accepts it through the same interface.

Close the empty-input obligation with no theorem change.

Transfer current HTML

TRANS-04: Transfer, direct, causal, and unary papers · Transfer Section 6 and assurance boundary; cross-paper dependency graph

Classification: Application assurance and route separation.

Before: The review needed to distinguish the checked generic compiler from the source of its palindrome recognizer premise and from the direct receipt route.

Exact result: The generic strict-machine-to-PEG implication and its EPAL specialization conditional on a supplied recognizer are machine-checked. The unconditional EPAL paper imports the classical strict recognizer; the other three papers are not premises of this route.

A reconstructed controller with growing microtime cannot instantiate the compiler, but that does not refute the imported classical theorem. Receipt, sequence, causal-compiler, and unary findings do not propagate into this transfer composition.

Keep the classical source layer explicit and separate. Make no paper change from Run 09; continue R05 with the unary guard audit.

Transfer current HTML · Direct Draft 5 · Causal current HTML · Unary current HTML

The generic strict-machine transfer and its implication from a supplied EPAL recognizer are machine-checked. The unconditional palindrome application still imports the classical strict recognizer. Run 09 found no timing, orientation, or empty-word mismatch inside the checked chain, and it does not promote that classical premise to machine-checked status.

The finite audit covered 326,592 control-and-orientation runs, 5,184 empty-word cases, and 5,015,520 tape-offset comparisons. The universal result comes from the Lean theorems and the composition above. No paper or PDF was changed.

Proof and assurance boundary · Finite checker · Recorded output · LMR source

Run 10: unary guards and terminal geometry

The four unary moves use four different certificates. A detour preserves a physical endpoint. Absorption requires an old target that is literally self-looping, not merely behaviorally recursive. Garbage changes only replay-irrelevant coordinates. A temporal slide transports a carrier between equal-labelled adjacent rows and preserves the final figure, although earlier prefix figures may change.

Move	Certificate	Preservation
D	Same physical endpoint	Every prefix figure
A	Literal old self-loop and equal recursive residual	Every prefix figure
G	Outside replay-closed causal support	Final replay and figure
T	Equal labels on candidate carriers	Final figure

The time-zero base is unlabelled, so a temporal slide cannot cross it. A missing or base terminal may therefore use time 1 for its first retained carrier. A recursive terminal needs an omitted positive-time physical loop below that carrier, leaving time 1 unavailable. This gives exactly the two carrier rectangles stated in Proposition 3.1.

[m-1]\times[n-m] \quad\text{versus}\quad [m-1]\times[n-m-1].

The focused audit checked 124,828 histories and found 33,060 cases that were behaviorally recursive without satisfying the literal absorption guard. Every checked move preserved the terminal kind. The unary proof uses full unfolding equivalence, not the incorrect same-radius identity repaired in Run 07. No new mismatch was found in any of the four papers, and R05 is complete.

UNARY-01: Unary scaffold coherence · Definition 2.1 and Sections 5 through 7

Classification: Exact guard stratification.

Earlier: The four elementary moves were listed together, leaving their different certificates to be reconstructed from later proofs.

Current: D uses physical endpoint equality; A uses a literal old self-loop plus equal recursive behavior; G uses replay-closed causal irrelevance; T uses equal-labelled adjacent carriers and preserves final rather than prefix behavior.

The proof does not confuse physical identity with behavioral equivalence. Each place that needs physical information states a physical guard, while the scaffold itself need not observe pointer identity.

Close the move-soundness boundary with no theorem change. Preserve this four-way distinction in any later exposition.

Unary original manuscript · Unary current HTML

UNARY-02: Unary scaffold coherence · Proposition 3.1, corrected carrier rectangles

Classification: Base and recursive terminal boundary.

Earlier: The recursive rectangle has one less time coordinate than the missing/base rectangle, but the role of the unlabelled base had not been checked separately in this review.

Current: A temporal slide compares labels on two candidate carrier rows and therefore cannot cross the unlabelled time-zero base. A recursive terminal also needs an omitted positive-time physical loop carrier below the first retained carrier.

Time 1 is available in the missing/base case and unavailable in the recursive case. This gives [m-1] x [n-m] versus [m-1] x [n-m-1], with the zero-carrier recursive case a singleton.

Retain the three terminal cases and the corrected coordinates. No additional base exception is missing.

Unary original manuscript

UNARY-03: Unary and causal scaffold algebra · Unary behavioral figures; causal Theorem 3.6

Classification: Inherited observation assumption survives.

Earlier: Run 07 repaired the causal proof of all-depth behavioral equivalence but left the unary guard audit open.

Current: The unary arguments use equality of full unfoldings, equivalently bisimilarity, and separately use physical endpoints in D and A. They do not use a same-radius native-view identity.

The one-layer finite-view correction does not alter unary coherence. The exact causal theorem needed by the unary paper remains valid.

Carry no theorem correction into the unary paper from the observation issue.

Unary current HTML · Causal current HTML

UNARY-04: All four scaffold papers · R05 dependency closure

Classification: No new cross-paper mismatch.

Earlier: Transfer timing and unary guard assumptions remained the final open dependency checks in R05.

Current: Run 09 closes the independent transfer composition. Run 10 closes the unary guard and terminal boundary. Unary coherence does not use the direct sequence contract or the causal batch compiler.

No newly found issue propagates across the four theorem statements. Previously recorded future edition repairs remain limited to their documented locations.

Mark R05 complete. Do not open piecemeal manuscript edits; retain the ledger for one future coordinated versioned revision.

Transfer current HTML · Direct Draft 5 · Causal current HTML · Unary current HTML

Argument and dependency closure · Focused checker · Recorded output

Run 02: recovering the earlier editions

Pinning today's files does not recover what earlier readers saw. This archive goes back to the transfer paper's July 30 source release, the direct and causal papers' August 21 releases, and the unary paper's August 23 release. It preserves exact PDF bytes, manuscript sources, recorded change logs, and later HTML body revisions. The current papers have not been changed.

Paper	Distinct PDF files	HTML body snapshots
Real-time multitape transfer	7	3
Direct palindrome scaffolding	7	19
Causal scaffold algebra	5	8
Unary scaffold coherence	2	3

These are byte-distinct artifacts, not newly assigned version numbers. The July transfer revisions reused one filename; the September 9 afterwords also changed PDFs without changing their filenames. Draft 1 of the direct paper itself had a compact and an expanded form. Each recovered file therefore has a full content hash and its source commit, not just a draft label.

The historical logs record substantive changes before today: the direct paper's Draft 2 repaired receipt closure and the transition-receipt layout; causal Draft 2 made the palindrome application conditional, and Draft 3 corrected carrier coordinates. Later Site revisions changed initialization and sequence-interface qualifications. These are records of prior changes, not a fresh certification of those proofs.

Commit dates below are not deployment dates. We have not identified which file each reviewer downloaded. HTML fragments preserve manuscript content, not an exact historical browser response, and no missing historic PDF has been manufactured from newer HTML.

Real-time multitape transfer: recovered PDFs

persistent-stacks-scaffolding-automata.pdf · 2026-07-30 · gitlab · 2e4a01d3a568 · Publish real-time multitape transfer to PEG
persistent-stacks-scaffolding-automata.pdf · 2026-07-31 · gitlab · 4b03f9e1df8a · Strengthen Lean tape-level transfer boundary
persistent-stacks-scaffolding-automata.pdf · 2026-07-31 · gitlab · 02b7a031e4bd · Close FPRD-T90 theorem package
persistent-stacks-scaffolding-automata.pdf · 2026-08-05 · gitlab · 5be6a0404688 · Publish current persistent-stacks paper
persistent-stacks-scaffolding-automata.pdf · 2026-08-05 · gitlab · 5bba550560a3 · Print Lean source URL in paper
persistent-stacks-scaffolding-automata.pdf · 2026-08-05 · gitlab · 5500a9f90a54 · Publish synchronized persistent-stack formalization
persistent-stacks-scaffolding-automata.pdf · 2026-09-09 · site · c00aa2c8ae07 · Add publication afterwords on FPRD methodology and specific contributions

Direct palindrome scaffolding: recovered PDFs

direct-palindrome-scaffolding.pdf · 2026-08-21 · gitlab · 808a776b8881 · Publish direct palindrome scaffolding proof
direct-palindrome-scaffolding.pdf · 2026-08-21 · gitlab · 3ffd9be2e586 · Publish specialist direct palindrome paper revision
direct-palindrome-scaffolding-draft-2.pdf · 2026-08-22 · gitlab · 672ae2a9c5cb · Publish standalone Draft 2 PEG papers
direct-palindrome-scaffolding-draft-2.pdf · 2026-09-09 · site · 79367355e9b6 · Add publication afterwords on FPRD methodology and specific contributions
direct-palindrome-scaffolding-draft-3-corrected.pdf · 2026-09-10 · site · 30509bab30f7 · Integrate T126 virtual initialization correction
direct-palindrome-scaffolding-draft-4-corrected.pdf · 2026-09-10 · site · 1aca9d5b1274 · Qualify direct palindrome route after source audit
direct-palindrome-scaffolding-draft-5.pdf · 2026-09-21 · site · a21873cd7173 · Update Site source

Causal scaffold algebra: recovered PDFs

persistent-scaffold-causal-algebra.pdf · 2026-08-21 · gitlab · 3aa2b2aaf48d · Publish persistent scaffold causal algebra
persistent-scaffold-causal-algebra-draft-2.pdf · 2026-08-22 · gitlab · 489a263b52ad · Publish standalone Draft 2 PEG papers
persistent-scaffold-causal-algebra-draft-3.pdf · 2026-08-23 · gitlab · 2eb5d4a0a607 · Publish unary scaffold coherent cubical algebra
persistent-scaffold-causal-algebra-draft-3.pdf · 2026-09-09 · site · 7c494be3d10d · Add publication afterwords on FPRD methodology and specific contributions
persistent-scaffold-causal-algebra-draft-4-corrected.pdf · 2026-09-10 · site · f4a375de5aec · Correct direct palindrome status across publications

Unary scaffold coherence: recovered PDFs

unary-scaffold-coherent-cubical-algebra-draft-1.pdf · 2026-08-23 · gitlab · 892936dc863a · Publish unary scaffold coherent cubical algebra
unary-scaffold-coherent-cubical-algebra-draft-1.pdf · 2026-09-09 · site · a13eb0fb03cb · Add publication afterwords on FPRD methodology and specific contributions

Full archive manifest, source references, and change events · Run 02 findings and remaining work

The load-bearing initialization, receipt, and sequence-contract changes now have a statement ledger. Existing draft labels will be retained. The next aligned editions will end with a cumulative history that also accounts for earlier unnumbered and HTML-only changes.

Run 01: the native observation boundary

In Loff, Moreira, and Reis's Definition 11, a missing pointer and the unlabelled base have the same depth-zero view. At positive depth the base appears as a node with empty children, so the two become distinguishable.

N_0(\mathrm{base})=N_0(\mathrm{missing}), \qquad N_1(\mathrm{base})\ne N_1(\mathrm{missing}).

A two-node example therefore separates exact finite-depth observation from a port-word description that distinguishes base and missing at every endpoint. The causal paper uses the latter description. Run 07 now proves the exact one-layer comparison. Agreement at every depth is equivalent even though agreement at one specified depth is not.

For the recent T160/T161 shortcut constructions, the example also shows why radius one alone cannot always reconstruct the source view. The radius-two reconstruction passed 6,120 native input runs and checks on 1,130 small legal scaffolds. This is finite evidence for the proposed repair; it does not certify the four manuscripts as a whole.

The terminology also needs care: one working label in T161 allows many ports. The unary coherence paper fixes one port. A normalization that increases degree cannot transfer that paper's restricted theorem automatically.

Work packages

Each run takes one bounded obligation and records what was checked, what follows, and what remains. A work package may take several runs. An unresolved observation remains a question until its mathematical consequences have been established.

Package	Status	Completion condition
R01: Model and edition baseline	Complete for the stated scope	Pin the four current editions, map shared interfaces, and reproduce the native base-node example.
H01: Historical editions and cross-paper change ledger	Complete for the load-bearing initialization, receipt, and sequence-contract chain; exact artifacts remain archived	Recover the earliest editions and same-name replacements, preserve exact bytes and source history, then classify substantive, explanatory, and formatting changes across all four papers. Do not identify source dates as deployment dates or assign editions to reviewers without evidence.
R02: Finite observations and full behavior	Complete: exact one-layer comparison proved and dependencies traced	Prove the exact comparison between native depth-m views and port-word observations, then trace every radius-sensitive use in the four papers and T153-T161.
R03: Initialization and simultaneous records	Complete: exact compiler interface proved and cross-paper boundary traced	Compare direct Theorem 10.2 with causal Theorem 9.2: initial roots, virtual records, positive degree, and absence of pointer-identity tests.
R04: Sequence contract and application references	Complete for current statements and source history	Match the direct theorem's hypotheses to its source evidence and every companion citation, including causal Example 9.6.
R05: Transfer and coherence dependencies	Complete: transfer composition and unary guard boundary checked	Check strict timing and reversal in the transfer route, then the observational and guard assumptions inherited by unary coherence.
R06: Controlled edition revisions	Deferred pending one coordinated edition plan	For each justified change, build matching numbered PDF and HTML editions from one source, retain prior editions, and append a concise change history.

Edition alignment

Real-time multitape transfer: Expanded HTML; earlier PDF dated 5 August.
Direct palindrome scaffolding: Draft 5, 21 September; PDF and HTML share one source.
Causal scaffold algebra: Expanded HTML; earlier corrected Draft 4 PDF.
Unary scaffold coherence: Expanded HTML; earlier Draft 1 PDF.

Future revisions will use one maintained manuscript for matching PDF and HTML editions, with the same version and date. Earlier versions remain available. A short history at the end will identify the changed statements, reasons, and consequences. This review page records the investigation; the paper editions remain unchanged in Runs 01 through 10.

Run log

Run 01 · 2026-09-23

Current edition inventory and the native observation boundary; not a complete reproof of the four manuscripts.

The native base-node example is verified. The exact finite-depth identification in the causal paper needs a coordinated impact check. The direct paper has a matching-edition build; the other three retain older PDF pairings.

Next: Superseded priority: recover historical editions in H01 before resuming R02.

Run 02 · 2026-09-23

Recover manuscript artifacts from the pinned GitLab and Site histories, including earlier drafts, same-name PDF replacements, and HTML-only revisions.

The archive reaches the earliest repository releases of all four papers. Exact PDFs, sources, HTML fragments, and prior change logs are preserved with hashes. Current paper bodies and PDFs remain unchanged. Source history does not establish reviewer downloads or deployment dates.

Next: H01: build the statement-level cross-paper change ledger before making coordinated numbered editions.

Run 03 · 2026-09-23

Compare initialization and compiler-resource statements across the archived and current editions of all four papers.

Five ledger entries identify the direct virtual-table change, the positive-degree qualification, the causal compiler's unstated initial contract, and the separate transfer/unary base cases. A finite initialization audit passes 143,325 two-step checks. Paper editions remain unchanged.

Next: Completed by Run 04: compare direct Draft 1-to-2 receipt closure and layout changes, then trace later sequence-contract statements into causal Example 9.6.

Run 04 · 2026-09-23

Compare the direct paper's Draft 1 receipt argument and record layout with Drafts 2 and 5, then trace those changes across the causal, transfer, and unary papers.

Draft 2 made two substantive repairs: a separate last-cell mirror-prefix proof and occurrence-indexed transition receipts that remove an unbounded access path. The causal application depends on the repaired companion construction; its generic compiler does not. No direct dependency was found in the transfer or unary proofs. Paper editions remain unchanged.

Next: Completed by Run 05: compare the later sequence-source, resource-certificate, and whole-client-normalization chain referenced by causal Example 9.6.

Run 05 · 2026-09-23

Compare the direct paper's sequence contract, whole-client theorem, and implementation evidence with the causal paper's companion claims, then trace dependencies through the transfer and unary papers.

The direct theorem is conditional on its Section 11.1 sequence contract, and Appendix D labels the pinned OCaml work as informal source evidence rather than a complete source-to-scaffold certificate. The causal palindrome example is scoped to the companion's abstract model but describes the implementation evidence more strongly and still cites Draft 4 while linking to Draft 5. Its generic compiler is unaffected; transfer and unary remain separate. Paper editions remain unchanged.

Next: H01: finish the historical sequence-contract change ledger, then resume R02's native-observation comparison. Reserve any wording repair for matching numbered editions.

Run 06 · 2026-09-23

Reconstruct the sequence-claim chronology from the early direct theorem through withdrawal, conditional restoration, radius rollback, and Draft 5, while matching the causal companion snapshots.

The direct theorem was genuinely withdrawn during the source audit, then restored in an abstract source-record model after whole-client normalization. A later mutation attack withdrew the numerical radius, and Draft 5 now separates the conditional theorem from informal implementation evidence. The causal wording froze at the restoration stage and did not absorb the later assurance rollback. Paper editions remain unchanged.

Next: R02: compare native finite views with port-word observations and trace every radius-sensitive use through the causal and unary papers and T153-T161.

Run 07 · 2026-09-23

Prove the exact relation between native LMR depth-m neighbourhoods and causal port-word observations through length m, then trace every affected use through the causal and unary papers and FPRD-T153 through FPRD-T161.

The native view is a recursive truncation of the causal table and loses only the base-versus-missing distinction at its outer frontier. One additional native layer recovers it. Causal Theorem 3.6's all-depth statement survives with a local proof repair; unary coherence and T153-T159 survive. T160 needs radius two rather than radius one for reconstruction, which its stated distance-two construction already provides. T161 already uses radius two. Paper editions remain unchanged.

Next: R03: compare the direct and causal batch compilers on initialization, positive degree, and pointer-identity observability.

Run 08 · 2026-09-23

Complete the direct-versus-causal simultaneous-record compiler comparison, including virtual initialization, positive degree, pointer-identity observability, and alias preservation.

The exact compiler theorem uses fixed finite pointer-closed virtual initial data, degree max{1,s+Aq}, distance r+1, and transition plans that factor through bounded labelled rooted unfoldings. Direct Theorem 10.2 already has this contract. Causal Theorem 9.2 has the correct one-step construction but needs the initialization and positive-degree clauses. Native views cannot reveal physical alias identity, although a fixed compiled plan preserves existing aliases. Transfer and unary results are unaffected. Paper editions remain unchanged.

Next: R05: audit strict timing, reversal, and empty-input handling in the transfer route, then close the remaining unary guard dependencies.

Run 09 · 2026-09-23

Audit strict timing, reversal orientation, empty-input acceptance, and the classical-recognizer assurance boundary in the independent transfer route.

The machine-to-scaffold compiler is exactly letter-synchronous and preserves the source language without reversal. The formal scaffold-to-PEG construction introduces exactly one reversal, and every layer preserves the empty word without an extra step. The compiler does not strictify a slower source machine. The generic transfer is machine-checked; the strict real-time palindrome recognizer remains the explicitly imported classical premise. No mismatch was found in the checked composition, and no paper edition changed.

Next: R05: audit the unary paper's move guards, base termination, and inherited behavioral assumptions.

Run 10 · 2026-09-23

Audit the unary paper's four move guards, the unlabelled-base boundary, the missing/base/recursive terminal split, and the exact behavioral assumption inherited from the causal paper.

The guards cleanly separate physical endpoint equality, literal self-loop absorption, causal irrelevance, and equal-label temporal transport. Slides cannot cross the unlabelled base, which accounts for the extra unavailable row in the recursive carrier rectangle. Every move preserves terminal kind. The theorem uses surviving all-depth behavioral equivalence, not the false same-radius identity. No paper mismatch was found and no edition changed.

Next: R05 is complete. Retain the ledger for a future coordinated edition; resume foundational FPRD work without opening piecemeal manuscript revisions.