StationaryHistoryContinuation

Abstract

Indexed history separation, first-read fibers and positive literal continuation gaps.

Theorem 1.1 (Original first-read fibers).

$$\forall P:\mathbb{N},\forall Q:Typ{e}_u,\forall C:\mathrm{Controller}(P,Q),\forall hP:1<P,\forall ell:\mathbb{N},\forall h:\mathbb{N},\forall I:\mathrm{Initialized}(C,hP,ell,h),[\mathrm{NeZero}(3\times P)]\forall c:\mathrm{Fin}(3),\forall x:\mathrm{ZMod}(3\times P),x\in \mathrm{support}(C,hP,I,\mathrm{root}(C,hP,I,c))⟺\mathrm{digit}(hP,x+ell)=c$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryContinuation.root_support (✓ std3). ∎

Source. Repository-derived.

Commentary.

The root support is exactly the original digit block after the common literal translation ell. No source-dependent preparation is introduced.

Theorem 1.2 (Phase separation at one control).

$$\forall P:\mathbb{N},\forall Q:Typ{e}_u,\forall C:\mathrm{Controller}(P,Q),\forall hP:1<P,\forall ell:\mathbb{N},\forall h:\mathbb{N},\forall I:\mathrm{Initialized}(C,hP,ell,h),[\mathrm{NeZero}(3\times P)]\forall n:\mathrm{History}(C,hP,I),\forall m:\mathrm{History}(C,hP,I),n\ne m\wedge \mathrm{readControl}(C,hP,I,n)=\mathrm{readControl}(C,hP,I,m)⟹\mathrm{Disjoint}(\mathrm{phaseSupport}(C,hP,I,n),\mathrm{phaseSupport}(C,hP,I,m))$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryContinuation.same_control_phase_disjoint (✓ std3). ∎

Source. Repository-derived.

Commentary.

A common physical phase and read control would give equal initialized configurations. Finite correctness then forces the same original label and time, and hence the same indexed read and full history. This also applies to histories at different levels and to terminating control cycles.

Theorem 1.3 (Literal read gaps are physical shift increases).

$$\forall P:\mathbb{N},\forall Q:Typ{e}_u,\forall C:\mathrm{Controller}(P,Q),\forall hP:1<P,\forall ell:\mathbb{N},\forall h:\mathbb{N},\forall I:\mathrm{Initialized}(C,hP,ell,h),[\mathrm{NeZero}(3\times P)]\forall x:\mathrm{ZMod}(3\times P),\forall i:\mathbb{N},i+1<\mathrm{reads}(C,hP,I,x)⟹0<\mathrm{readTime}(C,hP,I,x,i+1)-\mathrm{readTime}(C,hP,I,x,i)+1\wedge \mathrm{historyShift}(C,hP,I,\mathrm{event}(C,hP,I,(x,i+1)))=\mathrm{historyShift}(C,hP,I,\mathrm{event}(C,hP,I,(x,i)))+\mathrm{readTime}(C,hP,I,x,i+1)-\mathrm{readTime}(C,hP,I,x,i)+1$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryContinuation.literal_shift_gap (✓ std3). ∎

Source. Repository-derived.

Commentary.

The action immediately after a nonfinal read is a wait. Consecutive read times therefore have a positive intervening literal gap. Time equals shift plus read level, so the shift increases by that entire gap.

Theorem 1.4 (Singleton continuation stays unary).

$$\forall P:\mathbb{N},\forall Q:Typ{e}_u,\forall C:\mathrm{Controller}(P,Q),\forall hP:1<P,\forall ell:\mathbb{N},\forall h:\mathbb{N},\forall I:\mathrm{Initialized}(C,hP,ell,h),[\mathrm{NeZero}(3\times P)]\forall n:\mathrm{History}(C,hP,I),\mathrm{card}(\mathrm{support}(C,hP,I,n))=1\wedge \neg \mathrm{IsLeaf}(C,hP,I,n)⟹\mathrm{card}(\mathrm{children}(C,hP,I,n))=1$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Algorithms/StationaryHistoryContinuation.singleton_continuation (✓ std3). ∎

Source. Repository-derived.

Commentary.

Every child’s support is nonempty and lies in its parent’s support. When that support is one label, child level and input-index uniqueness force one child. The continuation is kept rather than erased.

References

• Truth anchor: D5/S3/ObserverMemory/Algorithms/StationaryHistoryContinuation.literal_shift_gap
• Truth anchor: D5/S3/ObserverMemory/Algorithms/StationaryHistoryContinuation.root_support
• Truth anchor: D5/S3/ObserverMemory/Algorithms/StationaryHistoryContinuation.same_control_phase_disjoint
• Truth anchor: D5/S3/ObserverMemory/Algorithms/StationaryHistoryContinuation.singleton_continuation
• Dependency: D5/S3/ObserverMemory/Algorithms/StationaryHistoryPrefix