Reusable certified-numerics infrastructure for one mode of the golden germ: rational beta, logarithm, exponential, phase, and trigonometric data are propagated to coordinate enclosures for a term and its derivative.
This module is the hand-written L2c infrastructure layer. It introduces no carrier definition. Its literal rational hypotheses certify the golden beta interval, a seventy-bit logarithm interval, an order-20 exponential envelope, exact pi phase reduction, order-10 sine and cosine envelopes, and the final interval arithmetic. The module is reusable certified-numerics infrastructure and makes no claim about RH.
Theorem 1.1 (The binary series encloses log 2 to seventy bits).
Proof. Machine-checked in Lean as D5/S3/Analytic/GermWindow/GermJetModeLemma.mode_term_enclosure (✓ std3). ∎
Source. Repository-derived.
Commentary.
For every mode v at most sixty, the displayed decidable rational hypotheses produce real and imaginary endpoint bounds for 2^{-c beta(v)}. Both returned interval widths are at most 10^{-15}. The live escape step multiplies the certified exponential enclosure by the phase-reduced cosine and sine enclosures and propagates the two error terms.
Theorem 1.3 (Rational mode data encloses the matching derivative term).
Proof. Machine-checked in Lean as D5/S3/Analytic/GermWindow/GermJetModeLemma.mode_deriv_enclosure (✓ std3). ∎
Source. Repository-derived.
Commentary.
The derivative certificate reuses the certified term coordinates and encloses the rational amplitude beta(v) log 2. Product-error propagation then bounds both coordinates of -beta(v) log(2) 2^{-c beta(v)}, again with widths at most 10^{-15}.