Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Chronological rectangle occurrence moments

Abstract

Chronological rectangle occurrence moments

Definition 1.1 (The complete original marked past at a cut).

Formalization. D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/Rectangles/OriginalRectangleMoments.markedField (✓ std3).

Source. Repository-derived.

Commentary.

For any measurable hidden type H and integer t, markedField(t) is the sigma-field generated by the pair consisting of H(t) and the entire sequence of hidden states and emitted bits strictly before t. It contains every hidden coordinate through t and every output coordinate below t. It contains no output at t or later.

Definition 1.2 (One success depends only on the block’s emitted bits).

Formalization. D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/Rectangles/OriginalRectangleMoments.blockSuccess (✓ std3).

Source. Repository-derived.

Commentary.

blockSuccess(w,b,d) is the original event that w is an infix of the b consecutive emitted bits beginning at integer d. It is the preimage of OriginalRectangleOccurrence.success(w,b) under the original future(d) map. Hidden starting states do not enter this event.

Definition 1.3 (The original chronological block count).

Formalization. D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/Rectangles/OriginalRectangleMoments.chronologicalCount (✓ std3).

Source. Repository-derived.

Commentary.

chronologicalCount(w,b,d,q) is the sum of the success indicators for the q disjoint blocks beginning at d, d+b, through d+(q-1)b, in that time order. Each block pays once, regardless of how many occurrences lie inside it. An empty block sequence has count zero.

Theorem 1.4 (The same-law conditional success probability).

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/Rectangles/OriginalRectangleMoments.marked_success_condExp (✓ std3). ∎

Source. Repository-derived.

Commentary.

Let theta be any original stationary binary edge presentation on finite measurable H, and J any probability measure with theta’s original marked cylinders. Fix a Boolean word w, a support rectangle for product(theta,w), a row r in its row support, and the given family a of positive labelled original routes from every h to r, each of length at most card(H). Set b=length(w)+card(H), and keep exactly the selectedEpsilon(theta,w,r,a) of that family. For every integer t, the conditional expectation under J of the blockSuccess(w,b,t) indicator given markedField(t) is at least this epsilon almost everywhere. The complete marked-past occurrence inequality is summed over the finite hidden fibers for an arbitrary measurable event of markedField(t). Its real integral characterization then gives the conditional-expectation lower bound. Null hidden fibers remain in the sum and require no division.

Theorem 1.5 (Successes pay the squared contraction in chronological time).

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/Rectangles/OriginalRectangleMoments.chronological_success_moment (✓ std3). ∎

Source. Repository-derived.

Commentary.

Under the same presentation, same original-cylinder probability J, same word, rectangle, support row and given route family as above, take any real rho with 0<=rho<=1, any integer start d and natural block count q. Let b=length(w)+card(H), epsilon=selectedEpsilon(theta,w,r,a), eta=1-epsilon*(1-rho^2), and K=chronologicalCount(w,b,d,q). The J integral of rho^(2*K) is at most eta^q. The single-block factor is rho^2 on success and one otherwise. Its conditional expectation at the block start is at most eta by the preceding conditional probability bound. All earlier factors are measurable in the complete marked past at the next block start; pulling them out and taking total expectation gives one factor eta at each step. No independence, future-conditioned success estimate, positivity of every matrix entry, aperiodicity or unifilarity is imposed. The case q=0 is the integral of one, including rho=0; eta may also be zero.

The blockSuccess defining equality displays its implicit hidden type H explicitly in blockSuccess(H,w,b,d) and future(H,d). In the formulas, generatedField(f) means the comap of the canonical product measurable space along f; condExp(J,f,m,z) is the conditional expectation of f given m evaluated at z. sumRange(q,f) is the natural finite sum over i in Finset.range(q); indicator(S,f), constFunction(T,c), preimage, integral and intCast have their corresponding Lean meanings. AE(J,(z maps to p)) denotes the almost-everywhere quantifier under J.

For a native source component C, instantiate theta with nativeComponent and use the very original-cylinder law on C identified by component_restriction. Choose the routes furnished by OriginalRectangleRoutes, without changing the selected family or its epsilon. Put rho=1-u/v from the original support rectangle. For q=floor(j/b), the left count uses d=-qb and the right count uses d=1. These are respectively the source blocks [-qb+(i-1)b,-qb+ib-1] and [1+(i-1)b,i*b], for i from one through q. Both applications average in chronological original time under this one class-restricted measure, even though the finite right-posterior comparison propagates in reverse. At j=0 both block counts are empty. The identity with the finite-list count in finite_record_smoothing_by_original_success_count and the identification of finite-record posteriors with conditional expectations supply the separate connections from posterior differences to these moments.

References