Skip to content

1 + 2 + 3 + … = −1/12: one S, or two?

Vitaly Reznik

"The sum of all natural numbers is minus one twelfth." The equation is Srinivasa Ramanujan's: he gave two derivations of it in chapter 8 of his first notebook and wrote it to G. H. Hardy in his second letter, dated 27 February 1913. A Numberphile video of January 2014 made it widely known. The usual answer is that the series has no sum in the ordinary sense, and that −1/12 is the value a particular method assigns to it. I agree, and I add no new mathematics. What I add is a reading in which the method is written down as a parameter of the claim. Read that way, the famous derivation is correct for its method, but it pads and shifts series as if every zero were harmless, and it never says why. For S itself, a zero in front is not harmless.

On this page proved marks a theorem checked in Lean 4, a proof assistant in which a machine checks every step; its name is given, and the code is at the end. My reading marks what I take the results to mean. Open marks what is not settled.

Terms

  • S is the series 1 + 2 + 3 + 4 + … . Its partial sums are Sₙ = 1 + 2 + … + n = n(n + 1)/2.
  • A summation method σ assigns numbers to some series. A method is additive if σ(a + b) = σ(a) + σ(b) when the series a + b is added term by term. It is linear if, in addition, σ(c·a) = c·σ(a). It is stable if a zero put in front does not change the value: σ(0, a₁, a₂, …) = σ(a₁, a₂, …).
  • Abel summation gives a series a₁ + a₂ + … the limit of a₁x + a₂x² + a₃x³ + … as x rises to 1. It is linear and stable: a zero in front multiplies the whole sum by x, and x tends to 1. It gives 1 − 1 + 1 − … = 1/2 and 1 − 2 + 3 − … = 1/4, but it gives 1 + 2 + 3 + … no value.
  • Zeta regularisation gives a series a₁ + a₂ + … the value at s = 0 of the function a₁·1⁻ˢ + a₂·2⁻ˢ + a₃·3⁻ˢ + … . The sum converges only for large s, but it may have an analytic continuation: a unique extension beyond the region where it converges. For S the function is ζ(s − 1), where ζ is Riemann's zeta function; its continuation exists for every s except s = 2, so S gets ζ(−1) = −1/12. A series whose function has no continuation to s = 0 gets no value.

What is already known

  • Hardy (Divergent Series, 1949) is the standard account of summation methods: they are different operations, and they assign a divergent series different values.
  • Tao (blog post, 10 April 2010: "The Euler–Maclaurin formula, Bernoulli numbers, the zeta function, and real-variable analytic continuation") shows where −1/12 comes from without complex analysis. Take a smooth cutoff η, equal to 1 near 0 and to 0 for large arguments. Then 1·η(1/N) + 2·η(2/N) + 3·η(3/N) + … equals −1/12 + C·N² + (terms that vanish as N grows). The constant C depends on η; the −1/12 does not.
  • A method that is linear and stable, and that gives 1 + 0 + 0 + … the value 1, cannot give S any value at all (Wikipedia, "1 + 2 + 3 + 4 + ⋯", section on summation methods). Proved below in this form (no_stable_additive_sum): a method whose domain contains S, 1 + 1 + 1 + … and 1 + 0 + 0 + … and is closed under a zero in front, which is additive on the splits used and stable, and whose values obey "x + y = y forces x = 0", gives 1 + 0 + 0 + … the value 0. So if it gives that series a nonzero value, it cannot contain S.

The claim, with its method written down

ZTL, the logic this site is about, has three values: true, false, and Z. Z marks a dirty parameter: a value that is not ours, that its owner may change between two reads, and that therefore has to be read separately at each place it occurs. A verdict is EARNED if it holds however the dirty parameters turn out. It is REFUTED if it fails however they turn out. It is OPEN if it depends on them. And it is EARNED IF STABLE if it holds whenever each dirty parameter is read the same at every occurrence.

In "1 + 2 + 3 + … = −1/12" the dirty parameter is the method: the notation does not name it. I make the claim a function of one parameter M, the method. That encoding is my choice. Given it, ZTL's judge (a program, not a theorem) returns:

  • M not given: OPEN;
  • M = zeta regularisation: EARNED;
  • M = the limit of the partial sums: REFUTED.

These verdicts only report what the choice of method decides. They are not a discovery. The mathematics behind them:

  • Proved (no axioms): the partial sums run past every bound, since Sₙ ≥ n (partial_sums_unbounded). So no limit exists, and for every n ≥ 1, Sₙ is more than 1 away from −1/12 (not_limit_neg_twelfth).
  • Proved (no axioms): −B₂/2 = −1/12 (zeta_neg_one). The Bernoulli numbers B₀, B₁, B₂, … are defined by a recursion, and for n ≥ 1 a general rule, ζ(−n) = −Bₙ₊₁/(n + 1), gives ζ at the negative integers. The theorem computes B₂ = 1/6 by that recursion (bern_two). Evaluating bernList 5 in Lean shows B₀ to B₅ as 1, −1/2, 1/6, 0, −1/30, 0 (the convention B₁ = −1/2); that list is a computation, not a theorem.
  • Proved with Mathlib, a large library that rests on the three standard axioms of classical mathematics: ζ(−1) = −1/12 (riemannZeta_neg_one, from Mathlib's riemannZeta_neg_nat_eq_bernoulli). Mathlib uses its own Bernoulli numbers; both definitions give −1/12 here, but no theorem links the two.

The famous derivation, in full

As it is usually presented:

  1. A = 1 − 1 + 1 − 1 + … = 1/2. The step is 1 − A = A.
  2. B = 1 − 2 + 3 − 4 + … . Add B to itself shifted by one place, 0 + 1 − 2 + 3 − …, term by term: the result is A. So 2B = 1/2, and B = 1/4.
  3. S − 4S. Write 4S with zeros in between, as 0 + 4 + 0 + 8 + 0 + 12 + …, and subtract it from S term by term: 1 + (2 − 4) + 3 + (4 − 8) + … = B. So −3S = 1/4, and S = −1/12.

Steps 1 and 2 shift a series by one place, which is putting a zero in front. For the alternating series A and B that is justified by Abel summation, which is stable. Under zeta regularisation the shifted values also come out right (1/2 and 1/4), but there no stability stands behind it; the values happen to agree. Step 3 inserts zeros between the terms of S. That is harmless under zeta regularisation: in the zero-padded series the number 4n sits at place 2n, so its function is the sum of 4n·(2n)⁻ˢ = 4·2⁻ˢ·ζ(s − 1), and 2⁻ˢ = 1 at s = 0. Zeta regularisation also gives B the value 1/4: B's function is (1 − 4·2⁻ˢ)·ζ(s − 1), and at s = 0 that is (1 − 4)·ζ(−1) = 1/4, the same as Abel's.

So the derivation is correct for zeta regularisation. What it never says is which zeros are harmless, and why.

The same S, one zero in front

Put a zero in front of S: 0 + 1 + 2 + 3 + … . Now the number n − 1 sits at place n. Under zeta regularisation the function is the sum of (n − 1)·n⁻ˢ = ζ(s − 1) − ζ(s), and at s = 0 that is −1/12 − (−1/2) = 5/12.

So the zero that was harmless for A and B is not harmless for S. Under zeta regularisation, S and 0 + S are two different numbers, and the notation gives no warning.

Proved (no axioms), the obstruction. Take any method that gives values (in ordinary numbers, or in any setting where x + y = y forces x = 0) to the three series (1, 2, 3, …), (1, 1, 1, …) and (0, 1, 2, …). Suppose it is additive on the one split (1, 2, 3, …) = (1, 1, 1, …) + (0, 1, 2, …). If it gives (1, 2, 3, …) and (0, 1, 2, …) the same value, then it gives 1 + 1 + 1 + … the value 0 (leading_zero_forces). Zeta regularisation gives 1 + 1 + 1 + … the value ζ(0) = −1/2. Mathlib proves the numbers: ζ(0) = −1/2 (riemannZeta_zero_val) and ζ(−1) − ζ(0) = 5/12 (shifted_value). That these are zeta regularisation's values for 1 + 1 + 1 + … and 0 + S, and that zeta regularisation is additive on that split (the three functions add where they converge, and continuation keeps the sum), is my argument and is not formalised: the method itself is not defined in Lean.

Where ZTL comes in

My reading. Ordinary notation treats the letter S as one object everywhere it appears. ZTL does not. That each occurrence of a dirty parameter is read on its own is ZTL's own rule, not something built for this page: every occurrence of an unverified value is substituted independently (the rule behind all of ZTL's tables; in Lean, the module ZDirty). Identifying two occurrences has to be earned, and ZTL's judge rates the identification of a dirty S with itself as EARNED IF STABLE. What is modelled here is only that the dirty value is a number, where ZTL's own atoms are true or false.

Once a method is fixed, it does not change between reads. What changes is the series written at each place: S itself, S with zeros inserted, 0 + S. So the dirty parameter is the value of S as read at a given place, and each identification of two places is a claim of its own. Under zeta regularisation:

what is written at that place its value the same value as S?
S = 1 + 2 + 3 + … −1/12 —
S with a zero before each term, 0 + 1 + 0 + 2 + 0 + 3 + … −1/12 (the sum of n·(2n)⁻ˢ is 2⁻ˢ·ζ(s − 1)) yes
S with one zero in front, 0 + 1 + 2 + 3 + … 5/12 no

For S itself the derivation uses only identifications of the first kind (its leading zeros are put in front of A and B, not of S), and so it lands on −1/12. Nothing in the notation tells the two kinds apart.

Proved (no axioms), but nearly a definition. A method reads all those occurrences as one value exactly when it gives the same value to every one of the written series (stable_iff_invariant). With the obstruction above it follows that an additive method that gives 1 + 1 + 1 + … a nonzero value cannot read S and 0 + S as one value (not_stable_of_ones).

My reading. This is what ZTL is for. The mathematics is Hardy's and Tao's. It took a book and a blog post to make the careful reading precise: "S" means whatever the method gives at this place, and nothing more. In ZTL that reading is the default. A logic that never identifies two occurrences of a dirty parameter until the identification has been earned does not make the derivation's hidden step: it does not take S and 0 + S, or S and its zero-padded copy, to be one number until the method in use has been shown to give them the same value. So the question "which zeros are harmless, and why?" is raised on the first reading of the derivation, not after a course on divergent series.

The bridge to classical mathematics

Added 2026-11-03. For formulas over true/false atoms, four of ZTL's six verdicts are now proved to be statements about classical propositions, and the other two up to one register of ZTL's own; in ztl-classical (ZClassical/Bridge.lean, theorem dispositions; Mathlib's classical axioms, printed, so this is a classical reading of ZTL, not ZTL's own zero-axiom ground). A clean atom's truth value is given (T or F); a dirty atom's is not, and it may stand for any proposition at all. A dirty atom is read either uniformly (one proposition at every occurrence) or occurrence by occurrence (each occurrence its own; the bridge proves this agrees with ZTL's formal dirty reading, rd_iff; the uniform reading agrees with ZTL's completions, enum_iff). Then:

ZTL's verdict in classical terms
EARNED / REFUTED true / false under every occurrence-by-occurrence reading
EARNED IF STABLE / REFUTED IF STABLE true / false under every uniform reading, but not under every occurrence reading
ON CREDIT, OPEN the uniform readings disagree (some make it true, some false)

Four verdicts translate completely. ON CREDIT and OPEN share the classical row and are told apart only by ZTL's greedy register (evalF: at each connective, a result not proved true counts as false). That split is not a function of the readings: p and ¬¬p, with p dirty, agree under every uniform and every occurrence reading, yet ZTL calls p OPEN and ¬¬p ON CREDIT (credit_not_semantic). So no translation that depends only on how the readings come out can separate the two: here ZTL tells apart formulas that are classically one. The split is a property of ZTL's evaluation procedure, not a classical invariant; that is both what it adds and what it costs.

On this page's case (ZClassical/ZetaReading.lean, selfEq_disposition): let p be "the value of S read at this place is −1/12". The formula "p iff p", with p read at two places, says less than "the two places have one value": only that both values are −1/12 or neither is (two different values, neither of them −1/12, satisfy it too). It follows from the identification, not the other way round, so whatever breaks it breaks the identification too. By the bridge, for any dirty p it is EARNED IF STABLE and not EARNED: true if the two places are read alike, which is exactly what is in question. The table alone says only that some occurrence reading breaks it. What the ζ case adds is that the method itself supplies such a reading: at the place where S is written, ζ gives −1/12, and at the place where 0 + S is written (read as in the table of "Where ZTL comes in"), ζ gives ζ(−1) − ζ(0) = 5/12. The two values are theorems on Mathlib's ζ (riemannZeta_neg_one, shifted_value); reading 0 + S as that shifted series is this page's reading, argued above. That a place's value is an atom of ZTL is the model step below.

Open

  • Open, in part. ZTL's atoms are true or false, and here the parameter is a number. The bridge now translates ZTL's verdicts over true/false atoms (four of six fully). The step from a number to an atom ("the value read at this place is −1/12") is still a model, and the stability of ZZetaBridge is not derived from the bridge.
  • Open. For a given method, which transformations of a series does it respect? This page settles one zero, for one series.
  • Open, in part. A theorem form of that default. The bridge settles the logical half: "p iff p" is EARNED if and only if every occurrence reading keeps it. What remains is the mathematical half, deciding for a given method and transformation whether the method's own values break it. This page does that for ζ and one zero in front of S.

The code

The first two files are Lean 4 core only (leanprover/lean4:v4.29.1): modules ZZeta and ZZetaBridge of the ZTL repository (lean/). The #print axioms lines at their ends report, when run, that no theorem depends on any axiom.

-- SPDX-License-Identifier: Apache-2.0 OR MIT
-- Formalised in Lean by Claude (Anthropic, an AI model) under the curation of Vitaly Reznik, 2026-11-02.
/-!
# ZZeta — "1 + 2 + 3 + ... = -1/12" read by ZTL: the finite facts, ZERO axioms (Lean core only)

The notation names no operation. Three finite facts decide each clean reading and show why the bare one is dirty:

* `zeta_neg_one` — the zeta-continuation reading as a FINITE OPERATION: the Bernoulli numbers by their recursion
  (B₀ = 1, Bₙ = −1/(n+1) Σ_{k<n} C(n+1,k) B_k) and `ζ(−1) = −B₂/2` give −1/12, computed by the kernel. (That
  `ζ(−n) = −B_{n+1}/(n+1)` IS the analytic continuation's value is Mathlib's `riemannZeta_neg_nat_eq_bernoulli` —
  classical axioms: a separate register, the ztl-classical repository (ZClassical/Zeta.lean), not used here.)
* `partial_sums_unbounded`, `not_limit_neg_twelfth` — the limit reading: `S n ≥ n`, so past any N some partial sum
  exceeds any bound; and `|S n − (−1/12)| > 1` for every n ≥ 1 (scaled: `12 < 12·S n + 1`).
* `no_stable_additive_sum` — no summation that is ADDITIVE (`σ(b + c) = σ b + σ c`) and STABLE
  (`σ(0, a₀, a₁, …) = σ a`) on a domain closed under that shift and under the differences used, with
  `σ(1, 0, 0, …) ≠ 0`, contains (1, 2, 3, …). So "1 + 2 + 3 + …" read as `S` and as `0 + S` (a leading zero) is
  not one value of one such operation. (The popular `S − 4S` derivation does NOT use a leading zero: it inserts zeros
  between terms, which zeta regularisation respects. The leading zero shows only that a method need not respect every
  zero — 2026-11-02 correction.)
-/
namespace ZZeta

/-! ## 1. The zeta-continuation value as a finite operation (kernel-computed rationals) -/

/-- a rational as a pair, not normalized: `n / d`, `d > 0` -/
structure Q where
  n : Int
  d : Nat
deriving Repr

def Q.add (a b : Q) : Q := ⟨a.n * b.d + b.n * a.d, a.d * b.d⟩
def Q.mulNat (a : Q) (k : Nat) : Q := ⟨a.n * k, a.d⟩
def Q.neg (a : Q) : Q := ⟨-a.n, a.d⟩
def Q.divNat (a : Q) (k : Nat) : Q := ⟨a.n, a.d * k⟩
/-- equality of the values: cross-multiplication -/
def Q.eqv (a b : Q) : Bool := a.n * b.d == b.n * a.d

def choose : Nat → Nat → Nat
  | _, 0 => 1
  | 0, _ + 1 => 0
  | n + 1, k + 1 => choose n k + choose n (k + 1)

/-- the k-th element (own definition: core's `List.getD` carries `propext`, MEASURED with `#print axioms`) -/
def nth (default : Q) : List Q → Nat → Q
  | [], _ => default
  | x :: _, 0 => x
  | _ :: xs, k + 1 => nth default xs k

/-- Bernoulli numbers (B₁ = −1/2) by the recursion, as a list B₀ … B_n -/
def bernList : Nat → List Q
  | 0 => [⟨1, 1⟩]
  | n + 1 =>
    let prev := bernList n
    let s := (List.range (n + 1)).foldl
      (fun acc k => Q.add acc (Q.mulNat (nth ⟨0, 1⟩ prev k) (choose (n + 2) k))) ⟨0, 1⟩
    prev ++ [Q.divNat (Q.neg s) (n + 2)]

def bern (n : Nat) : Q := nth ⟨0, 1⟩ (bernList n) n

/-- ζ(−1) = −B₂/2 — the value the continuation assigns, by the finite recursion -/
def zetaNegOne : Q := Q.divNat (Q.neg (bern 2)) 2

theorem bern_two : (bern 2).eqv ⟨1, 6⟩ = true := rfl
theorem zeta_neg_one : zetaNegOne.eqv ⟨-1, 12⟩ = true := rfl

/-! ## 2. The limit reading: the partial sums run away -/

def S : Nat → Nat
  | 0 => 0
  | n + 1 => S n + (n + 1)

theorem S_ge (n : Nat) : n ≤ S n := by
  induction n with
  | zero => exact Nat.le_refl 0
  | succ k ih => exact Nat.add_le_add_right ih (k + 1) |> Nat.le_trans (Nat.le_add_left (k + 1) k)

/-- past any N, some partial sum exceeds any bound B -/
theorem partial_sums_unbounded (B N : Nat) : ∃ n, N ≤ n ∧ B < S n :=
  ⟨N + (B + 1), Nat.le_add_right N (B + 1),
   Nat.lt_of_lt_of_le (Nat.lt_of_lt_of_le (Nat.lt_succ_self B) (Nat.le_add_left (B + 1) N)) (S_ge _)⟩

/-- `|S n − (−1/12)| > 1` for n ≥ 1, scaled by 12: `12 < 12·S n + 1` -/
theorem not_limit_neg_twelfth (n : Nat) (hn : 1 ≤ n) : 12 < 12 * S n + 1 :=
  Nat.lt_succ_of_le (Nat.mul_le_mul_left 12 (Nat.le_trans hn (S_ge n)))

/-! ## 3. No stable additive summation sums 1 + 2 + 3 + … -/

def shift0 (a : Nat → Nat) : Nat → Nat
  | 0 => 0
  | n + 1 => a n

def nat1 : Nat → Nat := fun n => n + 1
def ones : Nat → Nat := fun _ => 1
def e1 : Nat → Nat
  | 0 => 1
  | _ + 1 => 0

/-- (1, 2, 3, …) = (1, 1, 1, …) + (0, 1, 2, …), pointwise -/
theorem nat1_split (n : Nat) : nat1 n = ones n + shift0 nat1 n := by
  cases n with
  | zero => rfl
  | succ k => show k + 1 + 1 = 1 + (k + 1); exact Nat.add_comm (k + 1) 1

/-- (1, 1, 1, …) = (1, 0, 0, …) + (0, 1, 1, …), pointwise -/
theorem ones_split (n : Nat) : ones n = e1 n + shift0 ones n := by
  cases n with
  | zero => rfl
  | succ k => show 1 = 0 + 1; exact (Nat.zero_add 1).symm

/-- the values live in any type with an addition, a zero and right cancellation `x + y = y → x = 0`; additivity is
asked only where `a = b + c` term by term (no function extensionality: zero axioms) -/
theorem no_stable_additive_sum {G : Type} (add : G → G → G) (zero : G)
    (cancel : ∀ x y, add x y = y → x = zero)
    (D : (Nat → Nat) → Prop) (σ : (Nat → Nat) → G)
    (hshift : ∀ a, D a → D (shift0 a))
    (hadd : ∀ a b c, D a → D b → D c → (∀ n, a n = b n + c n) → σ a = add (σ b) (σ c))
    (hstable : ∀ a, D a → σ (shift0 a) = σ a)
    (hones : D ones) (he1D : D e1)
    (he1 : σ e1 ≠ zero) (hs : D nat1) : False := by
  have h1 : σ ones = zero := by
    have e := hadd nat1 ones (shift0 nat1) hs hones (hshift _ hs) nat1_split
    rw [hstable _ hs] at e
    exact cancel _ _ e.symm
  have h2 : σ e1 = zero := by
    have e := hadd ones e1 (shift0 ones) hones he1D (hshift _ hones) ones_split
    rw [hstable _ hones, h1] at e
    exact cancel _ _ e.symm
  exact he1 h2

end ZZeta

#print axioms ZZeta.bern_two
#print axioms ZZeta.zeta_neg_one
#print axioms ZZeta.S_ge
#print axioms ZZeta.partial_sums_unbounded
#print axioms ZZeta.not_limit_neg_twelfth
#print axioms ZZeta.nat1_split
#print axioms ZZeta.ones_split
#print axioms ZZeta.no_stable_additive_sum

-- SPDX-License-Identifier: Apache-2.0 OR MIT
-- Formalised in Lean by Claude (Anthropic, an AI model) under the curation of Vitaly Reznik, 2026-11-02.
/-!
# ZZetaBridge — a dirty atom's STABILITY = a summation method's INVARIANCE (zero axioms, Lean core)

The bridge between ZTL's notion and the analyst's (2026-11-02).

ZTL (ZDirty.lean): a dirty atom's occurrences are read each on its own; a verdict EARNED IF STABLE is true in every
COMPLETION — every assignment of ONE value to the atom at all its occurrences.
Analysis: a summation method σ is invariant under a transformation T of series (a leading zero, inserted zeros)
when σ (T a) = σ a.

The bridge: a derivation mentions "S" at occurrences i, and occurrence i DENOTES a transformed series T i a (the
series as written there: a itself, 0 + a, a with zeros inserted …). A method σ reads occurrence i as σ (T i a).
* `stable_iff_invariant` — the method's reading is a STABLE completion of the atom S (one value at all occurrences)
  if and only if σ is invariant under every transformation the derivation uses (relative to a reference occurrence).
* `leading_zero_forces` — if a derivation reads S also as 0 + S and the method is additive (where a = b + c term by
  term), stability forces σ (1 + 1 + 1 + …) = 0. The ζ-regularization gives 1 + 1 + 1 + … the value ζ(0) = −1/2,
  so it cannot make that S stable — the 0 + 1 + 2 + … = 5/12 of the brief (5/12 − (−1/12) = 1/2 = −ζ(0)).
* `not_stable_of_ones` — the contrapositive, the form the judge needs: an additive method with
  σ (1 + 1 + 1 + …) ≠ 0 cannot read S and 0 + S as one value.
A method stable under a leading zero on its WHOLE domain has no value on 1 + 2 + 3 + … at all: ZZeta.lean,
`no_stable_additive_sum`. The ZTL side here MIRRORS ZDirty's definitions (one value per atom at all its occurrences);
it does not import them (ZDirty's atoms are truth values, this atom is a number).
-/
namespace ZZetaBridge

/-! ## The ZTL side: occurrences, readings, stable completions -/

/-- a reading of an atom's k occurrences: a value at each (the dirty reading: each occurrence on its own) -/
def Reading (G : Type) (k : Nat) := Fin k → G

/-- a STABLE completion: one value at every occurrence (ZDirty's completion, for one atom) -/
def Stable {G : Type} {k : Nat} (ρ : Reading G k) : Prop := ∀ i j : Fin k, ρ i = ρ j

/-! ## The analyst's side: a method reads each occurrence's series -/

/-- the method σ's reading of the derivation whose occurrence i denotes the series `T i a` -/
def methodReading {G : Type} {k : Nat} (σ : (Nat → Nat) → G) (T : Fin k → (Nat → Nat) → (Nat → Nat))
    (a : Nat → Nat) : Reading G k :=
  fun i => σ (T i a)

/-- invariance of σ at `a` under every transformation of the derivation, relative to occurrence `r` -/
def Invariant {G : Type} {k : Nat} (σ : (Nat → Nat) → G) (T : Fin k → (Nat → Nat) → (Nat → Nat))
    (a : Nat → Nat) (r : Fin k) : Prop :=
  ∀ i, σ (T i a) = σ (T r a)

/-- THE BRIDGE: the method's reading is a stable completion iff σ is invariant under the derivation's
transformations -/
theorem stable_iff_invariant {G : Type} {k : Nat} (σ : (Nat → Nat) → G)
    (T : Fin k → (Nat → Nat) → (Nat → Nat)) (a : Nat → Nat) (r : Fin k) :
    Stable (methodReading σ T a) ↔ Invariant σ T a r :=
  ⟨fun h i => h i r, fun h i j => (h i).trans (h j).symm⟩

/-! ## The leading zero -/

def shift0 (a : Nat → Nat) : Nat → Nat
  | 0 => 0
  | n + 1 => a n

def nat1 : Nat → Nat := fun n => n + 1
def ones : Nat → Nat := fun _ => 1

theorem nat1_split (n : Nat) : nat1 n = ones n + shift0 nat1 n := by
  cases n with
  | zero => rfl
  | succ k => show k + 1 + 1 = 1 + (k + 1); exact Nat.add_comm (k + 1) 1

/-- a derivation reading "S" as S and as 0 + S: two occurrences, the identity and the leading zero -/
def idOrShift : Fin 2 → (Nat → Nat) → (Nat → Nat)
  | ⟨0, _⟩ => id
  | ⟨_ + 1, _⟩ => shift0

/-- if the method makes that S stable and is additive at (1, 2, 3, …) = (1, 1, 1, …) + (0, 1, 2, …), then it gives
1 + 1 + 1 + … the value 0 (values in any type with addition, zero and right cancellation) -/
theorem leading_zero_forces {G : Type} (add : G → G → G) (zero : G)
    (cancel : ∀ x y, add x y = y → x = zero) (σ : (Nat → Nat) → G)
    (hadd : σ nat1 = add (σ ones) (σ (shift0 nat1)))
    (hst : Stable (methodReading σ idOrShift nat1)) : σ ones = zero := by
  have hs : σ (shift0 nat1) = σ nat1 := (hst ⟨1, by decide⟩ ⟨0, by decide⟩)
  rw [hs] at hadd
  exact cancel _ _ hadd.symm

/-- contrapositive: an additive method with σ (1 + 1 + 1 + …) ≠ 0 (ζ: −1/2) cannot read S and 0 + S as one value -/
theorem not_stable_of_ones {G : Type} (add : G → G → G) (zero : G)
    (cancel : ∀ x y, add x y = y → x = zero) (σ : (Nat → Nat) → G)
    (hadd : σ nat1 = add (σ ones) (σ (shift0 nat1))) (hones : σ ones ≠ zero) :
    ¬ Stable (methodReading σ idOrShift nat1) :=
  fun hst => hones (leading_zero_forces add zero cancel σ hadd hst)

end ZZetaBridge

#print axioms ZZetaBridge.stable_iff_invariant
#print axioms ZZetaBridge.nat1_split
#print axioms ZZetaBridge.leading_zero_forces
#print axioms ZZetaBridge.not_stable_of_ones

The link to the zeta function needs Mathlib and rests on its classical axioms (propext, Classical.choice, Quot.sound); its #print axioms lines list them. It is in the separate repository ztl-classical (ZClassical/Zeta.lean):

import Mathlib.NumberTheory.LSeries.HurwitzZetaValues
import Mathlib.NumberTheory.Bernoulli
-- SPDX-License-Identifier: Apache-2.0 OR MIT
-- Formalised in Lean by Claude (Anthropic, an AI model) under the curation of Vitaly Reznik, 2026-11-02.
/-!
# ZClassical.Zeta — the CLASSICAL register: the analytic continuation's value at −1 is −1/12

Separate from ZTL's `ZZeta.lean` (zero axioms, Lean core, in the ZTL repository): this file rests on Mathlib's complex analysis and so on its
classical axioms (`#print axioms` below). It ties the finite operation of ZZeta (−B₂/2) to the function ζ.
-/

namespace ZClassical

theorem riemannZeta_neg_one : riemannZeta (-1) = -1 / 12 := by
  have h := riemannZeta_neg_nat_eq_bernoulli 1
  simp only [Nat.cast_one, pow_one] at h
  rw [h]
  norm_num

/-- ζ(0) = −1/2: the ζ-regularized value of 1 + 1 + 1 + …, so the ζ method cannot read S and 0 + S as one value
(ZZetaBridge.not_stable_of_ones); 0 + 1 + 2 + … gets ζ(−1) − ζ(0) = 5/12 -/
theorem riemannZeta_zero_val : riemannZeta 0 = -1 / 2 := riemannZeta_zero

theorem shifted_value : riemannZeta (-1) - riemannZeta 0 = 5 / 12 := by
  rw [riemannZeta_neg_one, riemannZeta_zero]; norm_num

end ZClassical

#print axioms ZClassical.riemannZeta_neg_one
#print axioms ZClassical.riemannZeta_zero_val
#print axioms ZClassical.shifted_value