uniform_tail_rate
plain-language theorem explainer
The uniform tail rate theorem asserts the existence of a real constant ρ strictly between 0 and 1 that serves as the uniform tail rate in the Pick spectral gap persistence formulation of the Riemann Hypothesis. Analysts studying the operator-theoretic approach to RH would reference this result when establishing bounds on the spectral gap. The proof proceeds by explicit term construction, supplying the witness 1/2 and verifying the inequalities via norm_num.
Claim. There exists a real number ρ such that 0 < ρ < 1.
background
The module formalizes the Riemann Hypothesis as a Pick spectral gap persistence problem in classical operator theory applied to the Riemann zeta function. Key results include pick_gap_pos_of_re_pos showing that positive real part of J implies positive Pick gap, euler_product_positive_real establishing J(σ) > 0 for real σ > 1, and pick_gap_persistence_implies_RH linking gap persistence to RH. The upstream result supplies the definition of a constant scalar field as a map sending every point to a fixed real value c.
proof idea
The proof is a term-mode construction that directly provides the pair consisting of the value 1/2 together with the two norm_num proofs of the strict inequalities 0 < 1/2 and 1/2 < 1.
why it matters
This result supplies the computable constant required for the reduction of the Riemann Hypothesis to Pick gap persistence, as noted in the module documentation. It supports the chain leading to pick_gap_persistence_implies_RH, which is fully proved. In the Recognition Science framework, it aligns with the forcing chain steps toward deriving physical constants from the functional equation, here instantiated in the number-theoretic setting for the zeta function.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.