Stopped-length continuity and deterministic depth separation

Abstract

The complete original phase-p length law is uniformly continuous while distinct deterministic depths remain separated.

D(r) denotes the existing explicitStoppedWordLaw(p,r) pushed through lengthProjection. nativeLengthPushforward(r) is rawReadLaw(r) pushed through the actual stoppedReadWord(p) followed by lengthProjection. noncompletionMass(r) is rawReadLaw(r) of the event stoppedReadWord(p)=none. The output carrier remains Option Nat: none is infinite noncompletion, and some zero is an impossible finite length. realMass is the real value of the indicated singleton measure; mass retains its extended nonnegative real value.

For every real t and natural j, A(j) and B(j) are the polynomial coordinate extensions below. Their values at a unit-interval parameter are the complete odd and even singleton masses. coordinateDerivative(r)(j) is the sum of the two absolute derivatives, so its series includes every positive length exactly once.

$$\forall j:Nat,(\forall t:Real,((A(j,t)=(t)\ast ({((t)\ast ((1-t)))}^j))\wedge (B(j,t)=({((1-t))}^2)\ast ({((t)\ast ((1-t)))}^j))))$$

$$\forall r:Real,(\forall j:Nat,(\mathrm{coordinateDerivative}(r,j)=(|\mathrm{deriv}(A(j),r)|+|\mathrm{deriv}(B(j),r)|)))$$

TV is the existing measurableTotalVariation: the supremum of the larger of the two directed event-mass gaps over all measurable events. It takes extended nonnegative real values. ofReal embeds a real bound in that carrier. Depth is the original positive natural depth carrier, and rate(k)=fib(k+1)/fib(k+3). The addition k+1 in the display means the positive depth with that natural value; fib uses F(0)=0 and F(1)=1.

$$\forall n:Nat,(\mathrm{adjacentLengthTV}(n)=\mathrm{TV}(D(\mathrm{rate}((n+1))),D(\mathrm{rate}((n+2)))))$$

$$\forall n:Nat,(\mathrm{adjacentFibonacciBound}(n)=\mathrm{ofReal}(\frac{12}{((7)\ast (\mathrm{fib}((n+4))))\ast (\mathrm{fib}((n+5)))}))$$

Theorem 1.1 (The full quantitative law).

$$(\forall r:unitInterval,((\mathrm{nativeLengthPushforward}(r)=D(r))\wedge (\mathrm{noncompletionMass}(r)=0)\wedge (\mathrm{mass}(D(r),none)=0)\wedge (\mathrm{mass}(D(r),\mathrm{some}(0))=0)\wedge (\forall j:Nat,((\mathrm{realMass}(D(r),\mathrm{some}(((2)\ast (j)+1)))=(r)\ast ({((r)\ast ((1-r)))}^j))\wedge (\mathrm{realMass}(D(r),\mathrm{some}(((2)\ast (j)+2)))=({((1-r))}^2)\ast ({((r)\ast ((1-r)))}^j))))))\wedge (\forall r:Real,((r\in [\frac{1}{3},\frac{2}{5}])\Rightarrow ((\mathrm{Summable}(\mathrm{coordinateDerivative}(r)))\wedge ((\frac{1}{2})\ast (\mathrm{tsum}(\mathrm{coordinateDerivative}(r)))\le \frac{(2)\ast ((1-r))}{(1-(r)\ast ((1-r)))})\wedge (\frac{(2)\ast ((1-r))}{(1-(r)\ast ((1-r)))}\le \frac{12}{7}))))\wedge (\forall r:unitInterval,(\forall s:unitInterval,(((r\in [\frac{1}{3},\frac{2}{5}])\wedge (s\in [\frac{1}{3},\frac{2}{5}]))\Rightarrow (\mathrm{TV}(D(r),D(s))\le \mathrm{ofReal}((\frac{12}{7})\ast (|(r-s)|))))))\wedge (\forall k:Depth,((|(\mathrm{rate}(k)-\mathrm{rate}((k+1)))|=\frac{1}{(\mathrm{fib}((k+3)))\ast (\mathrm{fib}((k+4)))})\wedge (\mathrm{TV}(D(\mathrm{rate}(k)),D(\mathrm{rate}((k+1))))\le \mathrm{ofReal}(\frac{12}{((7)\ast (\mathrm{fib}((k+3))))\ast (\mathrm{fib}((k+4)))}))))\wedge (\mathrm{Tendsto}(adjacentFibonacciBound,atTop,\mathrm{nhds}(0)))\wedge (\mathrm{Tendsto}(adjacentLengthTV,atTop,\mathrm{nhds}(0)))\wedge (\forall k:Depth,(\forall l:Depth,((k\ne l)\Rightarrow (\mathrm{TV}(\mathrm{dirac}(k),\mathrm{dirac}(l))=1))))$$

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

Source. Repository-derived.

Commentary.

The native stopped-word theorem supplies the original parser pushforward and proves zero mass of infinite noncompletion. The existing length projection and its all-index atom identities give the two complete coordinate families; no completion conditioning or finite cutoff is used.

Differentiating each polynomial coordinate gives an absolutely summable family. The geometric series and its weighted derivative series bound half its absolute derivative sum by 2(1-r)/(1-r(1-r)), which is at most 12/7 throughout the closed interval [1/3,2/5]. The endpoint cases are included.

For ordered r at most s, the original stopped-word measures share a submeasure with odd weights r xi(r)^j and even weights (1-s)^2 xi(r)^j. Its total mass is (r+(1-s)^2)/(1-xi(r)). The event-supremum distance is at most the missing common mass, hence at most (s-r)(2-r-s)/(1-xi(r)), and therefore at most (12/7)(s-r). Symmetry covers the reverse order, including r=s, and measurable length projection contracts TV.

Vajda’s Fibonacci identity gives the exact adjacent response-rate gap. The quantitative estimate applies to every positive depth; reciprocal Fibonacci products converge to zero, so the full adjacent output-law distances converge to zero. The singleton event at either of two distinct positive depths gives Dirac-law distance one.

These are different deterministic-depth sources. This result does not assert the stronger theorem about actual histories under one fixed installed prior. Exact length-law recovery is compatible with the loss of a uniform inverse stability estimate across unbounded deterministic source depths.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/FourthSegmentLengthStability.original_stopped_length_stability
• Dependency: D5/S1/Recurrence/FibVajda
• Dependency: D5/S3/Estimation/DataProcessing/MeasurableTotalVariationTriangle
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/FourthSegmentLawRecovery
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorAbsoluteRisk