A square double sum over the naturals splits exactly into the antidiagonal triangle plus the corner, which is the honest form of the finite Cauchy product

Identifier: F:finite-double-sum-rectangle-eq-triangle-plus-corner
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For any F : Nat -> Nat -> Nat and any n, the RECTANGLE sum over {(i,j) : i<n, j<n} equals the antidiagonal TRIANGLE sum over {(i,j) : i+j<n} plus the CORNER sum over {(i,j) : i<n, j<n, i+j>=n}. Concretely: sumRange (fun i => sumRange (fun j => F i j) n) n = add (sumRange (fun k => sumRange (fun i => F i (sub k i)) (succ k)) n) (sumRange (fun i => sumRange (fun k => F i (add (sub n i) k)) i) n). THIS EXISTS BECAUSE THE NAIVE FINITE CAUCHY IDENTITY IS FALSE. The claim (sum_{i<n} a_i)(sum_{j<n} b_j) = sum_{k<n} sum_{i<=k} a_i * b_{k-i} was dispatched as a target and REFUTED by hand at n = 2: the left side contains a_1*b_1 and the right side, being the antidiagonal triangle, does not. This theorem is not a weaker replacement -- it names and quantifies the exact defect. The triangle here is character-for-character the left-hand side of Nat.sumRange_diagonal, so the two compose: the diagonal lemma converts between antidiagonal and row-major views of the triangle, and this one relates the triangle to the rectangle that a product of partial sums actually is. Equality is Eq on Nat (the naturals are an inductive type here, not a setoid, so Eq is correct -- unlike CReal, where it never is). A NOTE ON `AxNat`, because the name is actively misleading: the `Ax` is `axeyum`, not `axiom`. `lean_pp` roots the kernel's COMPUTATIONAL (inductive, constructed) naturals at `AxNat` for one reason only -- so an exported term does not shadow Lean's own `Nat`. It collides badly with `AxReal`, where `Ax` DOES mean axiomatized and the trusted surface is 30. The `nat` prelude measures 0: no Axiom, no Opaque, no Quotient.

Formal statement

theorem Nat.sumRange_rect_eq_diag_add_corner : ((x0 : ((x0 : AxNat) -> ((x1 : AxNat) -> AxNat))) -> ((x1 : AxNat) -> Eq.{1} AxNat (AxNat.sumRange (fun (x2 : AxNat) => AxNat.sumRange (fun (x3 : AxNat) => x0 x2 x3) x1) x1) (AxNat.add (AxNat.sumRange (fun (x2 : AxNat) => AxNat.sumRange (fun (x3 : AxNat) => x0 x3 (AxNat.sub x2 x3)) (AxNat.succ x2)) x1) (AxNat.sumRange (fun (x2 : AxNat) => AxNat.sumRange (fun (x3 : AxNat) => (fun (x4 : AxNat) => x0 x2 x4) (AxNat.add (AxNat.sub x1 x2) x3)) x2) x1))))

Dependencies

The graph shows direct ledger edges. Follow a node to open its artifact page.

6 direct dependencies 1 direct dependents

Evidence

kernel-Nat.sumRange_rect_eq_diag_add_corner

Kind: kernel-term
Status: checked

Supports: `Nat.sumRange_rect_eq_diag_add_corner` is admitted with exactly the type in formal.statement. The proof splits every row via the companion `Nat.sumRange_split` at n = (n-i) + i (pointwise for i<n, lifted by `sumRange_congr_lt`), regroups via `sumRange_add`, then replaces the row-major half by the antidiagonal triangle via `Nat.sumRange_diagonal`. THE PARAMETRIZATION IS THE WHOLE DIFFICULTY: the corner summand is `add (sub n i) k` -- ONE truncated subtraction, never nested. The alternative reflection (i,j) |-> (n-1-i, n-1-j) needs nested `Nat.sub` and was rejected for that reason.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::the_rectangle_decomposition_is_stated_exactly -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

A footprint check cannot carry this claim: a theorem that DROPPED the corner term entirely -- i.e. the refuted naive identity -- has an identically empty footprint, as does one summing the triangle to `x2` instead of `succ x2`, which loses the whole antidiagonal. Mutation-verified 2026-08-24: rewriting the pinned corner shape `AxNat.add (AxNat.sub x1 x2) x3` to the nested `AxNat.add (AxNat.sub x1 (AxNat.sub x2 x3)) x3` makes cargo report `578 passed; 1 failed`, naming this test and no other; restored, 579/579 green. The command re-derives from source every run and is anchored on the exact `1 passed; 0 failed` count so an unmatched filter -- which prints `running 0 tests ... ok` and exits 0 -- cannot read as success.

kernel-Nat.sumRange_split

Kind: kernel-term
Status: checked

Supports: The companion `Nat.sumRange_split : forall f m j, sumRange f (add m j) = add (sumRange f m) (sumRange (fun k => f (add m k)) j)`. QUANTIFIED OVER THE SPLIT POINT AND THE TAIL LENGTH, with bound := m + j, NOT over a hypothesis m <= n. That is what keeps `Nat.sub` out of the induction on j entirely. CReal and Complex already had `sumRange_split` in this shape; Nat did not, and the precedent was found in `Rat.prob_complement`'s own private helper rather than invented.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::the_rectangle_decomposition_is_stated_exactly -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

The le-free/sub-free assertion is not decoration: both formulations are true theorems with empty footprints, and only the sub-free one supports an induction that never discharges a Le side condition. The distinction is invisible to any check that does not read the statement.

footprint-nat-rectangle

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] for both theorems and everything beneath them. The `nat` prelude's trusted surface is 0. Both names were added to `theorem_names()` in the SAME edit that declared them, moving the pinned count 26 + 161 -> 26 + 163.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib nat_prelude::nat_prelude_tests::the_nat_prelude_declares_no_axioms -- --exact 2>&1 | grep -Ec 'test result: ok\. 1 passed; 0 failed')" -ge 1

Evidence notes

Presence matters as much as the footprint: axiom_footprint of a name interned but never DECLARED is vacuously empty. A lane found five pre-existing declarations missing from another prelude's sweep on the same day, so registration in theorem_names() is the load-bearing half and `the_build_is_deterministic`'s pinned count is what makes an omission fail rather than pass quietly.

Provenance

{
  "date": "2026-08-24",
  "established_by": "lane agent-capability-assurance (2026-08-24), dispatched after the naive finite Cauchy identity was REFUTED by a prior lane at n = 2. Kernel theorems over the constructed inductive naturals, both with empty axiom_footprint. Statement pin and its mutation control added by the coordinating lane.",
  "source": "classical",
  "prior_art": [
    {
      "who": "standard",
      "what": "the decomposition of a square index set into the antidiagonal triangle and its complement",
      "year": null,
      "where": "folklore; the substance is the Cauchy-product rearrangement argument",
      "attribution": "This is elementary and is not claimed as new. What is recorded here is that the CORNER is named and quantified rather than dropped, which is exactly what the refuted target got wrong."
    }
  ]
}