Full coordinates and the original stationary class

Abstract

Identification of the surviving native law

Actual native laws on the full legal carriers

Theorem 1.1 (inclusion embedding).

$$\forall s:ActivePhase,\mathrm{MeasurableEmbedding}\left(\mathrm{legalSubtypeInclusion}\left(s\right)\right)$$

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

Source. Repository-derived.

Commentary.

legalSubtypeInclusion(s) is Subtype.val from ValidTail(s) to RawTail. Its injectivity and the countable measurable image give the exact comap interface used by complete continuous laws.

Theorem 1.2 (stopped legal).

$$\forall s:ActivePhase,\forall omega:Stream,\mathrm{Valid}\left(s,\mathrm{stoppedReadWord}\left(s,omega\right)\right)$$

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

Source. Repository-derived.

Commentary.

The original stopped parser lands in the complete legal carrier, including the noncompletion outcome.

Theorem 1.3 (geometric tail).

$$\forall z:ENNReal,\forall D:ENNReal,\forall j:Nat,\mathrm{tsumRestrictedGeometric}\left(z,D,j\right)=z^j\cdot \mathrm{tsumGeometric}\left(z,D\right)$$

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

Source. Repository-derived.

Commentary.

tsumRestrictedGeometric(z,D,j) is the sum over n:Nat of Dz^n when j<=n and zero otherwise. tsumGeometric(z,D) is the sum over all n:Nat of Dz^n. The identity holds for all extended nonnegative parameters, including infinity. It is consumed by every continuous source tail.

Theorem 1.4 (p atom tail).

$$\forall j:Nat,\forall n:Nat,\forall i:Letter,\mathrm{member}\left(\mathrm{pAtom}\left(n,i\right),\mathrm{tailSet}\left(p\left(\right),j\right)\right)\iff j\le n$$

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

Source. Repository-derived.

Commentary.

All p completion atoms have their original tail depth.

Theorem 1.5 (beta atom tail).

$$\forall j:Nat,\forall n:Nat,\forall i:Letter,\mathrm{member}\left(\mathrm{betaAtom}\left(n,i\right),\mathrm{tailSet}\left(\mathrm{beta}\left(\right),j\right)\right)\iff j\le n$$

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

Source. Repository-derived.

Commentary.

The same complete suspended atoms retain their original tail depth.

Theorem 1.6 (beta stop not tail).

$$\forall j:Nat,\mathrm{notMember}\left(\mathrm{betaStop}\left(\right),\mathrm{tailSet}\left(\mathrm{beta}\left(\right),j\right)\right)$$

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

Source. Repository-derived.

Commentary.

The immediate suspended stop is outside each return tail.

native(s,r) is the comap of the actual explicitStoppedWordLaw(s,r) along legal subtype inclusion. The actual stopped-word map always lands in the legal range; that range has mass one. Thus native is a probability law, rather than an unnormalized comap. endpoint(false)=1/3 and endpoint(true)=2/5. nativeEndpoint(s,b) bundles this actual law with the exact Regular predicate.

Theorem 1.7 (native coordinate).

$$\forall s:ActivePhase,\forall r:UnitInterval,\forall t:ValidTail,\mathrm{mass}\left(\mathrm{native}\left(s,r\right),t\right)=\mathrm{mass}\left(\mathrm{explicitStoppedWordLaw}\left(s,r\right),\mathrm{val}\left(t\right)\right)$$

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

Source. Repository-derived.

Commentary.

The atom t ranges over ValidTail(s), including infinity. Measurable subtype inclusion is injective and comap evaluates its singleton image exactly.

Theorem 1.8 (native atoms).

$$\forall r:UnitInterval,(\forall n:Nat,\forall i:Letter,\mathrm{mass}\left(\mathrm{native}\left(p\left(\right),r\right),\mathrm{pAtom}\left(n,i\right)\right)=\mathrm{markerCoefficient}\left(r,i\right)\cdot {\mathrm{alphaMass}\left(r\right)\cdot \mathrm{betaMass}\left(r\right)}^n)\wedge ((\mathrm{mass}\left(\mathrm{native}\left(\mathrm{beta}\left(\right),r\right),\mathrm{betaStop}\left(\right)\right)=\mathrm{betaMass}\left(r\right))\wedge ((\forall n:Nat,\forall i:Letter,\mathrm{mass}\left(\mathrm{native}\left(\mathrm{beta}\left(\right),r\right),\mathrm{betaAtom}\left(n,i\right)\right)=\mathrm{alphaMass}\left(r\right)\cdot \mathrm{markerCoefficient}\left(r,i\right)\cdot {\mathrm{alphaMass}\left(r\right)\cdot \mathrm{betaMass}\left(r\right)}^n)\wedge (\forall s:ActivePhase,\mathrm{mass}\left(\mathrm{native}\left(s,r\right),\mathrm{infinity}\left(s\right)\right)=0)))$$

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

Source. Repository-derived.

Commentary.

markerCoefficient(r,i) means alphaMass(r) when i=0 and betaMass(r)^2 otherwise. alphaMass(r)=r and betaMass(r)=1-r as ENNReal masses. The complete list is pAtom(n,0): r z^n; pAtom(n,1): (1-r)^2 z^n; betaStop: 1-r; betaAtom(n,0): r^2 z^n; betaAtom(n,1): r(1-r)^2 z^n; infinity in either phase: zero.

Theorem 1.9 (native tails).

$$\forall r:UnitInterval,\forall j:Nat,(\mathrm{mass}\left(\mathrm{native}\left(p\left(\right),r\right),\mathrm{tailSet}\left(p\left(\right),j\right)\right)={\mathrm{alphaMass}\left(r\right)\cdot \mathrm{betaMass}\left(r\right)}^j)\wedge (\mathrm{mass}\left(\mathrm{native}\left(\mathrm{beta}\left(\right),r\right),\mathrm{tailSet}\left(\mathrm{beta}\left(\right),j\right)\right)=\mathrm{alphaMass}\left(r\right)\cdot {\mathrm{alphaMass}\left(r\right)\cdot \mathrm{betaMass}\left(r\right)}^j)$$

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

Source. Repository-derived.

Commentary.

Countable legal atom reconstruction, word injectivity and shifted geometric sums give every exact tail. The p normalization fixes the full series sum. At j=0 the suspended tail is r, not one.

Theorem 1.10 (native endpoint residualA).

$$\forall b:Bool,\mathrm{residualA}\left(\mathrm{nativeEndpoint}\left(\mathrm{beta}\left(\right),b\right)\right)=\mathrm{law}\left(\mathrm{nativeEndpoint}\left(p\left(\right),b\right)\right)$$

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

Source. Repository-derived.

Commentary.

prependA sends every p completion atom to the corresponding beta atom and preserves infinity. Native atom evaluation gives its full comap law; the original nonzero alpha mass normalizes the entire residual.

For every theta in [0,1], the endpoint application uses unweighted marginals (1-theta) Dirac(native_a)+theta Dirac(native_b) and joint edge measures on the corresponding endpoint pairs. Deterministic Borel acquired kernels select the matching opposite endpoint. Singleton comap identities, including infinity, normalize both B and A residuals; each coordinate is one of the two comparison endpoints and hence satisfies the full min/max boxes. The upper native singleton has mass theta, including theta=0 and theta=1. This finite boundary application does not restrict the arbitrary Borel margins in the singleton-limit theorem.

F is an arbitrary original boxed Borel CommonFlow. All probability descriptors retain every finite legal tail and the infinite noncompletion coordinate. CRow(F,Q) is the original unweighted acquired return row, T=L/(6/25), and q is the decreasing limit of T to the power n applied to threeStepAverage. CoreAt asserts the original goodP conditions, h>=3/25, Th<=h, Tq=q, nonzero q implies zero excess, almost every B successor satisfies goodB, and almost every C edge preserves sixthFunctional. GoodP retains the full normalized B residual, its endpoint box, every coordinate recursion, the completion identity and bounds, and the third-step box; goodB retains the full normalized A residual and its endpoint box. AE denotes almost everywhere, sequence(n,x) the sequence with index n, nhds the neighborhood filter, and ite the indicated conditional value.

Theorem 1.11 (An absorbing conull core).

$$\forall F:CommonFlow,\exists G\subset PDescriptor,\mathrm{MeasurableSet}\left(G\right)\wedge \mathrm{AE}\left(\mathrm{nuP}\left(F\right),Q,Q\in G\right)\wedge \forall Q\in G,\mathrm{CoreAt}\left(F,Q\right)\wedge \mathrm{AE}\left(\mathrm{CRow}\left(F,Q\right),R,R\in G\wedge \mathrm{sixthFunctional}\left(F,R\right)=\mathrm{sixthFunctional}\left(F,Q\right)\right)$$

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

Source. Repository-derived.

Commentary.

Enclose the exceptional set in a measurable null set. Repeatedly intersect its complement with the states whose C row assigns zero mass to the previous complement. Stationarity makes every finite stage conull. Their countable intersection is conull and absorbing under the same C. The original full residuals and both endpoint boxes remain available there.

Theorem 1.12 (Survival identifies the actual upper law).

$$\forall F:CommonFlow,\exists G\subset PDescriptor,\mathrm{MeasurableSet}\left(G\right)\wedge \mathrm{AE}\left(\mathrm{nuP}\left(F\right),Q,Q\in G\right)\wedge (\forall Q\in G,\mathrm{CoreAt}\left(F,Q\right)\wedge \mathrm{AE}\left(\mathrm{CRow}\left(F,Q\right),R,R\in G\wedge \mathrm{sixthFunctional}\left(F,R\right)=\mathrm{sixthFunctional}\left(F,Q\right)\right))\wedge \forall Q\in G,(q\left(F,Q\right)\ne 0)⟺Q=\mathrm{nativeEndpoint}\left(p,true\right)$$

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

Source. Repository-derived.

Commentary.

On the positive sixth-functional class, acquired edge constancy makes the class absorbing and stationary localization gives g=9/25. In g=(1-u)B(1-v), both factors are at least 3/5, so equality forces u=2/5 and v=2/5 on almost every actual B successor. Hence L=(6/25)C there. Induction identifies both letter coordinates at every depth; the original regular tail bound gives zero infinite-coordinate mass. Equality of all singleton masses on the complete countable legal-tail carrier identifies the full upper native probability measure. Conversely, at an actual upper native input every normalized g coordinate equals 9/25. The inequality g<=3threeStepAverage forces a positive harmonic limit.

Theorem 1.13 (The original pointwise and averaged limits).

$$\forall F:CommonFlow,\mathrm{AE}\left(\mathrm{nuP}\left(F\right),Q,q\left(F,Q\right)=\mathrm{ite}\left(Q=\mathrm{nativeEndpoint}\left(p,true\right),\mathrm{endpointCompletion}\left(\right),0\right)\wedge \frac{q\left(F,Q\right)}{\mathrm{threeStepAverage}\left(F,Q\right)}=\mathrm{ite}\left(Q=\mathrm{nativeEndpoint}\left(p,true\right),1,0\right)\right)\wedge \mathrm{AE}\left(\mathrm{nuP}\left(F\right),Q,\mathrm{Tendsto}\left(\mathrm{sequence}\left(n,\frac{\mathrm{coordinate}\left(n,1,Q\right)}{{\mathrm{endpointRate}\left(\right)}^n}\right),atTop,\mathrm{nhds}\left(\mathrm{ite}\left(Q=\mathrm{nativeEndpoint}\left(p,true\right),\mathrm{endpointCompletion}\left(\right),0\right)\right)\right)\right)\wedge \mathrm{Tendsto}\left(\mathrm{sequence}\left(n,\frac{\mathrm{lintegral}\left(\mathrm{nuP}\left(F\right),Q,\mathrm{coordinate}\left(n,1,Q\right)\right)}{{\mathrm{endpointRate}\left(\right)}^n}\right),atTop,\mathrm{nhds}\left(\mathrm{endpointCompletion}\left(\right)\cdot \mathrm{measure}\left(\mathrm{nuP}\left(F\right),\mathrm{singleton}\left(\mathrm{nativeEndpoint}\left(p,true\right)\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

On the surviving class h=q=9/25. Elsewhere q=0 and 0<=T^n g<=3*T^n h tends to zero. The full coordinate recursion converts this into the original singleton ratio limit. The common bound 30 on all normalized iterates permits dominated convergence on the unchanged original margin. The integral of the native singleton indicator is its actual original marginal mass. These conclusions require neither finite support, mixing, reversibility nor deterministic successors.

Theorem 1.14 (Actual beta and return successors).

$$\forall F:CommonFlow,\mathrm{AE}\left(\mathrm{nuP}\left(F\right),Q,(q\left(F,Q\right)\ne 0)\Rightarrow u\left(Q\right)=\mathrm{upper}\left(\right)\wedge \mathrm{LRow}\left(F,Q\right)=\mathrm{smul}\left(\mathrm{endpointRate}\left(\right),\mathrm{CRow}\left(F,Q\right)\right)\wedge \mathrm{AE}\left(\mathrm{BRow}\left(F,Q\right),W,W=\mathrm{nativeEndpoint}\left(beta,true\right)\wedge \mathrm{AE}\left(\mathrm{ARow}\left(F,W\right),R,R=\mathrm{nativeEndpoint}\left(p,true\right)\right)\right)\right)$$

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

Source. Repository-derived.

Commentary.

The actual C row remains in the positive class, so almost every actual A successor on almost every B edge is the full upper p descriptor. The original normalized A residual is therefore exactly that native p law. Reconstruct the full suspended law from its stop mass and the image of its entire residual, including infinity. With v=2/5 this is the upper beta native descriptor. This identifies the given B/A successors rather than replacing their barycentres by sampled laws.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.beta_atom_tail
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.beta_stop_not_tail
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.common_flow_absorbing_core
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.common_flow_surviving_native
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.common_flow_surviving_transitions
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.common_flow_upper_endpoint_limits
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.geometric_tail
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.inclusion_embedding
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.native_atoms
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.native_coordinate
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.native_endpoint_residualA
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.native_tails
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.p_atom_tail
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelEndpointIdentification.stopped_legal
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/NativeBorelStationaryLocalization