Repeated acceptance on one fresh stream

Abstract

FreshServiceRestart

An iid external stream supplies candidates one at a time. The first accepted coordinate and the suffix strictly after it are semantic execution coordinates. Neither the search index nor the suffix is a retained machine register or a readable random tape. The fallback totalizes the zero-mass event of never accepting.

A first-hit event fixes a rejected prefix and one accepted candidate. Independence of disjoint coordinate sets factors its joint mass with any measurable suffix event. The rejected-prefix masses form a geometric series. Positive acceptance mass makes infinite rejection null, and summing the disjoint first-hit events gives the conditional accepted law times the unchanged iid suffix law.

Repeated services always consume the unused suffix of that same stream. Their prefix probabilities follow by induction from the joint restart identity. Equality of every finite prefix, followed by projective-limit uniqueness, identifies the complete infinite output measure. Countable intersection of the full-measure return events covers every repeated service.

RarePriorSerialExecution.repeated_fresh_bit_service applies this result to consecutive packets of seven external fair bits and relates the accepted candidates to the existing reset/bit/compare trajectory. This probability theorem does not implement a scanner or renderer, charge a complete machine snapshot, establish original COMPLETE membership or optimize an original inf-sup risk.

Theorem 1.1 (First hit characterization).

$$\forall (A:\mathrm{Type}),\forall (\mathrm{inst}:\mathrm{MeasurableSpace}(A)),\forall (\mathrm{accept}:\mathrm{Set}(A)),\forall (\mathrm{omega}:\mathbb{N}\to A),\forall (n:\mathbb{N}),\mathrm{firstHit}(\mathrm{accept},\mathrm{omega})=\mathrm{some}(n)⟺\mathrm{omega}(n)\in \mathrm{accept}\wedge \forall i<n,\neg (\mathrm{omega}(i)\in \mathrm{accept})$$

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

Source. Repository-derived.

Commentary.

The selected index has an accepted candidate and every strictly earlier coordinate rejects.

Theorem 1.2 (Accepted value and untouched suffix).

$$\forall (A:\mathrm{Type}),\forall (\mathrm{inst}:\mathrm{MeasurableSpace}(A)),\forall (\mathrm{mu}:\mathrm{Measure}(A)),\forall (\mathrm{hprob}:\mathrm{IsProbabilityMeasure}(\mathrm{mu})),\forall (\mathrm{accept}:\mathrm{Set}(A)),\forall (\mathrm{fallback}:A),\mathrm{MeasurableSet}(\mathrm{accept})\to \mathrm{mu}(\mathrm{accept})\ne 0\to \mathrm{Measure}.\mathrm{map}(\mathrm{restart}(\mathrm{accept},\mathrm{fallback}),\mathrm{Measure}.\mathrm{infinitePi}(\mathrm{fun}i:\mathbb{N}\mapsto \mathrm{mu}))=\mathrm{Measure}.\mathrm{prod}(\mathrm{ProbabilityTheory}.\mathrm{cond}(\mathrm{mu},\mathrm{accept}),\mathrm{Measure}.\mathrm{infinitePi}(\mathrm{fun}i:\mathbb{N}\mapsto \mathrm{mu}))$$

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

Source. Repository-derived.

Commentary.

First acceptance yields the conditional accepted value independently of the entire unused iid suffix.

Theorem 1.3 (Whole repeated output law).

$$\forall (A:\mathrm{Type}),\forall (\mathrm{inst}:\mathrm{MeasurableSpace}(A)),\forall (\mathrm{finite}:\mathrm{Fintype}(A)),\forall (\mathrm{singletons}:\mathrm{MeasurableSingletonClass}(A)),\forall (\mathrm{mu}:\mathrm{Measure}(A)),\forall (\mathrm{hprob}:\mathrm{IsProbabilityMeasure}(\mathrm{mu})),\forall (\mathrm{accept}:\mathrm{Set}(A)),\forall (\mathrm{fallback}:A),\mathrm{MeasurableSet}(\mathrm{accept})\to \mathrm{mu}(\mathrm{accept})\ne 0\to \mathrm{Measurable}(\mathrm{draws}(\mathrm{accept},\mathrm{fallback}))\wedge \mathrm{Measure}.\mathrm{map}(\mathrm{draws}(\mathrm{accept},\mathrm{fallback}),\mathrm{Measure}.\mathrm{infinitePi}(\mathrm{fun}i:\mathbb{N}\mapsto \mathrm{mu}))=\mathrm{Measure}.\mathrm{infinitePi}(\mathrm{fun}i:\mathbb{N}\mapsto \mathrm{ProbabilityTheory}.\mathrm{cond}(\mathrm{mu},\mathrm{accept}))\wedge (\mathrm{ae}\mathrm{omega}\mathrm{under}\mathrm{Measure}.\mathrm{infinitePi}(\mathrm{fun}i:\mathbb{N}\mapsto \mathrm{mu}),\forall (n:\mathbb{N}),\mathrm{firstHit}(\mathrm{accept},\mathrm{unused}(\mathrm{accept},\mathrm{fallback},n,\mathrm{omega}))\ne \mathrm{none})$$

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

Source. Repository-derived.

Commentary.

The complete repeated accepted sequence has the iid conditional-acceptance law, and every repeated service returns outside one null event.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/FreshServiceRestart.first_acceptance_restart
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/FreshServiceRestart.first_hit_some
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/FreshServiceRestart.repeated_acceptance_law