Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Five Mode Recurrent Pair Rigidity

Abstract

Every recurrent class of the actual synchronized source-observer chain has exact emissions and complete generated future laws.

The passive source has modes State=Fin 5, visible alphabet Visible=Fin 4, B=2, and the fixed transition matrix and uniform initialized law of FiniteStartFiveModeSource. Admissibility means p,q,r>0 and p+q+r<1. Both p=q and r=p+q are included. The visible rows in Lean order (0,1,B,3) are (c,p,r,q), (q,a,p,0), (0,q,a,p), (p,0,q,a), (r,0,b,0), with a=1-p-q, b=1-r and c=1-p-q-r.

A GeneratedObserver on the whole finite carrier Z has an initial configuration, arbitrary total update, and a normalized nonnegative emission row at every configuration. Its retained run folds that same update over actual observations; its generatedLaw multiplies the emissions along the same update on every hypothetical word. All generated-only configurations remain in Z. Forecast-zero actual-legal inputs remain defined. A source mode in a pair is a proof coordinate and supplies no observer input.

History means a finite chronological visible list. historyMass is its actual initialized cylinder mass. The empty query starts at Y0. A nonempty history of length n predicts Yn onward by the conditional acquired posterior. Words(H) is the entire function carrier Fin H to Visible, and finite TV is half the sum of absolute differences over that entire carrier. Thus impossible and zero-weight words are included. The theorem assumes the original guarantee only for positive natural H and arbitrary real epsilon<1. It derives epsilon>=0 from the guarantee and extends it to H=0 using normalization; no error-sign premise is added.

Synchronized(p,q,r,O,t) is witnessed by a positive actual history containing a symbol other than B, with sourceRun pure at mode(t) and the retained run equal to configuration(t). The acquired positive-history invariant identifies its actual posterior with the pure source vector. Every singleton-containing actual history has such a pure source tag. The symbol update nextPure is the singleton reset on 0,1,3; at B it maps 0 and 4 to 4 and the other modes to 2.

S=ActualPair(p,q,r,O) is this subtype of State times Z, hence finite. The positive actual history [0] makes it nonempty. For every source-positive symbol the acquired cylinder quotient gives the literal positive extension mass, and the source and observer folds give nextPair. Thus every such successor is again in S. actualStep is this lifted successor on a positive source weight; on a zero source weight it chooses the present pair as an auxiliary endpoint. This choice changes no transition mass and does not change the total observer update.

K=pairMatrix(p,q,r,O) sums v(mode(t),y) over symbols with actualStep(O,t,y)=u. Here v(i,y)=pureRow(p,q,r,i,y). It is the stochastic matrix on the actual subtype S. ClosedClass(K) means an actual terminal communicating class of the positive support, including reachability by the empty path. ClassStates(C) is its finite state set. The theorem quantifies every such class, proves it nonempty and irreducible, and supplies closure under every positive support path.

For a pair t, let aH(t) be the Bhattacharyya affinity of its pure source H-word law and the observer generated H-word law, and d(t,y)=sqrt(v(mode(t),y)*row(O,configuration(t),y)). The independently defined word laws give a(H+1)(t)=sum_y d(t,y)*aH(nextPair(O,t,y)). Nonnegativity and normalized row affinity make aH decrease from one, so its infimum l(t) is a limit and satisfies the same finite-sum equation. The Hellinger-to-TV lower bracket and the actual-history guarantee imply l(t)>=1-epsilon>0 on S. Source-zero symbols have d(t,y)=0, even if the observer gives them positive weight.

Fix any actual terminal class and maximize l there, with maximum M>0. Closure gives l(nextPair)<=M on every source-positive symbol. Therefore M=sum_y dl(nextPair)<=Msum_y d<=M. Equality forces sum_y d=1; normalized Hellinger separation then forces the observer row to equal the complete source row, including its zeros. The nonnegative weighted deficits M-l(nextPair) sum to zero. At an exact row every source-positive coefficient is positive, so each such successor also has limiting affinity M. Actual communication propagates this equality to every pair of the class, forcing every row exact.

With exact rows, induction on the complete future word length gives generatedLaw(O,configuration(t))=pureLaw(p,q,r,mode(t)). A source-zero first symbol makes both word weights zero; a positive first symbol stays inside the class, where the induction applies. This proves equality at every finite horizon without conditioning on a forecast-positive event or discarding generated words.

The positive square edges connect 0,1,2,3 and the positive leaf edges connect 0 and 4. More explicitly, any mode reaches 0 using singleton reads, with mode 2 first reading 1; from 0 the words [], [1], [1,B], [3], [B] reach modes 0,1,2,3,4. These paths lift inside every actual closed class. Choosing one pair above each mode gives actually reachable configurations. Existing full-domain pure-profile separation makes these five configurations distinct. The result does not assert a minimum observer cardinality, exactness of transient configurations, or uniqueness of the recurrent presentation.

Definition 1.1 (Synchronized).

Formalization. D5/S3/ObserverMemory/Prediction/FiveModeRecurrentPairRigidity.Synchronized (✓ std3).

Source. Repository-derived.

Commentary.

The definition uses the full fixed source and actual acquired histories.

Definition 1.2 (ActualPair).

Formalization. D5/S3/ObserverMemory/Prediction/FiveModeRecurrentPairRigidity.ActualPair (✓ std3).

Source. Repository-derived.

Commentary.

The definition uses the full fixed source and actual acquired histories.

Definition 1.3 (nextPair).

Formalization. D5/S3/ObserverMemory/Prediction/FiveModeRecurrentPairRigidity.nextPair (✓ std3).

Source. Repository-derived.

Commentary.

The definition uses the full fixed source and actual acquired histories.

Definition 1.4 (actualStep).

Formalization. D5/S3/ObserverMemory/Prediction/FiveModeRecurrentPairRigidity.actualStep (✓ std3).

Source. Repository-derived.

Commentary.

The lift carries the derived actual-history membership proof; its proof argument is suppressed.

Definition 1.5 (pairMatrix).

Formalization. D5/S3/ObserverMemory/Prediction/FiveModeRecurrentPairRigidity.pairMatrix (✓ std3).

Source. Repository-derived.

Commentary.

The definition uses the full fixed source and actual acquired histories.

Lemma 1.6 (guarantee accurate).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModeRecurrentPairRigidity.guarantee_accurate (✓ std3). ∎

Source. Repository-derived.

Commentary.

The guarantee at positive future horizons also gives the zero-horizon bound by normalization. This applies to arbitrary real epsilon and includes the positive empty actual history.

Theorem 1.7 (recurrent pair rigidity).

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Prediction/FiveModeRecurrentPairRigidity.recurrent_pair_rigidity (✓ std3). ∎

Source. Repository-derived.

Commentary.

For all admissible sources, all finite unrestricted normalized self-generated observers, and every real epsilon<1 satisfying the complete actual-history guarantee, all displayed conclusions hold simultaneously.

References