Absolute risk on complete native tails

Abstract

RarePriorAbsoluteRisk

The runtime law is the pushforward of the marked trajectory through the original stopped-word decoder. Its only inputs are the retained finite runtime and the active phase. ValidTail preserves every legal completion word and infinite fourth return. The injective full renderer preserves the original records, event blocks and Stop; configuration averaging is performed before taking the supremum over the original PhaseHistory domain.

Every actual fourth query has one retained row. Watching cannot persist into that phase; ordinary remains ordinary after every subsequent letter. The two recognized classes give the complete G and Gbeta laws, with ordinary iid probability 2/5 after their specified returns. The ordinary p comparison shares alpha mass 1/3 and beta-beta mass 9/25 with every zero-rare posterior mixture; beta shares beta mass 3/5. These masses give errors at most 23/75 and 2/5.

A recognized G history has at least 375 blocks. Its posterior mean exceeds 79/200. The two-atom reference G0 has total variation 9/10 minus that mean, since alpha is its sole positive discrepancy; the complete G law is exactly 1/1000 away from G0. Gbeta has error at most 2/5. Pending retains the unique matching Stop and delivered retains the empty future, with zero error. PhaseHistory queries only active fourth cuts, while the separate terminal identities preserve both original terminal compatibilities.

All-history zero-rare risk is at most 253/500 in p and 2/5 in beta. The rare-prior perturbation adds at most 1/1000 to each capped supremum. These statements concern absolute native risks; identifying the original minimax radii requires the full-depth sharp-radius theorem. Operational realization and charged COMPLETE membership are separate obligations.

Theorem 1.1 (The complete valid-tail inclusion preserves total variation).

$$\forall s\in \mathrm{ActivePhase}\left(\right),\forall P\in \mathrm{Measure}\left(\mathrm{ValidTail}\left(s\right)\right),\forall Q\in \mathrm{Measure}\left(\mathrm{ValidTail}\left(s\right)\right),\mathrm{measurableTotalVariation}\left(\mathrm{mapSubtype}\left(P\right),\mathrm{mapSubtype}\left(Q\right)\right)=\mathrm{measurableTotalVariation}\left(P,Q\right)$$

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

Source. Repository-derived.

Commentary.

For either active phase s and arbitrary measures P,Q on ValidTail(s), mapSubtype denotes pushforward by Subtype.val into RawTail. The inclusion preserves measurable total variation exactly, including the noncompletion outcome. Probability normalization is not a premise.

Theorem 1.2 (Common submeasure controls total variation).

$$\forall X\in Type,\forall m\in \mathrm{MeasurableSpace}\left(X\right),\forall P\in \mathrm{Measure}\left(X\right),\forall Q\in \mathrm{Measure}\left(X\right),\forall C\in \mathrm{Measure}\left(X\right),(\mathrm{IsProbabilityMeasure}\left(P\right)\wedge \mathrm{IsProbabilityMeasure}\left(Q\right)\wedge \mathrm{IsFiniteMeasure}\left(C\right)\wedge C\le P\wedge C\le Q)\Rightarrow \mathrm{measurableTotalVariation}\left(P,Q\right)\le 1-\mathrm{mass}\left(C,univ\right)$$

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

Source. Repository-derived.

Commentary.

For every measurable space X, P and Q are probability measures and C is a finite measure below both. The supremum of the two directed measurable-event gaps is bounded by one minus the total common mass. Subtracting C from each probability measure leaves this same residual mass. The measurable-space parameter m determines the measure types and the measurable events in total variation; mass(C,univ) is C of the whole space. The statement holds at every type universe.

Theorem 1.3 (runtime law risk bridge).

$$(\forall (s:\mathrm{ActivePhase})(z:\mathrm{Runtime}),\mathrm{IsProbabilityMeasure}(\mathrm{lawfulTail}sz))\wedge (\forall {(}_{:}\mathrm{PMF}\mathrm{Depth})(s:\mathrm{ActivePhase})(H:\mathrm{NativeObserverJointLaw}.\mathrm{PhaseHistory}s)(z:\mathrm{Runtime}),z\in (\mathrm{NativeObserverJointLaw}.\mathrm{row}\mathrm{actualObserver}H.\mathrm{val}.1).\mathrm{support}\Rightarrow \mathrm{decoder}z=(\mathrm{lawfulTail}sz).\mathrm{map}(\mathrm{fullRenderer}H.\mathrm{val}.2s))\wedge (\forall (\mathrm{mu}:\mathrm{PMF}\mathrm{Depth})(s:\mathrm{ActivePhase}),\mathrm{NativeObserverJointLaw}.\mathrm{fullRisk}\mathrm{actualObserver}\mathrm{mu}s({\mathrm{fun}}_{\mapsto }\mathrm{lawfulTail}s)=\mathrm{phaseConfRisk}\mathrm{mu}s\wedge \mathrm{NativeObserverJointLaw}.\mathrm{rawRisk}\mathrm{actualObserver}\mathrm{mu}s({\mathrm{fun}}_{\mapsto }\mathrm{lawfulTail}s)=\mathrm{phaseLawRisk}\mathrm{mu}s)\wedge (\forall (s:\mathrm{ActivePhase})(H:\mathrm{NativeObserverJointLaw}.\mathrm{PhaseHistory}s),\exists z:\mathrm{Runtime},\mathrm{runtimeRun}H.\mathrm{val}.1=\mathrm{some}z\wedge z.\mathrm{fields}=H.\mathrm{val}.2.\mathrm{source}.\mathrm{finiteFields}\wedge \mathrm{NativeObserverJointLaw}.\mathrm{row}\mathrm{actualObserver}H.\mathrm{val}.1=\mathrm{PMF}.\mathrm{pure}z\wedge \mathrm{historyGenerated}H.\mathrm{val}.1=\mathrm{decoder}z\wedge z.\mathrm{mode}\ne .\mathrm{watching}\wedge ((z.\mathrm{mode}=.\mathrm{ordinary}\wedge \mathrm{rawLaw}sz=\mathrm{explicitStoppedWordLaw}s\mathrm{ordinaryRate})\vee (s=.p\wedge z.\mathrm{mode}=.g\wedge \mathrm{rawLaw}sz=\mathrm{specialPLaw})\vee (s=.\mathrm{beta}\wedge z.\mathrm{mode}=.\mathrm{gBeta}\wedge \mathrm{rawLaw}sz=\mathrm{specialBetaLaw})))\wedge (\forall (z:\mathrm{Runtime})(x:\mathrm{Letter}),z.\mathrm{mode}=.\mathrm{ordinary}\Rightarrow (\mathrm{readAdvance}zx).\mathrm{mode}=.\mathrm{ordinary})$$

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

Source. Repository-derived.

Commentary.

The displayed statement retains all histories, actual row support, phase parameters and terminal conditions.

Theorem 1.4 (all history absolute risks).

$$(\forall (s:\mathrm{ActivePhase})(H:\mathrm{NativeObserverJointLaw}.\mathrm{PhaseHistory}s),\mathrm{lawError}\mathrm{muZero}H.\mathrm{val}.1H.\mathrm{val}.2\le \mathrm{ENNReal}.\mathrm{ofReal}(\mathrm{absoluteBound}s)\wedge \mathrm{confError}\mathrm{muZero}H.\mathrm{val}.1H.\mathrm{val}.2\le \mathrm{ENNReal}.\mathrm{ofReal}(\mathrm{absoluteBound}s))\wedge (\forall s:\mathrm{ActivePhase},(\mathrm{phaseLawRisk}\mathrm{muZero}s).\mathrm{toReal}\le \mathrm{absoluteBound}s\wedge (\mathrm{phaseConfRisk}\mathrm{muZero}s).\mathrm{toReal}\le \mathrm{absoluteBound}s)\wedge (\forall (s:\mathrm{ActivePhase})(H:\mathrm{Nat}),(\mathrm{shortLawRisk}(\mathrm{prior}(\mathrm{shortParameter}H))sH).\mathrm{toReal}\le \mathrm{absoluteBound}s+1/1000\wedge (\mathrm{shortConfRisk}(\mathrm{prior}(\mathrm{shortParameter}H))sH).\mathrm{toReal}\le \mathrm{absoluteBound}s+1/1000)\wedge (\forall (\mathrm{mu}:\mathrm{PMF}\mathrm{Depth})(s:\mathrm{ActivePhase})(HK:\mathrm{Nat}),H\le K\Rightarrow \mathrm{shortLawRisk}\mathrm{mu}sH\le \mathrm{shortLawRisk}\mathrm{mu}sK\wedge \mathrm{shortConfRisk}\mathrm{mu}sH\le \mathrm{shortConfRisk}\mathrm{mu}sK)\wedge (\forall (\mathrm{mu}:\mathrm{PMF}\mathrm{Depth})(h:\mathrm{List}\mathrm{Operation})(c:\mathrm{AcquiredNativeState}),\mathrm{run}h=\mathrm{some}c\Rightarrow ((\exists b,c.\mathrm{source}.\mathrm{finiteFields}.\mathrm{control}=.\mathrm{fourth}(.\mathrm{pending}b))\vee c.\mathrm{source}.\mathrm{finiteFields}.\mathrm{control}=.\mathrm{fourth}.\mathrm{delivered})\Rightarrow \mathrm{lawError}\mathrm{mu}hc=0\wedge \mathrm{confError}\mathrm{mu}hc=0)$$

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

Source. Repository-derived.

Commentary.

The displayed statement retains all histories, actual row support, phase parameters and terminal conditions.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorAbsoluteRisk.all_history_absolute_risks
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorAbsoluteRisk.common_measure_tv
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorAbsoluteRisk.runtime_law_risk_bridge
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorAbsoluteRisk.subtype_tv
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/ConstantSuspensionSeparator
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorThreePoint