RarePriorReferenceScalar

Abstract

RarePriorReferenceScalar

The PH14 rational expressions e and f use the supplied exact constants. The PH17 polynomial isolates their unique nonnegative common root between 0.2333613 and 0.2333615. The scalar is e at that root. The statement proves the needed strict bound and makes no minimax or irrationality claim.

Theorem 1.1 (exact reference scalar).

$$\mathrm{lower}<\mathrm{aStar}\wedge \mathrm{aStar}<\mathrm{upper}\wedge \mathrm{rootPolynomial}\mathrm{aStar}=0\wedge (\forall a:\mathrm{Real},0\le a\Rightarrow \mathrm{rootPolynomial}a=0\Rightarrow a=\mathrm{aStar})\wedge e\mathrm{aStar}=f\mathrm{aStar}\wedge 0<\mathrm{tStar}\wedge \mathrm{tStar}<1/10000$$

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

Source. Repository-derived.

Commentary.

The statement retains the complete original telescope and conditions.

References

• Truth anchor: D5/S3/Observer/ProbabilisticClosure/TrajectoryLaws/RarePriorReferenceScalar.exact_reference_scalar