Constant suspended emission separates complete endpoint laws

Abstract

A finite stationary generator with constant suspended emission cannot simultaneously center both endpoint complete laws within excess one over 35200.

RegularTable quantifies over arbitrary finite carriers X and Y, nonnegative stochastic update tables B:X to Y and A:Y to X, and probability rows pi and tau satisfying pi B=tau and tau A=pi. The emission probabilities u on X and v on Y lie in the closed interval [1/3,2/5]. No positive-entry, irreducibility, aperiodicity, independence or reversibility condition is imposed.

The output carrier is the existing RawTail=Option(List(Letter)), with Letter=Fin(2), alpha=0 and beta=1. None remains an outcome for noncompletion. Each Q(x) and W(y) is a normalized measure on the entire carrier. The table requires exact same-update recursion for every set E: Q(x)(E) equals u(x) times the indicator that [alpha] belongs to E, plus (1-u(x)) times the B(x,.) average of W evaluated on the beta-prefix preimage of E. The W recursion has immediate [beta] mass 1-v(y), followed by v(y) times the A(y,.) average of Q on the alpha-prefix preimage. Prefixing fixes none. No law is conditioned on completion.

Write Qbar and Wbar for the pi and tau averages. FullTVBound(mean,P,radius) means that the absolute difference between mean(E) and P(E) is at most radius for every complete event E. This is the event-supremum total variation convention. P is the existing Bernoulli stopped-word law, identified with the actual first-completion process by D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/FourthSegmentStoppedLaw.

In the displayed theorem, ep and eb denote epsilon_p and epsilon_beta, and inRegularInterval(s) means 1/3<=s<=2/5. constantOnPositiveSupport(R,s) means v(y)=s whenever tau(y)>0; values at zero-weight labels need not equal s. completeEndpointBounds requires FullTVBound for Qbar against both p endpoint laws, each with radius 1116529/22781250+epsilon_p, and for Wbar against both beta endpoint laws, each with radius 239/6750+epsilon_beta. The two endpoint alpha probabilities are exactly 1/3 and 2/5.

Theorem 1.1 (Every pure p type-one word has its exact singleton mass).

$$\forall r\in unitInterval,\forall j\in Nat,\mathrm{realMass}\left(\mathrm{explicitStoppedWordLaw}\left(p,r\right),\mathrm{some}\left(\mathrm{pWord}\left(j,1\right)\right)\right)=\mathrm{endpointTypeOne}\left(r,j\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ConstantSuspensionSeparator.endpoint_p_word (✓ std3). ∎

Source. Repository-derived.

Commentary.

realMass(mu,x)=mu.real({x}). For every r in the full closed unit interval and j natural, endpointTypeOne(r,j)=(1-r)^2[r(1-r)]^j is the mass of the original pWord(j,1)=(beta alpha)^j beta beta. The complete law and its infinite outcome are retained, including r=0 and r=1.

Theorem 1.2 (Uniform strict separation over every finite regular table).

$$\forall X\in FiniteType,\forall Y\in FiniteType,\forall R\in \mathrm{RegularTable}\left(X,Y\right),\forall s\in Real,\forall ep\in Real,\forall eb\in Real,(\mathrm{inRegularInterval}\left(s\right)\wedge \mathrm{constantOnPositiveSupport}\left(R,s\right)\wedge 0\le ep\wedge 0\le eb\wedge \mathrm{completeEndpointBounds}\left(R,ep,eb\right))\Rightarrow \frac{1}{35200}<\max \left(ep,eb\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ConstantSuspensionSeparator.constant_suspension_separator (✓ std3). ∎

Source. Repository-derived.

Commentary.

The acquired return table C=BA has stationary row pi. With U=1-u, one four-coordinate probability distribution has mass pi(i)C(i,j)C(j,k)C(k,l). Every coordinate has marginal pi. Positive-weight rows have no positive transition into a zero-weight row. This support fact permits the suspended constancy hypothesis to be used exactly where the recursion has positive weight.

Let m be the common mean of U and M_j the product expectation of the first j coordinates of that one distribution. The full law recursions give Qbar(pWord(j,1))=(1-s)s^j M_(j+1) for j=0,1,2,3, and Wbar(E_beta)=1-s+s(1-s)m for E_beta={[beta],alpha::pWord(0,1)}. The proof first establishes the word recursion for arbitrary natural j and the complete-event identity Wbar=(1-s)delta_beta+s alpha-prefix(Qbar). The suspended event and all four words therefore refer to the same table and the same m.

The consumed product bounds are M_2<=(19/15)m-2/5, M_3<=(271/225)m-38/75 and M_4>=(4/15)(4m-29/15). They are classical box-envelope instances described in D5/L/Analytic/xu2020polyhedral. Their finite proofs use polynomial nonnegativity inside the live derivation; no claim is made that their separate equality cases can be attained together.

Apply the full endpoint bounds to E_p={pWord(0,1),pWord(1,1),pWord(2,1)}, E_beta, and E_p union {pWord(3,1)}. Exact endpoint masses yield the two midpoint errors and Qbar(pWord(3,1))<=1944/390625+2 epsilon_p. The last bound follows by subtracting the E_p lower bound from the larger event’s upper bound. It does not replace the full-law hypothesis by a finite-probe hypothesis.

Set c=1489/6750. The same-law estimates imply Cp-F(s)<=epsilon_p+5 epsilon_beta and G(s)-1944/390625<=2 epsilon_p+epsilon_beta/5, where Cp=11758471/22781250, F(s)=(1-c/s)(1+19s/15+271s^2/225)-(2/5)s(1-s)(1+19s/15), and G(s)=(4/15)(31s^3/15+29s^4/15-4cs^2). Both functions increase on the regular interval. At s=3679/10000 their respective strict gaps exceed 1/4000 and 1/16000. The two exhaustive sides of this cut imply the displayed strict lower bound.

Application to the original installed observer. Fix any finite COMPLETE carrier Z, its source-independent Observer M with fixed M.init and acquired-operation kernels M.update, and any lawful InstalledEmitter e. Install any probability mass function mu on positive depths with mu(1)>0 and mu(2)>0. This includes finite and countably supported priors and priors supported only at depths 1 and 2. Draw one depth K before all seed and payload reads; conditional on K=k, the same rate r_k=F_(k+1)/F_(k+3) supplies every original read. The endpoint rates are r_1=1/3 and r_2=2/5. Both seeds, every rejected seed pair, partial parse, completion, fourth return, held record, original finite permission field and deterministic event block are retained. Analysis posteriors and common rows are not installed registers.

For phase s, let H range over the entire original positive active fourth-phase history domain PhaseHistory(s), including arbitrarily many fourth returns. Active risk cuts exclude pending matching-Stop cuts. Their complete future laws still retain the matching Stop, held records, completion and delivery through fullRenderer. The original law fullLaw(M,e,z) comes from the installed marked trajectory, not an arbitrarily assigned residual law. The actual row row(M,H) weights configuration total variation before averaging. installedRisk(M,e,mu,s) is the supremum of these configuration losses against the original fullTarget(mu,H). It is finite and at most one by probability_tv_le_one and risk_finite in NativePaidHistoryCommonRowRisks. Define ep=installedRisk(p).toReal-1116529/22781250, eb=installedRisk(beta).toReal-239/6750 and e(M)=max(ep,eb). The real conversion uses finite ENNReal sums, products and TV before subtraction; it does not replace configuration risk by TV of a mean law.

Constancy means that there exists one s0 in [0,1] such that e.emit(y,read alpha).toReal=s0 for every positive configuration in every positive active suspended history on the original seed-1, marker-100 held-record fibre. In native parameters, the condition is H.source.finiteFields=heldFields(beta), normalizer(mu,H)>0 and row(M,H,y)>0. Other fibres remain arbitrary. This includes s0=0 and s0=1, transient modes, zero or unit emissions, reducible and periodic acquired kernels, and noncompletion. It requires neither equal suspended complete laws nor equal successor rows.

Use NativePaidHistoryCommonRowRisks.native_complete_common_rows once to obtain pi and tau before selecting any supported depth. Put B(x,y)=M.update(read beta,x,y) and A(y,x)=M.update(read alpha,y,x); their PMF binds satisfy pi B=tau and tau A=pi. The same rows bound every supported depth’s tail-law configuration loss by its original phase risk. Each positive row entry has an actual positive windowPhaseHistory witness on heldFields, with positive original normalizer, positive acquired row and exact renderer identity. Hence constancy transports to every positive tau entry. This extraction does not assume that the original process is stationary or that every reachable state lies in the stationary support.

On X=pi.support and Y=tau.support the acquired rows are closed: a positive B successor of X lies in Y, and a positive A successor of Y lies in X. Restriction therefore loses no transition mass. FinitePmfLikelihood.pmfRealMass_sum, with Output(i)=Z and i=0, normalizes all real PMF rows. NativePaidHistoryCommonRowLimits.bind_real gives the two stationary real-weight identities. The extracted rows are analysis weights on the same implementation, not independently optimized phase laws.

Write rawLaw(s,z) for tailLaw(M,e,s,z) pushed forward by Subtype.val from ValidTail(s) to RawTail. RarePriorAbsoluteRisk.subtype_tv preserves its full TV, for arbitrary measures on ValidTail(s). NativeInstalledFullLaw.marked_regenerate, marked_head and marked_some_mass give its actual normalized generation: at p, Q_x(E)=u_x 1_[alpha in E]+(1-u_x) sum_y B(x,y) W_y(beta-prefix preimage E); at beta, W_y(E)=(1-v_y) 1_[beta in E]+v_y sum_x A(y,x) Q_x(alpha-prefix preimage E). Here u and v are the original read-alpha probabilities. The laws come from marked trajectories and include none. These equations hold for every complete event, also when an emission is zero. The incoming mark is discarded only by the original rawFrom projection, not by resetting any runtime configuration.

To see the continuation map directly, stopped_word_fiber and parses_normal_form characterize every finite stopped word. Prefixing beta at p or alpha at suspension sends a finite word w to the prefixed word and fixes none; prefixing the completing read produces respectively [alpha] or [beta]. The Option cases preserve the never-completing branch. Applying marked_head before the trajectory pushforward yields the displayed complete-event equations. The original lawful emitter rules out none and Stop only at active controls. FourthSegmentStoppedLaw.actual_fourth_segment_stopped_word_law identifies the two pure tail pushforwards with explicitStoppedWordLaw(s,r_k), including depths 1 and 2. No original termination premise enters this reconstruction.

Clamp each active read-alpha probability by c(t)=max(1/3,min(2/5,t)). Generate read beta with complementary probability and keep the original emitter elsewhere, using the same M.init and every M.update. This gives a lawful installed comparison emitter, not an assignment of unsupported off-fibre laws. Its complete trajectory pushforwards Qhat and What are probability measures at every configuration. Restrict them to X and Y with the same acquired B,A,pi,tau. The preceding all-event equations and closed support normalization prove every RegularTable generation and stationarity field. No source call, real sampling certificate or resource-preservation assertion is added.

The finite endpoint clipping estimate uses configuration laws before TV. For any complete probability law T, disjoint measurable E,G, endpoint laws P_a,P_b with G masses a<=b and E mass difference g, apply event_gap to E and E union G for both endpoints. measureReal_union gives the four atomic inequalities. The three cases T(G)<=a, a<=T(G)<=b, and b<=T(G) yield |T(G)-max(a,min(b,T(G)))|<=TV(T,P_a)+TV(T,P_b)-g. This needs neither countable L1 summation nor a pointwise minimax center.

At p use E_p={pWord(0,1),pWord(1,1),pWord(2,1)} and the disjoint singleton G={[alpha]}. NativePeriodicWordLaw.endpoint_coordinates at (s,n,b)=(p,0,0) gives the exact immediate mass r. At suspension use E_beta complement and G={[beta]}, with the endpoints reversed; endpoint_immediate gives 1-r. The supplied endpoint_p_event and endpoint_beta_event identities make g equal to twice the respective radius. Actual immediate-stop identities make T(G) equal to u at p and 1-v at suspension. Averaging the two endpoint configuration budgets on the common rows gives du=sum_x pi_x |u_x-c(u_x)|<=2ep and dv=sum_y tau_y |v_y-c(v_y)|<=2eb. Since du,dv are nonnegative, this also proves ep,eb>=0 directly from the original risks.

Every comparison survival event S_n contains none and every finite word longer than n. Prefixing pulls S_(n+1) back to S_n; the completing singleton has no mass there. The comparison equations and continuation bounds 2/3 and 2/5 give two-read domination by 4/15. Let F(n) be the maximum of zero and all Qhat_x(S_(2n)), What_y(S_(2n)). Finite maximum monotonicity gives F(n+1)<=(4/15)F(n) and F(0)<=1. Pinned Mathlib le_geom then gives F(n)<=(4/15)^n. Since {none} is contained in every S_(2n), measure monotonicity and the geometric limit prove both Qhat_x({none})=0 for every x and What_y({none})=0 for every y. These two conclusions concern regenerated comparison laws; the original laws may still have positive none mass.

Let DQ=sum_x pi_x TV(Q_x,Qhat_x) and DW=sum_y tau_y TV(W_y,What_y), on complete laws. For each event, subtract the original and comparison equations in the form (t-tprime)(indicator-K)+(1-tprime)(K-Kprime). The mixture event mass K lies in [0,1]; the finite triangle bound controls |K-Kprime| by the weighted successor TVs. Taking the complete-event supremum gives the one-step estimate with the comparison continuation coefficient. Weighting by pi and tau and using the same acquired stationarity yields DQ<=du+(2/3)DW and DW<=dv+(2/5)DQ. Solve these inequalities to get DQ<=(15du+10dv)/11<=(30ep+20eb)/11 and DW<=(6du+15dv)/11<=(12ep+30eb)/11. All events, including none, remain quantified. Original contraction, mixing or completion are not assumed.

The actual weighted endpoint configuration bounds and the complete-TV triangle inequality now imply FullTVBound for Qhatbar against each p endpoint with allowance hp=(41ep+20eb)/11, and for Whatbar against each suspended endpoint with allowance hb=(12ep+41eb)/11, in addition to the original radii. Both means use the same actual pi,tau and the same regenerated table. The actual-history witnesses transport suspended constancy to vhat_y=c(s0) throughout positive tau support. Apply constant_suspension_separator with this common s, hp and hb. It gives max(hp,hb)>1/35200, while max(hp,hb)<=(61/11)max(ep,eb). Therefore the original observer satisfies e(M)>1/195200. The geometric zero-none clauses are additional comparison consequences; this final separator argument uses full TV and does not assume them for the original laws.

The quantifiers cover all finite COMPLETE carriers and every finite or countable installed prior with positive endpoint masses. Taking the infimum of e(M) over the whole constant-suspension class gives a non-strict lower bound 1/195200; no uniform strict margin beyond that number follows. The class is nonempty, for example the original finite-control observer with deterministic active read-alpha emission, its lawful matching Stop and an endpoint-only prior. Nothing here claims a positive unrestricted infimum, a common exact unrestricted attainer, a vanishing family, a fixed-resource optimum or preservation of any hard defect budget.

For an exact common configuration attainer, ep=eb=0 contradicts the constant-suspension bound. Failure of constancy means that two original positive suspended configuration-history pairs on the designated fibre have distinct alpha emission probabilities. To justify this existential consequence, choose one positive suspended pair from the common-row history witness; if every other such pair had the same probability, that value would lie in [0,1] and satisfy the original constancy definition. For any sequence of original observers, allowing carriers, emitters and installed priors to vary, whose two real excesses tend to zero, the maximum is eventually below 1/195200. Every sufficiently late member therefore has those two distinct original reachable suspended emissions. No uniform interior prior mass, recurrence or fixed carrier assumption is introduced.

Boundary cases preserve the scope of the application. With original u=0,v=1, the actual generator never completes and its complete laws are delta_none; both comparisons have zero none mass, so both complete TVs are exactly one and the perturbation bounds saturate. Constant s0=0 or s0=1, endpoint-only priors, periodic and reducible acquired updates and actual transient positive histories remain included. Acquired stationarity cannot be replaced by stationarity after multiplying by emission probabilities. Averaging configuration laws before TV can cancel opposite discrepancies, so a bound on TV of a mean law cannot supply the configuration clipping budget. These distinctions concern one common implementation and do not change the original history domain or physical-variable interpretation.

Theorem 1.3 (Normalization of every complete stopped-word law).

$$\forall phase\in \mathrm{ActivePhase}\left(\right),\forall r\in \mathrm{unitInterval}\left(\right),\mathrm{IsProbabilityMeasure}\left(\mathrm{explicitStoppedWordLaw}\left(phase,r\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ConstantSuspensionSeparator.endpoint_probability (✓ std3). ∎

Source. Repository-derived.

Commentary.

This is the probability normalization of the existing actual fourth-segment pushforward for either active phase and every unit-interval parameter. The infinite return outcome remains in the carrier. The absolute-risk estimates consume this original supplier directly.

Theorem 1.4 (The source p witness event mass).

$$\forall r\in unitInterval,\mathrm{EndpointPEvent}\left(r\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ConstantSuspensionSeparator.endpoint_p_event (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every Bernoulli alpha rate r in [0,1], the real mass of RegularTable.pEvent under explicitStoppedWordLaw(p,r) is (1-r)^2 times (1+r(1-r)+(r(1-r))^2). The event consists of pWord(0,1), pWord(1,1) and pWord(2,1).

Theorem 1.5 (The source suspended witness event mass).

$$\forall r\in unitInterval,\mathrm{EndpointBetaEvent}\left(r\right)$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ConstantSuspensionSeparator.endpoint_beta_event (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every Bernoulli alpha rate r in [0,1], the real mass of RegularTable.betaEvent under explicitStoppedWordLaw(beta,r) is 1-r+r(1-r)^2. Its immediate completion singleton some[1] is contained in this event.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ConstantSuspensionSeparator.constant_suspension_separator
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ConstantSuspensionSeparator.endpoint_beta_event
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ConstantSuspensionSeparator.endpoint_p_event
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ConstantSuspensionSeparator.endpoint_p_word
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ConstantSuspensionSeparator.endpoint_probability
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/FourthSegmentStoppedLaw
• Narrative reference: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/FourthSegmentStoppedLaw