Central Bell Cubic Refutations

Abstract

Rational double-root certificates refute the two distinct-root claims for the printed n = 3, lambda = 3 central Bell cosine cubics. The proposed D5/S1/Polynomial bucket does not exist; D5/S3/Arith is the nearest existing integer/polynomial-arithmetic owner, and capacity was checked.

Definition 1.1 (Expanded Euler-type cubic).

$\forall x \in C, y \in C, z \in C, e u l er C u bi c (x, y, z) = - \frac{9 \cdot x}{4} + x^{3} - 3 \cdot x \cdot y^{2} - 2 \cdot z + 3 \cdot x^{2} \cdot z - 3 \cdot y^{2} \cdot z + 3 \cdot x \cdot z^{2} + z^{3}$

Formalization. D5/S3/Arith/CentralBellCubicRefutation.eulerCubic (✓ std3).

Citation. Waseem Ahmad Khan and Francesco Aldo Costabile and Khidir Shaib Mohamed and Ugur Duran and Abdulghani Muhyi and Azhar Iqbal and Wei Sin Koh (2026). Algebraic properties of central Bell-based type 2 Bernoulli and Euler polynomials of complex variable. DOI: 10.3934/nhm.2026030.

Commentary.

This repository definition transcribes the printed n = 3, lambda = 3 Euler-type cosine cubic, with all three arguments and its value in the complex numbers. Khan et al., Networks and Heterogeneous Media 21(2) (2026), 693-724, DOI 10.3934/nhm.2026030, Conjecture 3, is the claim in scope; the paper is not cited as proving the refutation below.

Definition 1.2 (Expanded Bernoulli-type cubic).

$\forall x \in C, y \in C, z \in C, b er n o u ll i C u bi c (x, y, z) = - \frac{3 \cdot x}{4} + x^{3} - 3 \cdot x \cdot y^{2} - \frac{z}{2} + 3 \cdot x^{2} \cdot z - 3 \cdot y^{2} \cdot z + 3 \cdot x \cdot z^{2} + z^{3}$

Formalization. D5/S3/Arith/CentralBellCubicRefutation.bernoulliCubic (✓ std3).

Commentary.

This repository definition transcribes the printed n = 3, lambda = 3 Bernoulli-type cosine cubic, with all arguments and its value complex. Conjecture 1 of the same paper is the claim in scope. The definition uses the printed expansion; its factorization is derived in the proof.

Definition 1.3 (Three pairwise distinct complex zeros).

$\forall f \in C \to C, H a s T h reeD i s t in c tR oo t s (f) \Leftrightarrow (\exists a \in C, b \in C, c \in C, f (a) = 0 \land (f (b) = 0 \land (f (c) = 0 \land (a \neq = b \land (a \neq = c \land b \neq = c)))))$

Formalization. D5/S3/Arith/CentralBellCubicRefutation.HasThreeDistinctRoots (✓ std3).

Source. Repository-derived.

Commentary.

The predicate asks for three zeros and all three pairwise inequalities. It counts distinct complex solutions, not algebraic multiplicities. Both refutation theorems use this predicate.

Definition 1.4 (Finite generating-function jet).

$\forall q \in C, x \in C, y \in C, z \in C, e g fJ e t (q, x, y, z) = (1 - C (q) \cdot X^{2}) \cdot (1 + C (x) \cdot X + C (\frac{x ^{2}}{2}) \cdot X^{2} + C (\frac{x ^{3}}{6}) \cdot X^{3}) \cdot (1 - C (\frac{y ^{2}}{2}) \cdot X^{2}) \cdot (1 + C (z) \cdot X + C (\frac{z ^{2}}{2}) \cdot X^{2} + C (\frac{z ^{3}}{6} + \frac{z}{24}) \cdot X^{3})$

Formalization. D5/S3/Arith/CentralBellCubicRefutation.egfJet (✓ std3).

Source. Repository-derived.

Commentary.

The product is a polynomial over the complex numbers. C denotes Polynomial.C and X denotes Polynomial.X. It records the four finite jets, including the central Bell z/24 contribution, without asserting an infinite-series identity.

Theorem 1.5 (Euler coefficient identity).

$\forall x \in C, y \in C, z \in C, 6 \cdot coe ff (e g fJ e t (\frac{3}{8}, x, y, z), 3) = e u l er C u bi c (x, y, z)$

Proof. Machine-checked in Lean as D5/S3/Arith/CentralBellCubicRefutation.euler_egf_coefficient (✓ std3). ∎

Source. Repository-derived.

Commentary.

Six times the degree-three coefficient with prefactor parameter 3/8 is the printed Euler cubic. coeff denotes Polynomial.coeff.

Theorem 1.6 (Bernoulli coefficient identity).

$\forall x \in C, y \in C, z \in C, 6 \cdot coe ff (e g fJ e t (\frac{1}{8}, x, y, z), 3) = b er n o u ll i C u bi c (x, y, z)$

Proof. Machine-checked in Lean as D5/S3/Arith/CentralBellCubicRefutation.bernoulli_egf_coefficient (✓ std3). ∎

Source. Repository-derived.

Commentary.

Six times the degree-three coefficient with prefactor parameter 1/8 is the printed Bernoulli cubic.

Theorem 1.7 (Shifted Euler identity).

$\forall x \in C, y \in C, z \in C, e u l er C u bi c (x, y, z) = (x + z)^{3} - 3 \cdot (x + z) \cdot (y^{2} + \frac{3}{4}) + \frac{z}{4}$

Proof. Machine-checked in Lean as D5/S3/Arith/CentralBellCubicRefutation.euler_coefficient_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

The shift x+z isolates the Euler quadratic parameter y squared plus 3/4.

Theorem 1.8 (Shifted Bernoulli identity).

$\forall x \in C, y \in C, z \in C, b er n o u ll i C u bi c (x, y, z) = (x + z)^{3} - 3 \cdot (x + z) \cdot (y^{2} + \frac{1}{4}) + \frac{z}{4}$

Proof. Machine-checked in Lean as D5/S3/Arith/CentralBellCubicRefutation.bernoulli_coefficient_bridge (✓ std3). ∎

Source. Repository-derived.

Commentary.

The shift x+z isolates the Bernoulli quadratic parameter y squared plus 1/4.

Theorem 1.9 (Euler rational factorization).

$\forall x \in C, e u l er C u bi c (x, \frac{1}{2}, 8) = (x + 7)^{2} \cdot (x + 10)$

Proof. Machine-checked in Lean as D5/S3/Arith/CentralBellCubicRefutation.euler_factorization (✓ std3). ∎

Source. Repository-derived.

Commentary.

At the rational parameters 1/2 and 8, the repeated factor is x+7.

Theorem 1.10 (Bernoulli rational factorization).

$\forall x \in C, b er n o u ll i C u bi c (x, \frac{2}{3}, \frac{125}{27}) = (x + \frac{205}{54})^{2} \cdot (x + \frac{170}{27})$

Proof. Machine-checked in Lean as D5/S3/Arith/CentralBellCubicRefutation.bernoulli_factorization (✓ std3). ∎

Source. Repository-derived.

Commentary.

At the rational parameters 2/3 and 125/27, the repeated factor is x+205/54.

Theorem 1.11 (Bernoulli rational parameter identities).

$(\frac{2}{3})^{2} + \frac{1}{4} = (\frac{5}{6})^{2} \land \frac{\frac{125}{27}}{4} = 2 \cdot (\frac{5}{6})^{3}$

Proof. Machine-checked in Lean as D5/S3/Arith/CentralBellCubicRefutation.bernoulli_parameter_identities (✓ std3). ∎

Source. Repository-derived.

Commentary.

Both equalities hold in the rationals and exhibit the parameter 5/6 in the Bernoulli double-root certificate.

Theorem 1.12 (Euler rational double-root refutation).

$(\exists y \in Q, z \in Q, y = \frac{1}{2} \land (z = 8 \land ((\forall x \in C, e u l er C u bi c (x, o f R e a l (v a l (y)), o f R e a l (v a l (z))) = 0 \Leftrightarrow (x = - 7 \lor x = - 10)) \land (\neg H a s T h reeD i s t in c tR oo t s (x \mapsto e u l er C u bi c (x, o f R e a l (v a l (y)), o f R e a l (v a l (z)))))))) \land (- 7 \neq = - 10 \land (\neg (\forall y \in R, z \in R, H a s T h reeD i s t in c tR oo t s (x \mapsto e u l er C u bi c (x, o f R e a l (y), o f R e a l (z))))))$

Proof. Machine-checked in Lean as D5/S3/Arith/CentralBellCubicRefutation.conjecture3_refuted (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the printed n = 3, lambda = 3 cubics, the Euler parameters y = 1/2 and z = 8 are rational and the entire complex zero set is {-7,-10}. These roots are unequal, so there are exactly two distinct solutions and there cannot be three. The last conjunct refutes the universal real-parameter reading of Conjecture 3 at this degree and lambda. It also refutes any universal-lambda reading that includes 3.

In both refutation formulas, val denotes Rat.cast : Rat -> Real and ofReal denotes Complex.ofReal : Real -> Complex. Thus the nested coercions in the rational witness and the single coercions in the universal clause are explicit. Every displayed division is field division.

Provenance correction: the atom bracket’s lambda=1 is an orchestrator typo corrected by 评注 27.847 (PR #5860). This module refutes the paper’s printed n = 3, lambda = 3 cubics; the existing 4.105 and 4.106 atoms remain the coverage targets.

The live proof extracts six times the degree-three coefficient of the finite generating-function jet with Euler prefactor 1-3t^2/8. It identifies the result with the expanded cubic, rewrites it as (x+z)^3-3(x+z)(y^2+3/4)+z/4, and proves the factorization (x+7)^2(x+10). Product-zero reasoning gives the complete root set. The finite-jet coefficient identity is kernel checked; an identity with the full infinite generating function is not asserted.

Theorem 1.13 (Bernoulli rational double-root refutation).

$(\exists y \in Q, z \in Q, y = \frac{2}{3} \land (z = \frac{125}{27} \land ((\forall x \in C, b er n o u ll i C u bi c (x, o f R e a l (v a l (y)), o f R e a l (v a l (z))) = 0 \Leftrightarrow (x = - \frac{205}{54} \lor x = - \frac{170}{27})) \land (\neg H a s T h reeD i s t in c tR oo t s (x \mapsto b er n o u ll i C u bi c (x, o f R e a l (v a l (y)), o f R e a l (v a l (z)))))))) \land (- \frac{205}{54} \neq = - \frac{170}{27} \land (\neg (\forall y \in R, z \in R, H a s T h reeD i s t in c tR oo t s (x \mapsto b er n o u ll i C u bi c (x, o f R e a l (y), o f R e a l (z))))))$

Proof. Machine-checked in Lean as D5/S3/Arith/CentralBellCubicRefutation.conjecture1_refuted (✓ std3). ∎

Source. Repository-derived.

Commentary.

For the printed n = 3, lambda = 3 cubics, the Bernoulli parameters y = 2/3 and z = 125/27 are rational and the entire complex zero set is {-205/54,-170/27}. The inequality of these two roots and the absence of three distinct roots are both explicit. The last conjunct refutes the universal real-parameter reading of Conjecture 1 at this degree and lambda, hence any universal-lambda reading including 3.

The finite-jet prefactor is 1-t^2/8. The coefficient bridge gives (x+z)^3-3(x+z)(y^2+1/4)+z/4. Exact rational arithmetic then yields (x+205/54)^2(x+170/27), and the proof determines all complex zeros before excluding three pairwise distinct ones. As for the Euler case, the kernel statement concerns the printed cubic and the finite coefficient computation, not an infinite-series theorem.

References

Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.HasThreeDistinctRoots
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.bernoulliCubic
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.bernoulli_coefficient_bridge
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.bernoulli_egf_coefficient
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.bernoulli_factorization
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.bernoulli_parameter_identities
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.conjecture1_refuted
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.conjecture3_refuted
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.egfJet
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.eulerCubic
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.euler_coefficient_bridge
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.euler_egf_coefficient
Truth anchor: D5/S3/Arith/CentralBellCubicRefutation.euler_factorization

Keyboard shortcuts

trureturing Blueprint

Central Bell Cubic Refutations

Abstract

References