Countable Normal-Jet Criterion

Abstract

Continuous normal-jet positivity is detected at rational ordinates.

Theorem 1.1 (Continuous positivity is detected on the rationals).

$$\forall f\in \mathrm{Real}\left(\right)\to \mathrm{Real}\left(\right),\mathrm{Continuous}\left(f\right)\Rightarrow \left(\left(\forall t\in \mathrm{Real}\left(\right),0\le f\left(t\right)\right)\iff \left(\forall q\in \mathrm{Rat}\left(\right),0\le f\left(q\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Zeros/CountableNormalJetCriterion.continuous_nonnegative_iff_rat (✓ std3). ∎

Source. Repository-derived.

Commentary.

For a continuous real-valued function, nonnegativity at every real point is equivalent to nonnegativity at every rational point. The reverse implication extends the closed nonnegative condition from the dense range of the rational embedding.

Theorem 1.2 (Rational normal jets give a countable criterion and finite certificates).

$$\left(\left(RH\iff \left(\forall t\in \mathrm{Real}\left(\right),m\in \mathrm{Nat}\left(\right),0\le \mathrm{normalJet}\left(t,m\right)\right)\right)\wedge \left(\forall m\in \mathrm{Nat}\left(\right),\mathrm{Continuous}\left((t\mapsto \mathrm{normalJet}\left(t,m\right))\right)\right)\right)\Rightarrow \left(\left(RH\iff \left(\forall q\in \mathrm{Rat}\left(\right),m\in \mathrm{Nat}\left(\right),0\le \mathrm{normalJet}\left(q,m\right)\right)\right)\wedge \left(\left(\neg RH\right)\iff \left(\exists q\in \mathrm{Rat}\left(\right),m\in \mathrm{Nat}\left(\right),\sum _{j=0}^{2m}\frac{(-1{)}^{m+j}}{\mathrm{factorial}\left(j\right)\cdot \mathrm{factorial}\left(2m-j\right)}\cdot \mathrm{iteratedDeriv}\left(j,criticalXi,q\right)\cdot \mathrm{iteratedDeriv}\left(2m-j,criticalXi,q\right)<0\right)\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/Zeros/CountableNormalJetCriterion.countable_normal_jet_criterion (✓ std3). ∎

Source. Repository-derived.

Commentary.

Assume the analytic bridge identifying the Riemann hypothesis with nonnegativity of every real normal jet, and assume continuity in the ordinate at each depth. The dense rational criterion then gives the countable equivalence.

Negating that equivalence produces a rational ordinate q and a finite depth m with a negative jet. The imported normal-jet formula rewrites this witness as a finite signed factorial convolution of critical-xi derivatives from order zero through 2m.

The real-axis RH characterization is not available in D5 or pinned Mathlib and is deliberately exposed as a premise. The theorem proves the countable reduction and finite-certificate step; it does not claim to establish that missing analytic criterion.

References

• Truth anchor: D5/S3/Zeros/CountableNormalJetCriterion.continuous_nonnegative_iff_rat
• Truth anchor: D5/S3/Zeros/CountableNormalJetCriterion.countable_normal_jet_criterion
• Dependency: D5/S3/Zeros/NormalJetFormula