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).
log ( 2 ) − 116896104058966015646750947554978314987992252416 81026204946914272618346609082102250801114907729 ≤ 2 70 1
Proof. Machine-checked in Lean as D5/S3/Analytic/GermWindow/GermJetModeLemma.log_two_binary_70✓ std3). ∎
Source. Repository-derived.
Commentary.
Mathlib’s logarithm-series remainder bound is normalized to the displayed rational center and an error of 2^{-70}.
Theorem 1.2 (Rational mode data encloses one complex germ term).
∀ v ∈ N , sc a l e ∈ N , s w a p ∈ B oo l , b e t a L o ∈ Q , b e t a H i ∈ Q , xL o ∈ Q , x H i ∈ Q , t h e t a L o ∈ Q , t h e t a H i ∈ Q , p ha se L o ∈ Q , p ha seH i ∈ Q , r 0 ∈ Q , rDe lt a ∈ Q , p i E rr ∈ Q , q L o ∈ Q , q H i ∈ Q , ba se L o ∈ Q , ba seH i ∈ Q , e x p L o ∈ Q , e x p H i ∈ Q , e x p 0 ∈ Q , e x pE rr ∈ Q , cos 0 ∈ Q , s in 0 ∈ Q , cos B a se E rr ∈ Q , s in B a se E rr ∈ Q , cos E rr ∈ Q , s in E rr ∈ Q , t h e t a C os 0 ∈ Q , t h e t a S in 0 ∈ Q , t h e t a C os E rr ∈ Q , t h e t a S in E rr ∈ Q , t er m R e L o ∈ Q , t er m R eH i ∈ Q , t er m I m L o ∈ Q , t er m I m H i ∈ Q , v ≤ 60 ∧ b e t a L o ≤ o5FloorTable ( v ) − 1 − v + v ⋅ 5000000000000000000 8090169943749474241 ∧ o5FloorTable ( v ) − 1 − v + v ⋅ 100000000000000000000 161803398874989484821 ≤ b e t a H i ∧ 0 ≤ b e t a L o ∧ xL o ≤ ℜ c ⋅ b e t a L o ⋅ 116896104058966015646750947554978314987992252416 81026204946914272618247594230558639436210831195 ∧ ℜ c ⋅ b e t a H i ⋅ 116896104058966015646750947554978314987992252416 81026204946914272618445623933645862166018984263 ≤ x H i ∧ t h e t a L o ≤ Im ( c ) ⋅ b e t a L o ⋅ 116896104058966015646750947554978314987992252416 81026204946914272618247594230558639436210831195 ∧ Im ( c ) ⋅ b e t a H i ⋅ 116896104058966015646750947554978314987992252416 81026204946914272618445623933645862166018984263 ≤ t h e t a H i ∧ p ha se L o ≤ if s w a p then t h e t a L o − 2 p i A pp ro x − 2 ⋅ 10 19 1 else t h e t a L o ∧ if s w a p then t h e t a H i − 2 p i A pp ro x + 2 ⋅ 10 19 1 else t h e t a H i ≤ p ha seH i ∧ 0 < sc a l e ∧ q L o ≤ sc a l e − x H i ∧ sc a l e − xL o ≤ q H i ∧ ∣ q L o ∣ ≤ 1 ∧ ∣ q H i ∣ ≤ 1 ∧ ba se L o ≤ i ∈ range ( 20 ) ∑ factorial ( i ) q L o i − factorial ( 20 ) ⋅ 20 ∣ q L o ∣ 20 ⋅ 21 ∧ i ∈ range ( 20 ) ∑ factorial ( i ) q H i i + factorial ( 20 ) ⋅ 20 ∣ q H i ∣ 20 ⋅ 21 ≤ ba seH i ∧ 0 ≤ ba se L o ∧ e x p L o ≤ ba se L o sc a l e ∧ ba seH i sc a l e ≤ e x p H i ∧ e x p 0 − e x pE rr ≤ e x p L o ∧ e x p H i ≤ e x p 0 + e x pE rr ∧ ∣ p ha se L o ∣ ≤ 10 7 ∧ ∣ p ha se L o − phaseIndexPi ( p ha se L o ) ⋅ p i A pp ro x ∣ + p ha seH i − p ha se L o ≤ 100 99 ∧ ∣ phaseIndexPi ( p ha se L o ) ∣ ⋅ 10 19 1 ≤ p i E rr ∧ r 0 = 2 p ha se L o + p ha seH i − phaseIndexPi ( p ha se L o ) ⋅ p i A pp ro x ∧ 2 p ha seH i − p ha se L o + p i E rr ≤ rDe lt a ∧ ∣ r 0 ∣ ≤ 1 ∧ factorial ( 20 ) ∣ r 0 ∣ 20 + i ∈ range ( 10 ) ∑ factorial ( 2 ⋅ i ) ( − 1 ) i ⋅ r 0 2 ⋅ i − cos 0 ≤ cos B a se E rr ∧ factorial ( 21 ) ∣ r 0 ∣ 21 + i ∈ range ( 10 ) ∑ factorial ( 2 ⋅ i + 1 ) ( − 1 ) i ⋅ r 0 2 ⋅ i + 1 − s in 0 ≤ s in B a se E rr ∧ ( rDe lt a + cos B a se E rr ≤ cos E rr ∧ ( rDe lt a + s in B a se E rr ≤ s in E rr ∧ ( if s w a p then ( − ( − 1 ) phaseIndexPi ( p ha se L o ) ) ⋅ s in 0 else ( − 1 ) phaseIndexPi ( p ha se L o ) ⋅ cos 0 = t h e t a C os 0 ∧ ( if s w a p then ( − 1 ) phaseIndexPi ( p ha se L o ) ⋅ cos 0 else ( − 1 ) phaseIndexPi ( p ha se L o ) ⋅ s in 0 = t h e t a S in 0 ∧ ( if s w a p then s in E rr else cos E rr ≤ t h e t a C os E rr ∧ ( if s w a p then cos E rr else s in E rr ≤ t h e t a S in E rr ∧ ( t er m R e L o ≤ e x p 0 ⋅ t h e t a C os 0 − ( e x pE rr + ∣ e x p 0 ∣ ⋅ t h e t a C os E rr ) ∧ ( e x p 0 ⋅ t h e t a C os 0 + e x pE rr + ∣ e x p 0 ∣ ⋅ t h e t a C os E rr ≤ t er m R eH i ∧ ( t er m I m L o ≤ − ( e x p 0 ⋅ t h e t a S in 0 ) − ( e x pE rr + ∣ e x p 0 ∣ ⋅ t h e t a S in E rr ) ∧ ( − ( e x p 0 ⋅ t h e t a S in 0 ) + e x pE rr + ∣ e x p 0 ∣ ⋅ t h e t a S in E rr ≤ t er m I m H i ∧ ( t er m R eH i − t er m R e L o ≤ 10 15 1 ∧ t er m I m H i − t er m I m L o ≤ 10 15 1 ) ) ) ) ) ) ) ) ) ) ) ⇒ ( ( ( t er m R e L o ≤ ℜ 2 ( − c ⋅ beta ( v ) ) ∧ ℜ 2 ( − c ⋅ beta ( v ) ) ≤ t er m R eH i ) ∧ ( t er m I m L o ≤ Im ( 2 ( − c ⋅ beta ( v ) ) ) ∧ Im ( 2 ( − c ⋅ beta ( v ) ) ) ≤ t er m I m H i ) ) ∧ ( t er m R eH i − t er m R e L o ≤ 10 15 1 ∧ t er m I m H i − t er m I m L o ≤ 10 15 1 ) )
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).
∀ v ∈ N , b e t a L o ∈ Q , b e t a H i ∈ Q , e x p 0 ∈ Q , t h e t a C os 0 ∈ Q , t h e t a S in 0 ∈ Q , t er m R e E rr ∈ Q , t er m I m E rr ∈ Q , t er m R e L o ∈ Q , t er m R eH i ∈ Q , t er m I m L o ∈ Q , t er m I m H i ∈ Q , am p 0 ∈ Q , am pE rr ∈ Q , d er i v R e L o ∈ Q , d er i v R eH i ∈ Q , d er i v I m L o ∈ Q , d er i v I m H i ∈ Q , ( v ≤ 60 ∧ ( b e t a L o ≤ o5FloorTable ( v ) − 1 − v + v ⋅ 5000000000000000000 8090169943749474241 ∧ ( o5FloorTable ( v ) − 1 − v + v ⋅ 100000000000000000000 161803398874989484821 ≤ b e t a H i ∧ ( 0 ≤ b e t a L o ∧ ( ( ( ( t er m R e L o ≤ ℜ 2 ( − c ⋅ beta ( v ) ) ∧ ℜ 2 ( − c ⋅ beta ( v ) ) ≤ t er m R eH i ) ∧ ( t er m I m L o ≤ Im ( 2 ( − c ⋅ beta ( v ) ) ) ∧ Im ( 2 ( − c ⋅ beta ( v ) ) ) ≤ t er m I m H i ) ) ∧ ( t er m R eH i − t er m R e L o ≤ 10 15 1 ∧ t er m I m H i − t er m I m L o ≤ 10 15 1 ) ) ∧ ( am p 0 − am pE rr ≤ 116896104058966015646750947554978314987992252416 81026204946914272618247594230558639436210831195 ⋅ b e t a L o ∧ ( 116896104058966015646750947554978314987992252416 81026204946914272618445623933645862166018984263 ⋅ b e t a H i ≤ am p 0 + am pE rr ∧ ( e x p 0 ⋅ t h e t a C os 0 − t er m R e E rr ≤ t er m R e L o ∧ ( t er m R eH i ≤ e x p 0 ⋅ t h e t a C os 0 + t er m R e E rr ∧ ( − ( e x p 0 ⋅ t h e t a S in 0 ) − t er m I m E rr ≤ t er m I m L o ∧ ( t er m I m H i ≤ − ( e x p 0 ⋅ t h e t a S in 0 ) + t er m I m E rr ∧ ( d er i v R e L o ≤ − ( am p 0 ⋅ e x p 0 ⋅ t h e t a C os 0 ) − ( am pE rr + ∣ am p 0 ∣ ⋅ t er m R e E rr ) ∧ ( − ( am p 0 ⋅ e x p 0 ⋅ t h e t a C os 0 ) + am pE rr + ∣ am p 0 ∣ ⋅ t er m R e E rr ≤ d er i v R eH i ∧ ( d er i v I m L o ≤ − ( am p 0 ⋅ ( − ( e x p 0 ⋅ t h e t a S in 0 ) ) ) − ( am pE rr + ∣ am p 0 ∣ ⋅ t er m I m E rr ) ∧ ( − ( am p 0 ⋅ ( − ( e x p 0 ⋅ t h e t a S in 0 ) ) ) + am pE rr + ∣ am p 0 ∣ ⋅ t er m I m E rr ≤ d er i v I m H i ∧ ( d er i v R eH i − d er i v R e L o ≤ 10 15 1 ∧ d er i v I m H i − d er i v I m L o ≤ 10 15 1 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ⇒ ( ( ( d er i v R e L o ≤ ℜ ( − beta ( v ) ) ⋅ log ( 2 ) ⋅ 2 ( − c ⋅ beta ( v ) ) ∧ ℜ ( − beta ( v ) ) ⋅ log ( 2 ) ⋅ 2 ( − c ⋅ beta ( v ) ) ≤ d er i v R eH i ) ∧ ( d er i v I m L o ≤ Im ( ( − beta ( v ) ) ⋅ log ( 2 ) ⋅ 2 ( − c ⋅ beta ( v ) ) ) ∧ Im ( ( − beta ( v ) ) ⋅ log ( 2 ) ⋅ 2 ( − c ⋅ beta ( v ) ) ) ≤ d er i v I m H i ) ) ∧ ( d er i v R eH i − d er i v R e L o ≤ 10 15 1 ∧ d er i v I m H i − d er i v I m L o ≤ 10 15 1 ) )
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}.