RarePriorFairBitService

Abstract

RarePriorFairBitService

The service holds a threshold tag, PC, Fin 7 position, Fin 128 candidate and one output bit. Reset clears the registers. Only a bit instruction reads fresh randomness. Seven sequential fair bits produce a binary candidate; comparison accepts 0 through 99 and tests the fixed thresholds 40, 90 and 1. Rejection clears both candidate and position and returns to reset without retaining a retry number.

The packet law is the product of seven fair Bernoulli bit measures. Independent packet streams retain all infinite paths. Rejection has probability 28/128=7/32, so finite rejection survival is (7/32) to the m. Actual first-return alpha cylinders are disjoint; summing their product masses gives 2/5, 9/10 and 1/100. The service trajectory either remains at reset after a rejected prefix or retains its first accepted result. Its eventual alpha output event equals the union of these first-return cylinders.

A paused bit instruction consumes precisely its remaining bits. Its first partial trial either returns or resets; every subsequent rejected trial is a fresh canonical packet. The actual never-return event is contained in the shifted infinite rejection event of measure zero. This argument covers every service microstate, including comparison, partial candidates, reset and already returned states. Individual transitions use only weights 0, 1/2 and 1.

Theorem 1.1 (seven bit candidate).

$$\forall (t:\mathrm{Threshold}),(\forall (p:\mathrm{Packet}),(\mathrm{collectPacket}tp=⟨t,.\mathrm{compare},6,\mathrm{packetEquiv}p,0⟩))$$

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

Source. Repository-derived.

Commentary.

Successive binary shifts assemble the seven fresh bits into the addressed Fin 128 candidate and enter comparison.

Theorem 1.2 (packet transaction).

$$\forall (t:\mathrm{Threshold}),(\forall (p:\mathrm{Packet}),(\mathrm{microStep}(\mathrm{collectPacket}tp)0=\mathrm{if}(\mathrm{packetEquiv}p).\mathrm{val}<100\mathrm{then}⟨t,.\mathrm{returned},6,\mathrm{packetEquiv}p,\mathrm{if}(\mathrm{packetEquiv}p).\mathrm{val}<(\mathrm{threshold}t).\mathrm{val}\mathrm{then}0\mathrm{else}1⟩\mathrm{else}\mathrm{entry}t))$$

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

Source. Repository-derived.

Commentary.

Comparison accepts candidates below 100, returns the threshold color, or clears the candidate and position and enters reset.

Theorem 1.3 (microstep weights).

$$\forall (sq:\mathrm{Service}),(\mathrm{microWeight}sq=0\vee \mathrm{microWeight}sq=1/2\vee \mathrm{microWeight}sq=1)$$

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

Source. Repository-derived.

Commentary.

A bit step is the sum of two half-weight deterministic images; every other instruction has a single unit-weight image.

Theorem 1.4 (fair packet mass).

$$\forall (p:\mathrm{Packet}),(\mathrm{wordMass}\mathrm{fairParameter}(\mathrm{packetBits}p)=1/128)$$

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

Source. Repository-derived.

Commentary.

The seven independent fair singleton masses multiply to one over 128 for every packet.

Theorem 1.5 (Packet singleton law).

$$\forall (p:\mathrm{Packet}),\mathrm{packetLaw}\{p\}=(1/128:{\mathbb{R}}_{\ge 0}^{\infty })$$

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

Source. Repository-derived.

Commentary.

The existing packet measure assigns one over 128 to each singleton. RarePriorSerialExecution uses this original supplier in its vector packet law and positive acceptance proof.

Theorem 1.6 (survival geometric).

$$\forall (m:\mathbb{N}),(\mathrm{survivalMass}m=(7/32{)}^m)$$

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

Source. Repository-derived.

Commentary.

Exactly 28 of the 128 packet addresses reject. Iterating the rejection recurrence multiplies survival by seven over 32.

Theorem 1.7 (exact service law).

$$\mathrm{returnedAlphaMass}.\mathrm{ordinary}=2/5\wedge \mathrm{returnedAlphaMass}.\mathrm{high}=9/10\wedge \mathrm{returnedAlphaMass}.\mathrm{low}=1/100\wedge \mathrm{Tendsto}\mathrm{survivalMass}\mathrm{atTop}(\mathrm{nhds}0)$$

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

Source. Repository-derived.

Commentary.

Summing the geometric first-return masses gives the three threshold fractions. The rejection survival tends to zero.

Theorem 1.8 (actual survival probability).

$$\forall (m:\mathbb{N}),(\mathrm{packetStreamLaw}(\mathrm{survives}m)=(7/32:{\mathbb{R}}_{\ge 0}^{\infty }{)}^m)$$

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

Source. Repository-derived.

Commentary.

Independent stream cylinders requiring m rejected packets have measure equal to the mth power of seven over 32.

Theorem 1.9 (almost sure service return).

$$\mathrm{packetStreamLaw}(\mathrm{iInter}m:\mathbb{N},\mathrm{survives}m)=0$$

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

Source. Repository-derived.

Commentary.

Continuity of measure for the decreasing rejection cylinders gives zero measure to infinite rejection.

Theorem 1.10 (actual service output law).

$$\forall (t:\mathrm{Threshold}),(\mathrm{packetStreamLaw}(\mathrm{iUnion}m:\mathbb{N},\mathrm{alphaReturnEvent}tm)=\mathrm{ENNReal}.\mathrm{ofReal}(\mathrm{returnedAlphaMass}t))$$

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

Source. Repository-derived.

Commentary.

Disjoint first-alpha-return cylinders have the computed product masses, whose countable sum is the returned alpha mass.

Theorem 1.11 (every microstate returns).

$$\forall (s:\mathrm{Service}),(\mathrm{packetStreamLaw}(\mathrm{neverReturns}s)=0)$$

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

Source. Repository-derived.

Commentary.

The first partial trial either returns or resets. Any subsequent nonreturning trajectory lies in a shifted infinite rejection event of measure zero.

Theorem 1.12 (rational service realization).

$$\forall (t:\mathrm{Threshold}),(\mathrm{packetStreamLaw}(\mathrm{iUnion}m:\mathbb{N},\mathrm{alphaReturnEvent}tm)=\mathrm{ENNReal}.\mathrm{ofReal}((\mathrm{threshold}t).\mathrm{val}/(100:\mathbb{R}))\wedge (\forall sq:\mathrm{Service},\mathrm{microWeight}sq=0\vee \mathrm{microWeight}sq=1/2\vee \mathrm{microWeight}sq=1)\wedge (\forall s:\mathrm{Service},\mathrm{packetStreamLaw}(\mathrm{neverReturns}s)=0))$$

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

Source. Repository-derived.

Commentary.

The measured first-return law, allowed microstep weights and almost-sure return hold together for the explicit service.

Theorem 1.13 (Rejected prefix resets).

$$\forall (t:\mathrm{Threshold}),\forall (\mathrm{omega}:\mathbb{N}\to \mathrm{Packet}),\forall (m:\mathbb{N}),(\forall j<m,100\le (\mathrm{packetEquiv}(\mathrm{omega}j)).\mathrm{val})\to \mathrm{trialRun}(\mathrm{entry}t)\mathrm{omega}m=\mathrm{entry}t$$

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

Source. Repository-derived.

Commentary.

Every finite rejected prefix leaves the actual trialRun at its prescribed reset entry. RarePriorSerialExecution uses this original supplier to identify the returned service after the first accepted packet.

Theorem 1.14 (operational service realization).

$$\forall (t:\mathrm{Threshold}),(\mathrm{alphaOutputEvent}t=\mathrm{iUnion}m:\mathbb{N},\mathrm{alphaReturnEvent}tm\wedge \mathrm{packetStreamLaw}(\mathrm{alphaOutputEvent}t)=\mathrm{ENNReal}.\mathrm{ofReal}((\mathrm{threshold}t).\mathrm{val}/(100:\mathbb{R}))\wedge (\forall sq:\mathrm{Service},\mathrm{microWeight}sq=0\vee \mathrm{microWeight}sq=1/2\vee \mathrm{microWeight}sq=1)\wedge (\forall s:\mathrm{Service},\mathrm{packetStreamLaw}(\mathrm{neverReturns}s)=0)\wedge \mathrm{packetStreamLaw}(\mathrm{iInter}m:\mathbb{N},\mathrm{survives}m)=0)$$

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

Source. Repository-derived.

Commentary.

The canonical trajectory retains the first accepted result. Its eventual alpha output event equals the cylinder union, transferring the exact probability calculation to operational output.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.actual_service_output_law
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.actual_survival_probability
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.almost_sure_service_return
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.every_microstate_returns
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.exact_service_law
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.fair_packet_mass
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.microstep_weights
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.operational_service_realization
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.packet_law_singleton
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.packet_transaction
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.prefix_reset
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.rational_service_realization
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.seven_bit_candidate
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFairBitService.survival_geometric
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorFiniteMonitor