Prefix probabilities reconstruct a detached consecutive path

Abstract

Prefix probabilities reconstruct a detached consecutive path

Bias consists of a real parameter p strictly between zero and one and different from one half. Its spin masses are pi(false)=1-p and pi(true)=p. Write T(n)=(1-p)^n+p^n and d(n)=T(n)-T(n+1). All finite-spin probabilities refer to one common iid assignment on the finite integer window V.

pathEdges(L,n) is the integer interval from L to L+n-1 and pathVertices(L,n) runs from L to L+n. zeroEdges(E) says that both endpoint spins of every edge in E agree. SupportsEdges requires both endpoints of every listed edge to lie in V. PrefixMasses means that every nonempty prefix of length r has zero-edge probability T(r+1).

Theorem 1.1 (Every new edge extends an endpoint).

$$\forall (\mathrm{beta}:\mathrm{Bias}),(\forall (V:\mathrm{Finset}(\mathrm{Int})),(\forall (\mathrm{es}:\mathrm{List}(\mathrm{Int})),(((\mathrm{SupportsEdges}(V,\mathrm{es}))\wedge (\mathrm{PrefixMasses}(\mathrm{beta},V,\mathrm{es}))\wedge (1\le \mathrm{length}(\mathrm{es})))\to ((\mathrm{Nodup}(\mathrm{es}))\wedge (\exists (L:\mathrm{Int}),(\mathrm{toFinset}(\mathrm{es})=\mathrm{pathEdges}(L,\mathrm{length}(\mathrm{es}))))))))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/StoppingLaw/PathRigidity.prefixes_force_consecutive (✓ std3). ∎

Source. Repository-derived.

Commentary.

Induction appends one edge at a time. A repeated edge retains the old prefix mass. A detached edge gives a strictly different factorized mass. Both alternatives contradict the prescribed next prefix mass, leaving exactly the two adjacent endpoint extensions. Query order need not be monotone.

Theorem 1.2 (Joint masses also separate the target vertex).

$$\forall (\mathrm{beta}:\mathrm{Bias}),(\forall (V:\mathrm{Finset}(\mathrm{Int})),(\forall (\mathrm{es}:\mathrm{List}(\mathrm{Int})),(\forall (q:\mathrm{Int}),(((1\le \mathrm{length}(\mathrm{es}))\wedge (\mathrm{SupportsEdges}(V,\mathrm{es}))\wedge (\mathrm{PrefixMasses}(\mathrm{beta},V,\mathrm{es}))\wedge (\forall (s:\mathrm{Bool}),(\mathrm{prob}(\mathrm{beta},V,\mathrm{inter}(\mathrm{zeroEdges}(\mathrm{toFinset}(\mathrm{es})),\mathrm{spinEvent}(q,s)))=(\mathrm{pi}(\mathrm{beta},s)\ast T(\mathrm{beta},(\mathrm{length}(\mathrm{es})+1))))))\to ((\mathrm{Nodup}(\mathrm{es}))\wedge (\exists (L:\mathrm{Int}),((\mathrm{toFinset}(\mathrm{es})=\mathrm{pathEdges}(L,\mathrm{length}(\mathrm{es})))\wedge (\mathrm{notMem}(q,\mathrm{pathVertices}(L,\mathrm{length}(\mathrm{es})))))))))))$$

Proof. Machine-checked in Lean as D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/StoppingLaw/PathRigidity.finite_path_geometry (✓ std3). ∎

Source. Repository-derived.

Commentary.

spinEvent(q,s) is the set of source spins with S(q)=s. If q lay on the recovered path, the two conditional zero-prefix probabilities would force (1-p)^n=p^n for positive n. The biased interior parameter excludes this equality. Both target-spin sections are required.

The finite product factorizations concern the same source realization. Positivity and strict mass gaps hold for every permitted bias; no numerical approximation is used.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/StoppingLaw/PathRigidity.finite_path_geometry
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/StoppingLaw/PathRigidity.prefixes_force_consecutive
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/StoppingLaw/SemanticNormalization