Run 07: native views and port-word observations

Date: 23 September 2026

Scope

This run proves the exact comparison between Loff-Moreira-Reis native finite-depth neighbourhoods and the causal paper’s port-word endpoint observations. It then traces the result through the causal and unary papers and FPRD-T153 through FPRD-T161.

The four circulated paper bodies and PDFs were not changed.

Exact comparison

Let (P_m(S,v)) record, for every port word of length at most (m), whether following that word from (v) reaches:

• a working-labelled node and its label;
• the distinguished unlabelled base; or
• a missing endpoint.

This is the finite restriction of the causal paper’s unfolding. Let (N_m(S,v)) be the native LMR radius-(m) neighbourhood.

There is a canonical recursive truncation map

$$\tau_m(P_m(S,v))=N_m(S,v).$$

At positive remaining depth, the truncation retains whether the current endpoint is a node or is missing, together with the node label and recursively truncated children. At remaining depth zero, it retains only the endpoint label. The base has the empty label, and a missing endpoint also has the empty radius-zero view. Therefore the only nonredundant information lost is:

At the outer frontier, a path ending exactly at the base and a path becoming missing have the same native radius-(m) leaf.

It follows that

$$P_m(S,v)=P_m(T,u)\Longrightarrow N_m(S,v)=N_m(T,u),$$

and

$$N_{m+1}(S,v)=N_{m+1}(T,u)\Longrightarrow P_m(S,v)=P_m(T,u).$$

Both implications can be strict. A chain reaching the base exactly at depth (m) and a matching chain becoming missing there have the same (N_m) but different (P_m). Conversely, (N_{m+1}) can see the children of an ordinary depth-(m) endpoint, while (P_m) records only that endpoint’s label.

Full behavior is unchanged

The one-layer finite discrepancy disappears when every depth is considered:

$$\forall m\;N_m(S,v)=N_m(T,u) \quad\Longleftrightarrow\quad \mathcal U_{S,v}=\mathcal U_{T,u}.$$

The forward direction is immediate unless the first port-word difference is base versus missing. If that word has length (r), native depth (r+1) distinguishes the base node from the missing endpoint. The reverse direction is structural induction on the native view.

Thus the main statement of causal Theorem 3.6 remains valid: equal full unfoldings, equality at every native finite depth, and labelled bisimilarity coincide. Its continuation-stability argument also remains valid because it is formulated with full unfoldings.

The proof contains two same-radius overstatements that need a future edition repair:

1. LMR’s transition does not literally see (P_k); it sees (N_k=_k(P_k)).
2. (N_m) is not literally the restriction of the unfolding through length (m). It is its recursive frontier truncation.

The distance-two separating continuation remains sound. When its cursor points to the first differing endpoint, the extra native layer distinguishes base from missing.

Dependency trace

Causal scaffold algebra

• Definition of the full unfolding is sound.
• Theorem 3.6’s all-depth equivalence, bisimulation equivalence, continuation stability, and distance-two separation survive.
• The same-radius explanatory sentences require the truncation and one-layer shift above.
• The minimal-figure, chain, folding, support, and normalization results use full behavior or physical endpoints, not the false same-radius identity.

Unary scaffold coherence

The unary paper works with full behavioral figures, physical endpoint guards, and distinct missing, base, and recursive terminal cases. It does not use the claim that a native radius-one view equals the causal endpoint table through length one. No theorem change follows from this audit.

FPRD-T153 through FPRD-T159

• T153 is already written in native recursive-view semantics. Its count starts with (V_0=|Gamma|+1), explicitly identifying the radius-zero base and missing observations. Its pullback radius and capacity theorem survive.
• T154 and T158 use T153’s native theorem and survive.
• T155 and T156 are abstract support and residual results and do not use the scaffold finite-view identification.
• T157 defines the native scaffold transport spectrum and does not use it.
• T159’s distance-one DFA summary is genuinely native. A new radius-one view needs only the old radius-one view: any base-versus-missing target appears at the new frontier and is supposed to be identified there. The regular-collapse theorem survives.

FPRD-T160 and FPRD-T161

T160’s distance-two normal-form theorem survives, but one proof sentence is too strong. A shortcut-closed radius-one view does not always reconstruct the source radius-(k) view because a shortcut ending at the base and a missing shortcut coincide at radius zero. The compiled machine already has distance two. Its radius-two view distinguishes those endpoints and reconstructs the source view, without changing the stated degree or distance bound. The descriptor-installation proof was already two-hop.

T161 already uses the repaired boundary explicitly: its radius-two view follows one shortcut hop and one marker hop, and it reserves the all-zero marker pattern for the nonmissing base. Its theorem survives unchanged.

Executable evidence

check_native_observation_shift.py checks the recursive truncation and the two finite-depth implications on:

• 6,295 degree-one chronological scaffolds through five nodes;
• 595 degree-two scaffolds through three nodes;
• 27,560 truncation instances;
• joint stable behavioral partitions on 32,644 node states; and
• explicit base-versus-missing frontier witnesses at depths one through four.

It also checks the exact current statement markers in the causal paper and T153, T159, T160, and T161. The finite audit corroborates the boundary cases; the recursive arguments above prove the general statements.

Next

R03 resumes the compiler-interface review: compare direct Theorem 10.2 and causal Theorem 9.2 on initialization, positive degree, and pointer-identity observability. Any eventual wording change remains reserved for matching numbered PDF and HTML editions with a concise cumulative history.