Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Original rectangle theorem 4.2 native component consumer

Abstract

Original rectangle theorem 4.2 native component consumer

Definition 1.1 (The actual sum of square roots of the two erasure risks).

Formalization. D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/Rectangles/OriginalRectangleTheorem42.rootErasureTail (✓ std3).

Source. Repository-derived.

Commentary.

The sum is the real tsum of the square roots of the existing leftRisk and rightRisk. The theorem below separately proves summability of this exact series for every natural lower radius.

Theorem 1.2 (The original rectangle bounds and both geometric tails on one actual component).

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

Source. Repository-derived.

Commentary.

Let theta be a finite original stationary binary edge presentation and J a probability measure with exactly theta’s original marked integer-time cylinders. Let D be an actual closed communicating class of the support of M_0+M_1, with positive original stationary mass c, and let kappa be nativeComponent(theta,D,c-positive). Fix a nonempty Boolean word w and a rectangle R for product(kappa,w), with r in its row support. The hidden type in the conclusion is exactly the subtype D; kappa keeps the original matrix entries, normalizes the original stationary masses by c, and retains the scalar stationary no11 condition. The actual closed-class structure supplies irreducibility. Periodicity and structural zeros remain unrestricted, and the original scalar stationary no11 condition supplies the labelled-route seam.

The theorem supplies a bounded positive labelled route family a from every h in D to r in the actual closed-class restriction. The route at r is empty. Each route has injective states and length at most card(D), with strict inequality when w starts with zero. When w starts with one, every nonempty selected route ends with a zero label and every incoming one-labelled matrix entry at r is zero. The occurrence probability uses the exact selectedEpsilon(kappa,w,r,a). The block length is b=length(w)+card(D); rho=1-u/v uses the minimum and maximum of the actual rectangle entries, and eta=1-epsilon*(1-rho^2).

For every integer cut t, component_restriction identifies c times the inclusion pushforward of K=jointLaw(kappa) with J restricted to state(t) in D. For every Boolean word and every two states in D, the component word-product entry equals the original word-product entry. The output coordinate is unchanged by inclusion. The same law’s visible pushforward K.map Prod.snd is identified with the existing visibleLaw(kappa) used by OriginalErasureComparison.leftRisk and rightRisk, so no convenient redefined risk or unrelated posterior law is introduced.

For every j>=0, the finite posterior ratio is the existing bitPredictor conditional expectation on the exact finite record almost everywhere, after removing the union of null observation fibers; the ordered limits retain the entire opposite infinite half-line. The left and right pointwise defects are bounded under the same class law K=jointLaw(kappa) by rho raised to the chronological original b-block counts starting at -floor(j/b)*b and 1. Squaring and the chronological occurrence moment give leftRisk(kappa,j), rightRisk(kappa,j) <= eta^(floor(j/b)). The statement preserves j=0, rho=0, eta=0, and the natural 0^0=1 convention without division by rho or eta.

For every natural R, the theorem asserts summability of the nonnegative root series, so its real sum represents the original tail. The public tail conclusion defines rootErasureTail(kappa,R) as the sum over j>=R of the square roots of the two existing risks and keeps erasureTail(kappa,R) as the existing sum of the two risks in extended reals. Existing OriginalUnifilarErasureTail.tail_series is consumed with rho=sqrt(eta) for the root tail and eta for the squared tail, yielding rootErasureTail(kappa,R) <= 2b(sqrt(eta))^(floor(R/b))/(1-sqrt(eta)), erasureTail(kappa,R) <= 2beta^(floor(R/b))/(1-eta), and rootErasureTail(kappa,0) <= 2*b/(1-sqrt(eta)). The root numerator equals eta^((floor(R/b):Real)/2): the division by two is real division, including odd floor quotients. This identity uses nonnegativity, including eta=0. The endpoint and zero-rate cases remain in the same statement.

In the displayed formula, natDiv is natural division and realCast and intCast are the indicated canonical casts. headOption and getLastOption denote the list operations head? and getLast?, respectively. productEntry is the corresponding entry of product; sum over val(D) is the finite sum over the actual subtype D. AE(K,(z:T maps to p)) means p holds for K-almost every z:T. The displayed let expressions are abbreviations, not additional hypotheses. As in the Lean statement, the tail assertions occur inside the universal quantifier over j; they do not depend on j and hold for every natural lower radius, including zero. The finite hidden type has its given measurable space and measurable singletons; J is a probability measure. The class mass is the finite sum of the original initial weights over the subtype D.

The proof combines the same-law opposite-half-line posterior comparison with the chronological original-block moment bound. The component restriction identifies the actual conditioned joint law, irreducible labelled routes give the occurrence probability, and the geometric block series bounds both tails. The contraction and occurrence estimates act on the same original law throughout.

References