Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original rectangle posteriors and squared erasure defects

Abstract

Original rectangle posteriors and squared erasure defects

Theorem 1.1 (The support rectangle gives a contraction parameter below one).

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

Source. Repository-derived.

Commentary.

For every real matrix B on a finite index type and every positive support rectangle R, OriginalRectangleSmoothing.extrema supplies 0 < u <= v for its least and greatest rectangle entries. Hence rho=1-u/v lies in [0,1), including rho=0. The same statement supplies the range in the posterior proof and the native component theorem.

Theorem 1.2 (The finite ratios and chronological counts meet on the same original law).

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

Source. Repository-derived.

Commentary.

Let H be any finite measurable hidden type with measurable singletons, theta an original stationary binary edge presentation, and J any probability measure on the original marked integer-time path space with HasOriginalCylinders(J,theta). Fix a nonempty Boolean word w, a support rectangle R for product(theta,w), a state r in its row support, and a family a(h) of positive labelled original routes from every hidden h to r, each of length at most card(H). Let j be any natural number. No hypothesis asserts a posterior bound, independence, future-conditioned occurrence, unifilarity, aperiodicity, or positivity outside the support rectangle.

Define P=J.map(Prod.snd), b=length(w)+card(H), u=rectangleMinimum(product(theta,w),R), v=rectangleMaximum(product(theta,w),R), rho=1-u/v, epsilon=selectedEpsilon(theta,w,r,a), eta=1-epsilon*(1-rho^2), and q=j/b. Define q0, pL, and pR to be the total bounded OriginalErasureComparison.bitPredictor versions for the center bit under P, evaluated respectively on exterior=(before,after), leftObservation(j)=(leftWord(j),after), and rightObservation(j)=(before,rightWord(j)). bitPredictor_condExp identifies these versions almost everywhere with the corresponding P conditional expectations of erasedBit. Both before and after are the entire infinite half-lines. The theorem first asserts that, for J-almost every original marked path z, abs(q0(z.2)-pL(z.2)) is at most rho raised to chronologicalCount(w,b,-q*b,q,z), and abs(q0(z.2)-pR(z.2)) is at most rho raised to chronologicalCount(w,b,1,q,z). It then asserts that the P integral of (q0-pL)^2 and the P integral of (q0-pR)^2 are each at most eta^q. All three conclusions retain the same J and its exact visible pushforward P.

In the displayed formulas, integral(P,f) is the real integral of f under P; map, snd and intCast are the measure pushforward, second projection and canonical integer cast. natDiv is natural division, and AE(J,(z maps to p)) means p holds J-almost everywhere. All predictors use the same P and the center-bit map x maps to x(0).

The finite observation is the pair of chronological original words X[-k,-1] and X[1,n]. Its fiber at (a,c) is exactly OriginalRectangleSmoothing.record(List.ofFn(a),List.ofFn(c)). The alphabet is finite, so the union of zero-mass observation fibers is null, including when either word is empty. On every remaining fiber, Mathlib condDistrib_apply_of_ne_zero identifies the conditional distribution with the ratio of the center-true record mass to the full record mass. OriginalErasureComparison.bitPredictor_condExp identifies this ratio with the erasedBit conditional expectation given OriginalRectangleHalfLines.recordField(k,n). There is no division on a null record or hidden fiber.

For k>=j, the chronological left word splits as its earlier prefix followed by the retained j-bit suffix. For n>=j, the chronological right word splits as the retained j-bit prefix followed by the extra future. Those two decompositions are passed directly to finite_record_smoothing_by_original_success_count, using the positive long and short observed records. No reverse or extra-past kernel, transfer contraction, or likelihood matrix bound is reconstructed.

The recursive finite-list success count is identified by induction with the sum of the same visible block-success indicators in chronological order. In a sampled word of length n, each take(b) is the original b-bit block at the current integer start and each drop(b) advances that start by b. The trimmed left word has length (j/b)b and begins at -j+(j mod b)=-(j/b)b. The right word begins at 1; its final incomplete block is unused by the count. Thus for i from one through q the left blocks are [-qb+(i-1)b,-qb+ib-1] and the right blocks are [1+(i-1)b,ib]. Every success is a complete w-infix in that block’s emitted bits, counted once. None includes X0.

finite_record_bounds_to_half_lines consumes the two finite conditional-expectation inequalities. It completes the past and then the future for left erasure, and the future and then the past for right erasure, without changing either count. Pullback by Prod.snd and the bitPredictor_condExp identities give the two bounds for the actual total bitPredictor versions under J. Squaring, changing variables between P and J, and applying chronological_success_moment at starts -qb and 1 gives both squared-defect bounds with the original selected epsilon. For the chronological-power integrand, OriginalRectangleMoments.payment_integrable supplies integrability of the chronological product, and payment_power identifies it pointwise with rho^(2chronologicalCount) under the same measure and parameters. Earlier blocks are paid in forward chronological time on each side; no lower bound after conditioning on a future is used. Integrability is obtained from bounded erasedBit and the conditional-expectation MemLp theorem, not from a claim that Mathlib’s L1 martingale limit is an L2 theorem.

At j=0 the two counts are empty and the bound is one, while each observation retains the full opposite infinite half-line. Natural powers preserve rho=0 and 0^0=1. No step divides by rho or eta, so eta=0 is retained. Structural zeros remain governed by the existing positive-record supplier. This source is a reusable probability bridge for a supplied original-cylinder law and original route family. The native-component theorem instantiates theta and J with nativeComponent and the exact class-restricted original law via component_restriction; choose the original routes with irreducible_rectangle_occurrence; identify P with the exact visible law used by the native-component risk definitions; and use tail_series with eta and sqrt(eta) to give both original tails. OriginalRectangleTheorem42 states those native-component and tail conclusions.

References