Rational Basis for the Robin Certificate

Abstract

Sharp rational logarithm bounds and an exact rational checker certify the additive Robin gap at 10080 without floating-point assumptions.

Definition 1.1 (Truncated atanh expansion).

$\forall t \in R, K \in N, a t anh P a r t ia l (t, K) = 2 \cdot j \in r an g e (K) \sum (\frac{( t ) ^{2 \cdot j + 1}}{( c a s tR e a l ( 2 \cdot j + 1 ) )})$

Formalization. D5/S3/Arith/GoldenResource/RobinRationalBasis.atanhPartial (✓ std3).

Source. Repository-derived.

Commentary.

For real t and natural K, atanhPartial is twice the sum over natural j with 0 <= j < K of t^(2j+1)/(2j+1). The denominator is coerced to the reals. This is the defining expression in the ZECKENDORF_EULER_5040 appendix.

Definition 1.2 (Atanh reduction parameter).

$\forall y \in R, a t anh P a r am e t er (y) = \frac{y - 1}{( y + 1 )}$

Formalization. D5/S3/Arith/GoldenResource/RobinRationalBasis.atanhParameter (✓ std3).

Source. Repository-derived.

Commentary.

For real y, atanhParameter is exactly (y-1)/(y+1), as stated in the ZECKENDORF_EULER_5040 appendix.

Theorem 1.3 (Atanh parameter interval).

$\forall y \in R, (1 \leq y \land y < 2) \Rightarrow (0 \leq a t anh P a r am e t er (y) \land a t anh P a r am e t er (y) < \frac{1}{3})$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.atanhParameter_lt_third (✓ std3). ∎

Source. Repository-derived.

Commentary.

For 1 <= y < 2, the appendix parameter is nonnegative and strictly less than 1/3. This elementary estimate is stated as in the ZECKENDORF_EULER_5040 appendix.

Definition 1.4 (Named logarithm remainder).

$\forall y \in R, K \in N, l o g R e main d er (y, K) = l o g (y) - a t anh P a r t ia l (a t anh P a r am e t er (y), K)$

Formalization. D5/S3/Arith/GoldenResource/RobinRationalBasis.logRemainder (✓ std3).

Source. Repository-derived.

Commentary.

For real y and natural K, logRemainder is exactly log y minus the truncated atanh series evaluated at atanhParameter y.

Theorem 1.5 (Sharp logarithm expansion remainder).

$\forall y \in R, K \in N, (1 \leq y \land y < 2) \Rightarrow (0 \leq l o g R e main d er (y, K) \land l o g R e main d er (y, K) \leq \frac{2 \cdot (( a t anh P a r am e t er ( y ) ) ) ^{2 \cdot K + 1}}{( c a s tR e a l ( 2 \cdot K + 1 ) \cdot ( 1 - (( a t anh P a r am e t er ( y ) ) ) ^{2} ) )})$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.log_expansion_remainder_bound (✓ std3). ∎

Source. Repository-derived.

Commentary.

For 1 <= y < 2, substitute t=(y-1)/(y+1). The logarithm exceeds the finite sum by a nonnegative remainder bounded by 2t^(2K+1)/((2K+1)(1-t^2)). The sharp factor 1/(2K+1) is proved by an integral majorant. This is the first boxed statement of the ZECKENDORF_EULER_5040 appendix and an elementary atanh-series remainder estimate stated there.

Theorem 1.6 (Termwise logarithmic estimate).

$\forall x \in R, 0 < x \Rightarrow (\frac{1}{( 2 \cdot (( x + 1 ) ) ^{2} )} < l o g (\frac{x + 1}{( x )}) - \frac{1}{( x + 1 )} \land l o g (\frac{x + 1}{( x )}) - \frac{1}{( x + 1 )} < \frac{1}{( 2 \cdot x \cdot ( x + 1 ) )})$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.log_harmonic_term_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

For positive real x, the displayed strict two-sided estimate bounds log((x+1)/x)-1/(x+1). It is the elementary appendix estimate used to prove A.1, stated as in ZECKENDORF_EULER_5040.

Theorem 1.7 (Euler–Mascheroni tail identity).

$\forall N \in N, 1 \leq N \Rightarrow c a s tR e a l (ha r m o ni c (N)) - l o g (c a s tR e a l (N)) - e u l er M a sc h ero ni C o n s t an t () = k \in N \sum (l o g ((1 + \frac{1}{( c a s tR e a l ( k + N ) )})) - \frac{1}{( c a s tR e a l ( k + N + 1 ) )})$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.eulerMascheroni_tail_identity (✓ std3). ∎

Source. Repository-derived.

Commentary.

附录展示的尾和恒等式

Theorem 1.8 (Euler–Mascheroni remainder bracket A.1).

$\forall N \in N, 1 \leq N \Rightarrow (\frac{1}{( 2 \cdot c a s tR e a l ( N + 1 ) )} < c a s tR e a l (ha r m o ni c (N)) - l o g (c a s tR e a l (N)) - e u l er M a sc h ero ni C o n s t an t () \land c a s tR e a l (ha r m o ni c (N)) - l o g (c a s tR e a l (N)) - e u l er M a sc h ero ni C o n s t an t () < \frac{1}{( 2 \cdot c a s tR e a l ( N ) )})$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.eulerMascheroni_remainder_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

For every natural N >= 1, this is exactly equation (A.1) of the ZECKENDORF_EULER_5040 appendix. The proof squeezes strictly monotone and antitone corrected harmonic sequences to the Euler–Mascheroni constant; this elementary harmonic-asymptotic estimate is stated as in that appendix.

Theorem 1.9 (Pinned decimal bounds for log 2).

$\frac{6931471803}{10000000000} < l o g (2) \land l o g (2) < \frac{6931471808}{10000000000}$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.log_two_decimal_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

This companion records the two certified Mathlib decimal inequalities for log 2. Its consumer is eulerMascheroni_decimal_bounds through the logarithm-of-1000 calculation.

Theorem 1.10 (Decimal Euler–Mascheroni bracket).

$\frac{5772155}{10000000} < e u l er M a sc h ero ni C o n s t an t () \land e u l er M a sc h ero ni C o n s t an t () < \frac{5772161}{10000000}$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.eulerMascheroni_decimal_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

The N=1000 specialization of A.1, together with the sharp logarithm expansion, proves 0.5772155 < gamma_EM < 0.5772161 in the Lean kernel.

Definition 1.11 (Rational interval data).

$R a t i o na lB r a c k e t = s t r u c t u re (l o w er (Q), u pp er (Q))$

Formalization. D5/S3/Arith/GoldenResource/RobinRationalBasis.RationalBracket (✓ std3).

Source. Repository-derived.

Commentary.

RationalBracket is a structure with rational fields lower and upper. It is data; endpoint order and semantic containment are checked separately.

Definition 1.12 (Semantic bracket containment).

$\forall b \in R a t i o na lB r a c k e t, x \in R, C o n t ain s (b, x) \Leftrightarrow (c a s tR e a l (l o w er (b)) \leq x \land x \leq c a s tR e a l (u pp er (b)))$

Formalization. D5/S3/Arith/GoldenResource/RobinRationalBasis.Contains (✓ std3).

Source. Repository-derived.

Commentary.

Contains b x means that the rational endpoints b.lower and b.upper, each coerced to the reals, enclose x with non-strict inequalities.

Definition 1.13 (Truncated rational exponential).

$\forall q \in Q, t er m s \in N, e x pP a r t ia l (q, t er m s) = p a r t ia lS u m (e x pS er i es (Q, Q), t er m s, q)$

Formalization. D5/S3/Arith/GoldenResource/RobinRationalBasis.expPartial (✓ std3).

Source. Repository-derived.

Commentary.

For rational q and natural term count, expPartial is Mathlib’s exponential formal-series partial sum evaluated at q.

Theorem 1.14 (Finite-sum form of the exponential partial sum).

$\forall q \in Q, t er m s \in N, e x pP a r t ia l (q, t er m s) = i \in r an g e (t er m s) \sum (\frac{( q ) ^{i}}{( c a s tR a t ( f a c t or ia l ( i ) ) )})$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.expPartial_eq_sum (✓ std3). ∎

Source. Repository-derived.

Commentary.

The Mathlib formal-series wrapper equals the rational indexed sum over natural i in range terms of q^i/i!.

Definition 1.15 (Additive Robin gap).

$\forall n \in N, ro bin De lt a (n) = e x p (e u l er M a sc h ero ni C o n s t an t ()) \cdot c a s tR e a l (n) \cdot l o g (l o g (c a s tR e a l (n))) - c a s tR e a l (s i g ma (1, n))$

Formalization. D5/S3/Arith/GoldenResource/RobinRationalBasis.robinDelta (✓ std3).

Source. Repository-derived.

Commentary.

The additive Robin gap exp(gamma_EM) times n times log(log n), minus sigma_1(n), is an auxiliary quantity of this module. The volume’s chapter-9 margin Delta(n) = gamma_EM + log(log(log n)) - log(sigma_1(n)/n) is a different (logarithmic) quantity, formalized in the companion module GoldenCell5040Certificate. Only the signs of the two agree, and no identity between them is claimed here. Its exact rational basis follows 「ZECKENDORF_EULER_5040 附录」.

Definition 1.16 (Rational positivity predicate).

$\forall n \in N, t er m s \in N, g amma \in R a t i o na lB r a c k e t, l o gL o g \in R a t i o na lB r a c k e t, R o bin P os i t i v e J u d g e (n, t er m s, g amma, l o gL o g) \Leftrightarrow (l o w er (g amma) \leq u pp er (g amma) \land (l o w er (l o gL o g) \leq u pp er (l o gL o g) \land (0 \leq l o w er (g amma) \land (0 \leq l o w er (l o gL o g) \land c a s tR a t (s i g ma (1, n)) < e x pP a r t ia l (l o w er (g amma), t er m s) \cdot c a s tR a t (n) \cdot l o w er (l o gL o g)))))$

Formalization. D5/S3/Arith/GoldenResource/RobinRationalBasis.RobinPositiveJudge (✓ std3).

Source. Repository-derived.

Commentary.

This module’s own auxiliary judge for the additive Robin gap checks ordered gamma and log-log brackets, nonnegative lower endpoints, and one strict rational inequality. sigma_1(n) and n are coerced to rationals. Its exact rational basis follows 「ZECKENDORF_EULER_5040 附录」; no floating-point value enters this predicate.

Definition 1.17 (Decidability of the rational judge).

$\forall n \in N, t er m s \in N, g amma \in R a t i o na lB r a c k e t, l o gL o g \in R a t i o na lB r a c k e t, Dec i d ab l e (R o bin P os i t i v e J u d g e (n, t er m s, g amma, l o gL o g))$

Formalization. D5/S3/Arith/GoldenResource/RobinRationalBasis.robinPositiveJudgeDecidable (✓ std3).

Source. Repository-derived.

Commentary.

For every natural input and rational bracket pair, the checker predicate has the explicitly named Decidable instance robinPositiveJudgeDecidable.

Theorem 1.18 (Soundness of the rational checker).

$\forall n \in N, t er m s \in N, g amma \in R a t i o na lB r a c k e t, l o gL o g \in R a t i o na lB r a c k e t, (C o n t ain s (g amma, e u l er M a sc h ero ni C o n s t an t ()) \land (C o n t ain s (l o gL o g, l o g (l o g (c a s tR e a l (n)))) \land R o bin P os i t i v e J u d g e (n, t er m s, g amma, l o gL o g))) \Rightarrow 0 < ro bin De lt a (n)$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.robinPositiveJudge_sound (✓ std3). ∎

Source. Repository-derived.

Commentary.

Valid semantic brackets and this module’s own auxiliary judge imply positivity of the additive Robin gap. The proof lower-bounds exp(gamma_EM) by the truncated Taylor sum from the exact rational basis in 「ZECKENDORF_EULER_5040 附录」 and uses monotonicity. This is the general result named by the checker utility record, not an identity with the volume’s logarithmic margin.

Theorem 1.19 (Logarithm bounds after binary scaling).

$\forall y \in R, k \in N, K \in N, (1 \leq k \land (1 \leq y \land y < 2)) \Rightarrow c a s tR e a l (k) \cdot \frac{6931471803}{10000000000} + a t anh P a r t ia l (\frac{y - 1}{( y + 1 )}, K) < l o g ((2)^{k} \cdot y) \land l o g ((2)^{k} \cdot y) < c a s tR e a l (k) \cdot \frac{6931471808}{10000000000} + a t anh P a r t ia l (\frac{y - 1}{( y + 1 )}, K) + \frac{2 \cdot (( \frac{y - 1}{( y + 1 )} ) ) ^{2 \cdot K + 1}}{( c a s tR e a l ( 2 \cdot K + 1 ) \cdot ( 1 - (( \frac{y - 1}{( y + 1 )} ) ) ^{2} ) )}$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.log_pow_two_mul_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

For positive natural k and 1 <= y < 2, the appendix log-2 bracket and sharp atanh remainder give the displayed enclosure of log(2^k y).

Theorem 1.20 (Transfer a checked atanh calculation).

$\forall x \in R, y \in R, l o \in R, hi \in R, k \in N, K \in N, x = (2)^{k} \cdot y \land 1 \leq k \land 1 \leq y \land y < 2 \land l o < c a s tR e a l (k) \cdot \frac{6931471803}{10000000000} + a t anh P a r t ia l (\frac{y - 1}{( y + 1 )}, K) \land c a s tR e a l (k) \cdot \frac{6931471808}{10000000000} + a t anh P a r t ia l (\frac{y - 1}{( y + 1 )}, K) + \frac{2 \cdot (( \frac{y - 1}{( y + 1 )} ) ) ^{2 \cdot K + 1}}{( c a s tR e a l ( 2 \cdot K + 1 ) \cdot ( 1 - (( \frac{y - 1}{( y + 1 )} ) ) ^{2} ) )} < hi \Rightarrow (l o < l o g (x) \land l o g (x) < hi)$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.rational_log_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

An exact identity x=2^k y and a checked pair of rational endpoint inequalities transfer to lo < log x < hi. This public helper is consumed by module 2.

Theorem 1.21 (Transfer logarithm endpoint bounds).

$\forall x \in R, a \in R, b \in R, l o \in R, hi \in R, (0 < a \land (a < x \land (x < b \land (l o < l o g (a) \land l o g (b) < hi)))) \Rightarrow (l o < l o g (x) \land l o g (x) < hi)$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.log_interval_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

For 0<a<x<b, a certified lower bound for log a and upper bound for log b transfer across strict monotonicity of the real logarithm.

Theorem 1.22 (Rational bounds for log 10080).

$\frac{921830853}{100000000} < l o g (10080) \land l o g (10080) < \frac{184366171}{20000000}$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.log_10080_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

The public exact-rational calculation encloses log 10080 between the displayed endpoints.

Theorem 1.23 (Rational bounds for log log 10080).

$\frac{55529789}{25000000} < l o g (l o g (10080)) \land l o g (l o g (10080)) < \frac{222119157}{100000000}$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.logLog_10080_bounds (✓ std3). ∎

Source. Repository-derived.

Commentary.

The public interval transfer encloses log(log 10080); its endpoints are those stored in logLog10080Bracket.

Definition 1.24 (Concrete gamma checker input).

$g amma B r a c k e t = R a t i o na lB r a c k e t (\frac{5772155}{10000000}, \frac{5772161}{10000000})$

Formalization. D5/S3/Arith/GoldenResource/RobinRationalBasis.gammaBracket (✓ std3).

Source. Repository-derived.

Commentary.

gammaBracket is exactly the pair 5772155/10000000 and 5772161/10000000.

Definition 1.25 (Concrete log-log checker input).

$l o gL o g 10080 B r a c k e t = R a t i o na lB r a c k e t (\frac{55529789}{25000000}, \frac{222119157}{100000000})$

Formalization. D5/S3/Arith/GoldenResource/RobinRationalBasis.logLog10080Bracket (✓ std3).

Source. Repository-derived.

Commentary.

logLog10080Bracket is exactly the pair 55529789/25000000 and 222119157/100000000.

Theorem 1.26 (First exact checker computation).

$R o bin P os i t i v e J u d g e (10080, 4, g amma B r a c k e t, l o gL o g 10080 B r a c k e t)$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.robin_positive_judge_10080 (✓ std3). ∎

Source. Repository-derived.

Commentary.

Kernel reduction proves that four exponential terms make the rational checker true at n=10080. The exact divisor sum sigma_1(10080)=39312 is proved privately.

Theorem 1.27 (Positive additive Robin gap at 10080).

$0 < ro bin De lt a (10080)$

Proof. Machine-checked in Lean as D5/S3/Arith/GoldenResource/RobinRationalBasis.robin_delta_10080_pos (✓ std3). ∎

Source. Repository-derived.

Commentary.

Checker soundness, the two semantic brackets, and the decided four-term input from the exact rational basis in 「ZECKENDORF_EULER_5040 附录」 prove that this module’s own auxiliary additive Robin gap is positive at 10080 without floating point; this is not an identity with the volume’s logarithmic margin.

References

Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.Contains
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.RationalBracket
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.RobinPositiveJudge
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.atanhParameter
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.atanhParameter_lt_third
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.atanhPartial
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.eulerMascheroni_decimal_bounds
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.eulerMascheroni_remainder_bounds
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.eulerMascheroni_tail_identity
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.expPartial
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.expPartial_eq_sum
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.gammaBracket
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.logLog10080Bracket
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.logLog_10080_bounds
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.logRemainder
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.log_10080_bounds
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.log_expansion_remainder_bound
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.log_harmonic_term_bounds
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.log_interval_bounds
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.log_pow_two_mul_bounds
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.log_two_decimal_bounds
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.rational_log_bounds
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.robinDelta
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.robinPositiveJudgeDecidable
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.robinPositiveJudge_sound
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.robin_delta_10080_pos
Truth anchor: D5/S3/Arith/GoldenResource/RobinRationalBasis.robin_positive_judge_10080

Keyboard shortcuts

trureturing Blueprint

Rational Basis for the Robin Certificate

Abstract

References