Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Accepted words and legal future effects

Abstract

Actual accepted partial runs generate effect propagation, a simultaneous finite horizon, and arbitrary initial-state delay.

Let K be a division ring and E a left K-module with an additive commutative group. Let Alphabet and Q be arbitrary types, with decidable equality on Q. A BaseAutomaton M has a distinguished start state and partial transition M.step(q,a). Its existing runFrom operation follows the list from left to right, returning none as soon as a transition is absent. Let F be a finite set of accepting states, A assign a total K-linear endomorphism to each letter, and U be the common terminal submodule. No epsilon transitions or intermediate reads are added. For chronological w = a1…ak the effect is the list product A(a1)…A(ak): the head acts after the tail and the empty word acts as identity. Real finite-dimensional spaces are obtained by K = R.

Definition 1.1 (Actual terminal acceptance).

Formalization. D5/S3/Observer/LinearMemory/AcceptedWordEffectPropagation.Accepts (✓ std3).

Source. Repository-derived.

Commentary.

Acceptance requires a successful whole run ending in F. A missing transition supplies no execution event.

Definition 1.2 (Bounded accepted effect span).

Formalization. D5/S3/Observer/LinearMemory/AcceptedWordEffectPropagation.acceptedSpan (✓ std3).

Source. Repository-derived.

Commentary.

The span is defined directly from runFrom acceptance and word length, independently of the recurrence.

Definition 1.3 (All finite accepted effects).

Formalization. D5/S3/Observer/LinearMemory/AcceptedWordEffectPropagation.fullFuture (✓ std3).

Source. Repository-derived.

Commentary.

There is no length bound. Only accepted terminal reads contribute.

Definition 1.4 (One propagation step).

Formalization. D5/S3/Observer/LinearMemory/AcceptedWordEffectPropagation.effectStep (✓ std3).

Source. Repository-derived.

Commentary.

The supremum is the sum of the image subspaces indexed by all and only defined transitions. Repeated targets and loops are allowed. An empty index family contributes the zero submodule.

Definition 1.5 (The all-state recurrence).

Formalization. D5/S3/Observer/LinearMemory/AcceptedWordEffectPropagation.propagation (✓ std3).

Source. Repository-derived.

Commentary.

The initialization is U exactly at accepting states and zero elsewhere. The next tuple uses the same fixed transition operator, so a simultaneous plateau is a fixed point.

Theorem 1.6 (Exact accepted-word characterization).

Proof. Machine-checked in Lean as D5/S3/Observer/LinearMemory/AcceptedWordEffectPropagation.propagation_eq_accepted (✓ std3). ∎

Source. Repository-derived.

Commentary.

At horizon zero the only possible word is empty. A nonempty accepted word uniquely separates into its head a, the actual next state qprime, and an accepted tail from qprime. The identity A(aw) = A(a)A(w), submodule map of a span, and induction identify the independent word span with the recurrence at every state and horizon. No extra permission or read is inferred.

Theorem 1.7 (The simultaneous rank-offset horizon).

Proof. Machine-checked in Lean as D5/S3/Observer/LinearMemory/AcceptedWordEffectPropagation.simultaneous_stabilization (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume Q is finite and E is finite dimensional. Set d = finrank(K,E), r = finrank(K,U), and B = |Q|d - |F|r, using natural subtraction. The rank sum over the actual coordinate subspaces starts at |F|r and is bounded by |Q|d. The existing FiniteSequentialWordCertificate.bounded_monotone_has_equal_step supplies a consecutive equal-rank pair by B. Since every coordinate increases, equality of the sums forces equal rank at every coordinate; inclusion then forces simultaneous subspace equality. Iteration of the same tuple operator preserves that equality. Every accepted word belongs to its own finite-horizon span, hence to the stable tuple, proving fullFuture(q) = propagation(B,q) for every q, including the distinguished start. This uses the sum of coordinate ranks directly; it does not identify that sum with the rank of a correlated lifted space. Empty F or Alphabet, zero U or E, arbitrary loops and partial undefined transitions need no additional hypothesis.

Definition 1.8 (The actual finite successor chain).

Formalization. D5/S3/Observer/LinearMemory/AcceptedWordEffectPropagation.chain (✓ std3).

Source. Repository-derived.

Commentary.

The alphabet is Unit, the states are Fin(L+1), the start has value zero, and only the final state has no successor. The displayed natural successor is regarded as its bounded Fin element.

Definition 1.9 (Sole terminal acceptance).

Formalization. D5/S3/Observer/LinearMemory/AcceptedWordEffectPropagation.chainFinal (✓ std3).

Source. Repository-derived.

Commentary.

The singleton contains the Fin(L+1) state of value L. It also describes the length-zero chain.

Theorem 1.10 (Arbitrary initial-state plateaus).

Proof. Machine-checked in Lean as D5/S3/Observer/LinearMemory/AcceptedWordEffectPropagation.arbitrary_chain_delay (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural L and every submodule U over any of the stated scalar and carrier choices, put every letter effect equal to identity and accept only the chain terminal. At state q the propagated space is U exactly when L <= q.val+n and is zero otherwise. Induction on n uses the actual successor edge and the absence of an edge from the terminal. Consequently the initial space is zero for every n<L and is U at L. Taking K=R, E=R and U=R gives the scalar delay family, with L=0 and L=1 included. If L>=2 and U is nonzero, the initial spaces at zero and one agree, but the length-L space differs. Thus equality at the initial state alone cannot replace simultaneous equality. Arbitrarily many initial plateaus follow by increasing L. These are algebraic horizon statements; they assert no numerical, physical-resource or cost improvement.

References