The product of two finite complex partial sums equals the diagonal-grouped convolution plus a corner term, which the naive Cauchy identity omits

Identifier: F:finite-cauchy-product-over-complex-equals-triangle-plus-corner
Proof route: kernel-lean
External status: proved
Axiom footprint: Empty

Recorded description

For f, g : Nat -> Complex and any n, with F i j := f i * g j: (sum_{i<n} f i) * (sum_{j<n} g j) ~ TRIANGLE(F,n) + CORNER(F,n), where TRIANGLE is the antidiagonal sum sum_{k<n} sum_{i<=k} F i (k-i) and CORNER is sum_{i<n} sum_{j<i} F i ((n-i)+j), the sum over {(i,j) : i<n, j<n, i+j>=n}. Equivalence is Complex.Equiv, a DEFINED Prop relation on a setoid, never Eq. THIS EXISTS BECAUSE THE NAIVE FINITE CAUCHY IDENTITY IS FALSE. The claim (sum a)(sum b) = 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, being only the antidiagonal triangle, does not. This theorem is not a weaker replacement -- it names and quantifies the exact defect, and the CORNER at n = 2 is exactly the missing a_1*b_1. A NOTE ON `AxNat`, which appears throughout the formal statement: the `Ax` is `axeyum`, not `axiom`. `lean_pp` roots the kernel's CONSTRUCTED inductive naturals there only so exported terms do not shadow Lean's own `Nat`. It collides badly with `AxReal`, where `Ax` DOES mean axiomatized and the trusted surface is 30. Every prelude involved here -- nat, rat, creal, complex -- measures 0.

Formal statement

theorem Complex.sumRange_mul_eq_diag_add_corner : ((x0 : ((x0 : AxNat) -> Complex)) -> ((x1 : ((x1 : AxNat) -> Complex)) -> ((x2 : AxNat) -> Complex.Equiv (Complex.mul (Complex.sumRange x0 x2) (Complex.sumRange x1 x2)) (Complex.add (Complex.sumRange (fun (x3 : AxNat) => Complex.sumRange (fun (x4 : AxNat) => (fun (x5 : AxNat) => fun (x6 : AxNat) => Complex.mul (x0 x5) (x1 x6)) x4 (AxNat.sub x3 x4)) (AxNat.succ x3)) x2) (Complex.sumRange (fun (x3 : AxNat) => Complex.sumRange (fun (x4 : AxNat) => (fun (x5 : AxNat) => (fun (x6 : AxNat) => fun (x7 : AxNat) => Complex.mul (x0 x6) (x1 x7)) x3 x5) (AxNat.add (AxNat.sub x2 x3) x4)) x3) x2)))))

Dependencies

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

4 direct dependencies 0 direct dependents

Evidence

kernel-Complex.sumRange_mul_eq_diag_add_corner

Kind: kernel-term
Status: checked

Supports: `Complex.sumRange_mul_eq_diag_add_corner` is admitted with exactly the type in formal.statement. It composes `Complex.sumRange_mul_double[f,g,n,n]` -- which turns a product of partial sums into the RECTANGLE sum over {(i,j) : i<n, j<n} -- with `Complex.sumRange_rect_eq_diag_add_corner`, via Equiv.trans. The rectangle decomposition is itself the Equiv-port of Nat.sumRange_rect_eq_diag_add_corner, same induction structure. THE PORT IS NOT MECHANICAL: Complex.Equiv has no free single-sided congruence, so every rewrite under `add` needs an explicit add_congr paired with Equiv.refl on the untouched side, where over Nat it is just Eq and a rewrite chain.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib complex::complex_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: the theorem with the CORNER TERM DROPPED is precisely the refuted naive identity, and it would have an identically empty footprint. Mutation-verified by the establishing lane: a single-character mutation of the pinned constant took the suite from 10 passed to 9 passed / 1 failed, naming this test and no other; the file was then restored and hash-verified against the committed blob, and the suite returned to 10 passed. The command 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. Note that complex_tests.rs OVERFLOWS the default 2 MiB stack and aborts with SIGABRT; the suite runs bodies on a 64 MiB thread via its own on_a_deep_stack helper, so a SIGABRT here is an environment fact and not a proof failure.

footprint-complex-cauchy

Kind: kernel-term
Status: checked

Supports: axiom_footprint: [] for both Complex.sumRange_mul_eq_diag_add_corner and Complex.sumRange_rect_eq_diag_add_corner and everything beneath them. The `complex` prelude's trusted surface is 0: no Axiom, no Opaque, no Quotient. Both names were added to the complex sweep in the SAME edit that declared them.

Checker command

test "$(scripts/cargo-serialized.sh test -p axeyum-lean-kernel --lib complex::complex_tests::every_named_complex_declaration_is_checked_and_footprint_free -- --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. Counting Declaration::Axiom alone would also not suffice in this kernel, since Opaque has no proof body and Quotient admits Quot.sound; axiom_footprint covers all three.

Provenance

{
  "date": "2026-08-24",
  "established_by": "lane agent-capability-assurance (2026-08-24) across three dispatched lanes: one refuted the naive identity at n = 2, one built the Nat repair (Nat.sumRange_rect_eq_diag_add_corner plus the sub-free Nat.sumRange_split), and one ported both to Complex and composed with sumRange_mul_double. Kernel theorems over the constructed complex numbers, all with empty axiom_footprint.",
  "source": "classical",
  "prior_art": [
    {
      "who": "Augustin-Louis Cauchy",
      "what": "the Cauchy product of series",
      "year": 1821,
      "where": "Cours d'Analyse",
      "attribution": "standard attribution; this lane did not consult the primary source. Cauchy's theorem concerns INFINITE series under absolute convergence. The finite-partial-sum statement proved here is the elementary index-set decomposition underneath it, and the corner term is exactly what vanishes in the limit under Cauchy's hypotheses."
    }
  ]
}