Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Same-seed stopping-law rigidity and sharp actual-read bounds

Abstract

Same-seed stopping-law rigidity and sharp actual-read bounds

The probability space is the original source law times an arbitrary probability measure nu on an arbitrary measurable seed space U. No atomlessness, standard Borel assumption or extra randomizer is required. The full joint law retains the unchanged seed together with the hidden endpoint, output, return indicator and paid count. A seed-independent input observation has no seed argument.

The witness stoppingRule(j,k) reads j+2i+1 for i from one through k, returns a1 at the first one reply and returns a0 after k zero replies. Its addresses and decisions depend on neither the bias nor the seed. Write W for this original-rule witness and T(n)=(1-p)^n+p^n.

The nonzero stopping masses, for each Boolean s, are pi(s)d(i)/2 at (b(s),a(true),true,i) for 1 <= i <= k; pi(s)T(k+1)/2 at (b(s),a(false),true,k); and pi(s)/2 at (a(s),a(false),true,k). Every other observation has mass zero, including every nonreturn and zero-count observation. Here d(i)=T(i)-T(i+1)=pi(false)^ipi(true)+pi(true)^ipi(false), which is strictly positive.

Theorem 1.1 (Full joint equality determines almost every seed section).

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

Source. Repository-derived.

Commentary.

independentJointLaw(beta,nu,w) is the pushforward of sourceLaw(beta).prod(nu) by (source,u) mapped to (u,w(source)); fiber(w,z) is its source observation fiber. Positive-measure countable tree fibers permit cancellation of their seed mass. Null fibers are discarded by one countable union. All observation equalities hold simultaneously, without conditioning on singleton seeds.

Theorem 1.2 (Exact witness law on every seed rectangle).

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

Source. Repository-derived.

Commentary.

rectangleSingleton(B,z) is B times the singleton observation z. stoppingMass gives every listed atom and gives zero to every unlisted tuple. In the opposite phase the witness reads only separators and returns a0 at depth k; in the active phase its first one reply ends the run, so early terminal depths are exact.

Theorem 1.3 (Almost every raw seed has the exact stopping path).

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

Source. Repository-derived.

Commentary.

This statement quantifies arbitrary completion-lawful raw rules with the all-path total cap and the same full joint law as W. Almost every normalized seed tree is the k-node stopping comb on a duplicate-free consecutive edge interval detached from the original target. It does not identify arbitrary exceptional seed versions pointwise.

Theorem 1.4 (Sharp bound and witness attainment for actual paid reads).

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

Source. Repository-derived.

Commentary.

The event remote(Q,j,2k+1) asks whether an actual original-rule read has distance at least 2k+1 from the unchanged endpoint j. The same witness attains the lower bound exactly. At k=1 every preserving competitor has remote-read probability one. Repeated and separator calls remain included in the cap.

Theorem 1.5 (Lawfulness, cap, all branch returns, full law and radius).

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

Source. Repository-derived.

Commentary.

For every arbitrary measurable probability seed space, permitted bias, endpoint j and k at least one, W is lawful, has total cap k on every source and seed, and every formal branch returns with a paid count between one and k. For every measurable seed set B and every observation z its full-law rectangle mass is nu(B) times stoppingMass(beta,k,z). Every actual read of W has distance at most 2k+1 from j.

Theorem 1.6 (Every raw preserving actual radius is at least 2k+1).

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

Source. Repository-derived.

Commentary.

WithinActualRadius quantifies every acquired actual read record, including null and nonreturn paths. A smaller radius makes the positive-mass remote event empty and contradicts the sharp probability bound. Together with the witness contract this proves an attained least natural radius, rather than merely a lower-bound predicate.

Theorem 1.7 (Ambient completed versions admit the same ordinary sections).

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

Source. Repository-derived.

Commentary.

For every arbitrary probability seed space U, bias beta, endpoint j, ambient-lawful CompletedRule Q, natural k with Q.TotalCap(k), and measurable source observation w whose seed joint law equals Q.fullLaw, there is a measurable selector T:U to trees of height at most k. Q.normalize equals T(seed) product-almost everywhere; for almost every seed the equality holds source-almost everywhere and every observation mass equals the source mass of w. No everywhere selector identity is asserted for ambient null changes.

Theorem 1.8 (Completed competitors have rigidity and the sharp read bound).

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

Source. Repository-derived.

Commentary.

For every arbitrary measurable probability seed space, permitted bias, endpoint j, k at least one, ambient-lawful completed Q with total cap k and the full law of W, there is one measurable bounded tree selector. Almost every seed has source-almost-everywhere agreement with the actual completed expansion and the exact detached k-node stopping-path geometry. The actual completed remote probability is at least (1+T(k))/2; W attains equality, and when k=1 the competitor probability is one.

For both raw and ambient completed competitors, the natural radii admitting a lawful total-cap-k representative with this same full law have least element 2k+1. The witness realizes membership on the same U and nu, and the actual remote event excludes each smaller radius. This is the minimum for the witness law at fixed k; it does not assert universal all-k radius nonemptiness for arbitrary inputs.

References