Metadata

slug: bala126156
bibkey: bala2026a126156
doi: null
url: https://oeis.org/A126156
triage: theorem
motivation_gids:
  - D5/S1/Recurrence/Periodic/SquareRootSecantTotientPeriodRefutation

The A126156 eventual totient-period conjecture is false

Problem

OEIS A126156, revision 110, NAME:

Expansion of e.g.f. sqrt(sec(sqrt(2)*x)), showing coefficients of only the even powers of x.

The third COMMENTS entry states:

Conjecture: the sequence {a(n)} reduced modulo a positive integer k is eventually periodic with the period dividing phi(k), where phi(n) = A000010(n). An example is given below. - Peter Bala, Mar 01 2026

The source has offset zero. For a rational formal power series $A$ with $A (0) = 1$ and $A (x)^{2} cos (2 x) = 1$ , put $a_{A} (n) = (2 n)! [x^{2 n}] A$ . The assertion includes existence of such a series and says that, for every such $A$ and every positive natural modulus $k$ , there are natural numbers $N, p$ with $p > 0$ , $p ∣ φ (k)$ and $a_{A} (n + p) - a_{A} (n) = k z$ for some integer $z$ at every $n \geq N$ . The delivered claim is this positive universal assertion; result negates it.

Statement echo

Source clause	Lean counterpart	Fidelity
Rational expansion of $cos (2 x)$	`cosSqrtTwo`	At even degree $j$ , $(- 2)^{j /2} / j!$ ; at odd degree, zero.
Square root with constant term one	`IsSourceEGF`	Both the constant-coefficient condition and the square equation.
Even-power EGF coefficients; offset zero	Factorial coefficient expressions in `claim`	The expressions are literal; proofs use the existing `IntegralEGFComposition.eCoeff`.
Every positive integer modulus	Natural `k` and `0 < k`	Positive integers have the same domain.
Eventually	Natural `N`; every natural `n` with `N ≤ n`	No onset is fixed or bounded.
Period dividing the totient	Natural `p`, `0 < p`, `p ∣ Nat.totient k`	Every positive divisor is retained.
Reduced modulo $k$	Existential integer multiple of $k$ in the rational field	The coefficients’ integrality is derived, not assumed.
The sequence exists	Existential source-series conjunct in `claim`	A preregistered existence conjunct, not an extra hypothesis on `result`.

Motivation

Preregistration #22077 identifies this first-tier external named conjecture. The settling GID is D5/S1/Recurrence/Periodic/SquareRootSecantTotientPeriodRefutation.result; its admission basis is open-problem-resolution (#22077; Refuted). The Library source note identifies the OEIS locator. There is no source DOI or arXiv identifier.

Gap

The inspected literature in #22077 contains no identified settlement of the universal eventual-period assertion. Its screen includes the OEIS entry and history, Bala’s triangle note, Singh’s arithmetic-convolution paper, the two Connes–Consani–Moscovici moment papers, and the stated generalized-Euler congruences of Gessel and Nishibuchi. The generalized-Euler family inspected there differs from the half-power secant series here. The triangle-to-EGF characterization is not assumed or proved by this module: it uses the EGF source definition directly. Literature completeness is ASSUMED-UNVERIFIED.

Route

Write $D$ for formal differentiation and $C (x) = cos (2 x)$ . The private cos_second proves $D^{2} C = - 2 C$ . Differentiating $A^{2} C = 1$ yields the system $D A = A U$ , $D U = 1 + 2 U^{2}$ , with $U (0) = 0$ (source_system). For the integer-polynomial operator $L (P) = XP + (1 + 2 X^{2}) P^{'}$ , iterated differentiation gives $D^{r} A = A (L^{r} 1) (U)$ (deriv_iter). Consequently $a_{A} (n) = [X^{0}] L^{2 n} 1$ (source_intA), which proves integrality.

The coefficient calculation step_four gives $[X^{0}] L^{4} P + [X^{0}] P = 4 (2 [X^{0}] P + 11 [X^{2}] P + 6 [X^{4}] P)$ . The parity invariant intA_odd and this identity imply $a_{A} (n + 2) - a_{A} (n) = 4 z + 2$ for some integer $z$ , for every natural $n$ (persistent_obstruction). This is an all-index identity.

Falsifier

At $k = 4$ , $φ (4) = 2$ and the permitted positive periods are $1, 2$ . Period $2$ contradicts persistent_obstruction at any proposed onset. Period $1$ implies period $2$ by adding consecutive differences, so it is also excluded. A finite failed shift alone would not exclude arbitrary onsets. The proof uses the all-index obstruction instead.

Evidence

The settling theorem is D5.S1.Recurrence.Periodic.SquareRootSecantTotientPeriodRefutation.result. The private declarations cited in Route are in that same module and feed its proof. The public result is the designated refutation result (basis=refutes) and is exempt from four-slot escape registration (CLAUDE.md §3.9).

The independent finite experiment is the pinned experiment directory. The script is docs/reports/bala-a126156-totient-period/check.py at commit c2e136ef37ea6d8610d3bdb475f70a20fc3515e3, SHA-256 1d2ea054dbc8cb7285102d90275b218c13553923476f1393efa546e0e33e1650. Command: python3 /Users/auric/trureturing-experiments/docs/reports/bala-a126156-totient-period/check.py; exit code: 0. Its local bytes equal the script at the cited commit. The triangle, tangent recurrence and exact rational EGF recovery agree at $n = 0, \dots, 200$ . All 17 displayed A126156 terms, the displayed triangle row at $n = 4$ , and all 28 displayed modulus-55 residues agree. The residue cycle $1, 1, 3, 3$ holds through $n = 200$ ; the two-step differences were checked at $n = 0, \dots, 198$ . Shift $20$ modulo $55$ holds at $n = 1, \dots, 180$ . These finite readings do not prove any uniform extension.

Triage

Item	Status and evidence
The binding universal claim is false, with no extra hypothesis.	Proved, kernel-checked: `result : ¬ claim`.
For every source EGF, factorial-normalized even coefficients are integers and odd, and every two-step difference is $2$ modulo $4$ .	Proved, kernel-checked: `source_intA` identifies the coefficients with integer polynomial coefficients; `intA_odd` proves their parity; `persistent_obstruction` gives the difference.
No positive eventual period dividing $φ (4)$ exists at any onset; period $1$ would also give period $2$ .	Proved inside the kernel-checked `result`: divisor classification and addition of consecutive differences give the contradiction from `persistent_obstruction`. No separate public theorem is added.
Residue cycle $1, 1, 3, 3$ through $n = 200$ .	Computed: the pinned checker and command in Evidence, exit 0. The module adds no separate four-cycle theorem.
The displayed modulus-55 example and shift $20$ on $n = 1, \dots, 180$ .	Computed: the pinned checker and command in Evidence, exit 0.
A universal revised bound such as $2 φ (k)$ and any general odd-modulus theorem.	Open: neither is settled by this module or by the finite experiment.

What the settlement shows

The failure is the factor-of-two obstruction at modulus $4$ : the scaled coefficients remain odd and a shift by two always changes the residue by two. The finite four-cycle is compatible with allowing period four at this modulus; a universal twice-totient bound remains open. The displayed modulus-55 example survives on its tested interval. The literature screen in #22077 identified no result in the inspected moment papers that relies on Bala’s conjecture; this is a bounded literature reading, not a theorem about every source citing the sequence.

ASSUMED-UNVERIFIED

Completeness of prior art and worldwide priority are not established. The literature readings are the orchestrator’s and the named research seats’ readings recorded in #22077. Rate-limited services, an arXiv full-text index missing known occurrences, unread Grebenkov and Oste–Van der Jeugt full texts, Wall page 366, the Connes journal version, and the SSRN citing work leave the screen incomplete. These are literature boundaries, not premises of the Lean theorem. No triangle-to-EGF identity, universal twice-totient bound, or general odd-modulus theorem is claimed.

Keyboard shortcuts

trureturing — Discovering truth