RarePriorThreePoint

Abstract

RarePriorThreePoint

The normalized prior has rational weights at native depths 1, 2 and 3, whose source rates are 1/3, 2/5 and 3/8. Every legal short history uses the same selected prior. The exact same-history endpoint posterior identifies the zero-rare posterior, yielding a perturbation bound for the complete unbounded original record target. Long native histories activate the fixed monitor and concentrate on depth 3. Law error is the complete-record TV of historyGenerated and fullTarget. Configuration error averages that TV under the actual retained row before the supremum. phaseLawRisk and phaseConfRisk take the original PhaseHistory domain; shortLawRisk and shortConfRisk restrict its paid Reads to H. Pure actual rows prove equality, and all these ENNReal risks are bounded by 1 before toReal. Short-cap risk differs from the zero-rare risk by at most 1/1000. The full first-alpha cylinder gives phase-p risk at least 21/40. RarePriorAbsoluteRisk.all_history_absolute_risks bounds both absolute native zero-rare law and configuration risks on all original phase histories by 253/500 in p and 2/5 in beta. Original radius identification, Phi, charged full-machine realization and the uniform cutoff refutation U remain open.

Theorem 1.1 (every short history).

$$\forall (H:\mathrm{Nat}),(0<(\mathrm{shortParameter}H).\mathrm{value}\wedge (\forall k:\mathrm{Depth},\mathrm{prior}(\mathrm{shortParameter}H)k=\mathrm{weight}(\mathrm{shortParameter}H)k)\wedge (\forall (\mathrm{ops}:\mathrm{List}\mathrm{Operation})(c:\mathrm{AcquiredNativeState})(\mathrm{hc}:\mathrm{run}\mathrm{ops}=\mathrm{some}c),(\mathrm{readLetters}\mathrm{ops}).\mathrm{length}\le H\Rightarrow ((\mathrm{posterior}(\mathrm{prior}(\mathrm{shortParameter}H))\mathrm{ops}c\mathrm{hc})\mathrm{depthThree}).\mathrm{toReal}<1/1000))$$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.2 (every short complete target).

$$\forall (H:\mathrm{Nat}),(\forall (\mathrm{ops}:\mathrm{List}\mathrm{Operation}),(\forall (c:\mathrm{AcquiredNativeState}),(\forall (\mathrm{hc}:\mathrm{run}\mathrm{ops}=\mathrm{some}c),(((\mathrm{readLetters}\mathrm{ops}).\mathrm{length}\le H)\Rightarrow ((\forall k:\mathrm{Depth},(\mathrm{posterior}(\mathrm{prior}(\mathrm{shortParameter}H))\mathrm{ops}c\mathrm{hc})k=\mathrm{ENNReal}.\mathrm{ofReal}(1-((\mathrm{posterior}(\mathrm{prior}(\mathrm{shortParameter}H))\mathrm{ops}c\mathrm{hc})\mathrm{depthThree}).\mathrm{toReal})\ast (\mathrm{posterior}\mathrm{muZero}\mathrm{ops}c\mathrm{hc})k+\mathrm{ENNReal}.\mathrm{ofReal}((\mathrm{posterior}(\mathrm{prior}(\mathrm{shortParameter}H))\mathrm{ops}c\mathrm{hc})\mathrm{depthThree}).\mathrm{toReal}\ast (\mathrm{PMF}.\mathrm{pure}\mathrm{depthThree})k)\wedge \mathrm{measurableTotalVariation}(\mathrm{NativeObserverJointLaw}.\mathrm{fullTarget}\mathrm{RarePriorFullFields}.\mathrm{actualObserver}(\mathrm{prior}(\mathrm{shortParameter}H))\mathrm{ops}c)(\mathrm{NativeObserverJointLaw}.\mathrm{fullTarget}\mathrm{RarePriorFullFields}.\mathrm{actualObserver}\mathrm{muZero}\mathrm{ops}c)<\mathrm{ENNReal}.\mathrm{ofReal}(1/1000)\wedge \exists z:\mathrm{Runtime},\mathrm{runtimeRun}\mathrm{ops}=\mathrm{some}z\wedge z.\mathrm{fields}=c.\mathrm{source}.\mathrm{finiteFields}\wedge \mathrm{NativeObserverJointLaw}.\mathrm{row}\mathrm{RarePriorFullFields}.\mathrm{actualObserver}\mathrm{ops}=\mathrm{PMF}.\mathrm{pure}z\wedge \mathrm{RarePriorGeneratedLaw}.\mathrm{historyGenerated}\mathrm{ops}=\mathrm{RarePriorGeneratedLaw}.\mathrm{decoder}z\wedge \forall (\mathrm{op}:\mathrm{Operation})(d:\mathrm{AcquiredNativeState}),\mathrm{nativeStep}c\mathrm{op}=\mathrm{some}d\Rightarrow \mathrm{NativeObserverJointLaw}.\mathrm{row}\mathrm{RarePriorFullFields}.\mathrm{actualObserver}(\mathrm{ops}++[\mathrm{op}])=\mathrm{RarePriorFullFields}.\mathrm{actualUpdate}\mathrm{op}z\wedge (\mathrm{ProbabilityTheory}.\mathrm{cond}(\mathrm{RarePriorGeneratedLaw}.\mathrm{historyGenerated}\mathrm{ops})\{t|\mathrm{RarePriorGeneratedLaw}.\mathrm{firstOperation}t=\mathrm{some}\mathrm{op}\}).\mathrm{map}\mathrm{NativeFullResidual}.\mathrm{deleteBlock}=\mathrm{RarePriorGeneratedLaw}.\mathrm{historyGenerated}(\mathrm{ops}++[\mathrm{op}]))))))$$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.3 (long history concentration).

$$\forall (t:\mathrm{Parameter}),((0<t.\mathrm{value})\Rightarrow ((\forall n:\mathrm{Nat},\mathrm{run}(\mathrm{longHistory}n)=\mathrm{some}(\mathrm{longState}n)\wedge 0<\mathrm{normalizer}(\mathrm{prior}t)(\mathrm{longHistory}n))\wedge (\forall n:\mathrm{Nat},375\le n\Rightarrow \mathrm{runtimeRun}(\mathrm{longHistory}n)=\mathrm{some}⟨\mathrm{latchedFields},.\mathrm{accepted},.g⟩)\wedge \mathrm{realMass}\mathrm{depthOne}\mathrm{blockWord}<\mathrm{realMass}\mathrm{depthThree}\mathrm{blockWord}\wedge \mathrm{realMass}\mathrm{depthTwo}\mathrm{blockWord}<\mathrm{realMass}\mathrm{depthThree}\mathrm{blockWord}\wedge \mathrm{Tendsto}(\mathrm{fun}n\mapsto ((\mathrm{posterior}(\mathrm{prior}t)(\mathrm{longHistory}n)(\mathrm{longState}n)({\mathrm{long}}_{\mathrm{run}}n))\mathrm{depthThree}).\mathrm{toReal})\mathrm{atTop}(\mathrm{nhds}1)))$$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.4 (long endpoint calibration).

$$\forall (n:\mathrm{Nat}),((375\le n)\Rightarrow (\mathrm{realMass}\mathrm{depthTwo}(\mathrm{blocks}n++\mathrm{latchWord})/\mathrm{realMass}\mathrm{depthOne}(\mathrm{blocks}n++\mathrm{latchWord})=(27/25:\mathrm{Real}{)}^3\ast (1594323/1562500:\mathrm{Real}{)}^{(2\ast n)}\wedge 16<\mathrm{realMass}\mathrm{depthTwo}(\mathrm{blocks}n++\mathrm{latchWord})/\mathrm{realMass}\mathrm{depthOne}(\mathrm{blocks}n++\mathrm{latchWord})\wedge 79/200<((\mathrm{posterior}\mathrm{muZero}(\mathrm{longHistory}n)(\mathrm{longState}n)({\mathrm{long}}_{\mathrm{run}}n))\mathrm{depthOne}).\mathrm{toReal}/3+((\mathrm{posterior}\mathrm{muZero}(\mathrm{longHistory}n)(\mathrm{longState}n)({\mathrm{long}}_{\mathrm{run}}n))\mathrm{depthTwo}).\mathrm{toReal}\ast (2/5)\wedge \mathrm{RarePriorReferenceScalar}.\mathrm{tStar}+47/100<21/40-(1116529/22781250:\mathrm{Real})\wedge (\forall (t:\mathrm{Parameter}),0<t.\mathrm{value}\Rightarrow \mathrm{Tendsto}(\mathrm{fun}m\mapsto ((\mathrm{posterior}(\mathrm{prior}t)(\mathrm{longHistory}m)(\mathrm{longState}m)({\mathrm{long}}_{\mathrm{run}}m))\mathrm{depthThree}).\mathrm{toReal})\mathrm{atTop}(\mathrm{nhds}1))))$$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

Theorem 1.5 (complete record risk bridges).

$$\forall (t:\mathrm{Parameter}),((0<t.\mathrm{value})\Rightarrow ((\forall (\mathrm{mu}:\mathrm{PMF}\mathrm{Depth})(h:\mathrm{List}\mathrm{Operation})(c:\mathrm{AcquiredNativeState}),\mathrm{run}h=\mathrm{some}c\Rightarrow \mathrm{confError}\mathrm{mu}hc=\mathrm{lawError}\mathrm{mu}hc\wedge \mathrm{lawError}\mathrm{mu}hc\le 1)\wedge (\forall (\mathrm{mu}:\mathrm{PMF}\mathrm{Depth})(s:\mathrm{ActivePhase}),\mathrm{phaseConfRisk}\mathrm{mu}s=\mathrm{phaseLawRisk}\mathrm{mu}s\wedge \mathrm{phaseLawRisk}\mathrm{mu}s\le 1\wedge \forall H:\mathrm{Nat},\mathrm{shortConfRisk}\mathrm{mu}sH=\mathrm{shortLawRisk}\mathrm{mu}sH\wedge \mathrm{shortLawRisk}\mathrm{mu}sH\le 1)\wedge (\forall (s:\mathrm{ActivePhase})(H:\mathrm{Nat}),(\mathrm{shortLawRisk}(\mathrm{prior}(\mathrm{shortParameter}H))sH).\mathrm{toReal}\le (\mathrm{shortLawRisk}\mathrm{muZero}sH).\mathrm{toReal}+1/1000)\wedge (\forall n:\mathrm{Nat},375\le n\Rightarrow \mathrm{RarePriorGeneratedLaw}.\mathrm{historyGenerated}(\mathrm{longHistory}n)\mathrm{firstAlpha}=\mathrm{ENNReal}.\mathrm{ofReal}(9/10)\wedge -1/10+(5/8)\ast ((\mathrm{posterior}(\mathrm{prior}t)(\mathrm{longHistory}n)(\mathrm{longState}n)({\mathrm{long}}_{\mathrm{run}}n))\mathrm{depthThree}).\mathrm{toReal}\le (\mathrm{lawError}(\mathrm{prior}t)(\mathrm{longHistory}n)(\mathrm{longState}n)).\mathrm{toReal})\wedge 21/40\le (\mathrm{phaseLawRisk}(\mathrm{prior}t).p).\mathrm{toReal}\wedge \mathrm{RarePriorReferenceScalar}.\mathrm{tStar}+47/100<(\mathrm{phaseLawRisk}(\mathrm{prior}t).p).\mathrm{toReal}-(1116529/22781250:\mathrm{Real})))$$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorThreePoint.complete_record_risk_bridges
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorThreePoint.every_short_complete_target
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorThreePoint.every_short_history
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorThreePoint.long_endpoint_calibration
• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorThreePoint.long_history_concentration
• Dependency: D5/S3/Estimation/DataProcessing/MeasurableTotalVariationTriangle
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorGeneratedLaw
• Dependency: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorReferenceScalar