noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformLogLower : ℝ

Lower endpoint of the fixed 32-term odd-log expansion, evaluated exactly.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformLogLower = 65950865779868241286341246906292389374730392248406166651554921752248327983608712622624452911395657604020873914345906954334860 / 139200177231575000540913611420539494385060560737387374997917880249188693846020408531067587241017041316034446547352995184835249

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformLogUpper : ℝ

Upper endpoint after adding the analytic tail, not a floating-point estimate.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformLogUpper = 65950865779868241286341246906292389374732357269754084435583521752248327983608712622624452911395657604020873914345906954334860 / 139200177231575000540913611420539494385060560737387374997917880249188693846020408531067587241017041316034446547352995184835249

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformScalar : ℝ

The coefficient of the existing actual uniform-8 G11 estimate.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformScalar = 8 * (561522 / 1000000) * MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral fun (x : ℝ) => 1

noncomputable def MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformScalarUpper : ℝ

Rational upward rounding at the prescribed denominator.

Equations

• MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformScalarUpper = 10385101 / 100000000

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_one_eq_uniform_primitives : (goldbachG11PrimeIntegral fun (x : ℝ) => 1) = g11AuthorPrimitive0 (4 / 33) - g11AuthorPrimitive0 (4 / 53)

Only the unweighted kernel primitive is consumed from the imported file.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11PrimeIntegral_one_eq_uniform_log : (goldbachG11PrimeIntegral fun (x : ℝ) => 1) = 15 + 53 / 8 * Real.log (53 / 33) ^ 2 - 139 / 4 * Real.log (53 / 33)

Exact endpoint reduction; the linear logarithm coefficient is negative.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformLog_endpoints_eq : g11UniformLogLower = 2 * ∑ k ∈ Finset.range 32, (10 / 43) ^ (2 * k + 1) / (2 * ↑k + 1) ∧ g11UniformLogUpper = g11UniformLogLower + 2 * (10 / 43) ^ 65 / (1 - (10 / 43) ^ 2)

The exact lower and upper rational literals agree with the fixed analytic budget.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformLog_bounds : g11UniformLogLower ≤ Real.log (53 / 33) ∧ Real.log (53 / 33) ≤ g11UniformLogUpper

Analytic odd-log bounds, with exactly 32 terms and no numerical oracle.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformScalar_enclosure : 8 * (561522 / 1000000) * (15 + 53 / 8 * g11UniformLogLower ^ 2 - 139 / 4 * g11UniformLogUpper) ≤ g11UniformScalar ∧ g11UniformScalar ≤ 8 * (561522 / 1000000) * (15 + 53 / 8 * g11UniformLogUpper ^ 2 - 139 / 4 * g11UniformLogLower)

Separate directions: the positive square uses the upper log endpoint, whereas the negative linear term uses the lower endpoint. The lower bound reverses those choices. Thus there is no sign-incorrect endpoint substitution.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformScalar_rational_budget : 8 * (561522 / 1000000) * (15 + 53 / 8 * g11UniformLogUpper ^ 2 - 139 / 4 * g11UniformLogLower) < g11UniformScalarUpper ∧ g11UniformScalarUpper - 8 * (561522 / 1000000) * (15 + 53 / 8 * g11UniformLogLower ^ 2 - 139 / 4 * g11UniformLogUpper) ≤ 1 / 1000000

Exact rational comparison of both analytic endpoints with the rounded upper.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformScalar_lt_upper : g11UniformScalar < g11UniformScalarUpper

Strictness leaves enough genuine slack to obtain a fixed numeric count bound.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.g11UniformScalar_upper_error : 0 ≤ g11UniformScalarUpper - g11UniformScalar ∧ g11UniformScalarUpper - g11UniformScalar ≤ 1 / 1000000

Requested one-sided error certificate for the actual uniform-8 coefficient.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_uniform8_coefficient_error : (0 ≤ 10385101 / 100000000 - 8 * (561522 / 1000000) * goldbachG11PrimeIntegral fun (x : ℝ) => 1) ∧ (10385101 / 100000000 - 8 * (561522 / 1000000) * goldbachG11PrimeIntegral fun (x : ℝ) => 1) ≤ 1 / 1000000

Literal version for consumers that do not unfold the scalar definitions.

theorem MathlibNt.SieveTheory.LiLiuOnePlusOneNine.GoldbachBig.goldbachG11_uniform8_coefficient_gt_author_number : 10191 / 100000 < 8 * (561522 / 1000000) * goldbachG11PrimeIntegral fun (x : ℝ) => 1

Explicitly excludes relabeling the present coefficient as the author's 0.10191.