series.bend checks

raw source on the hub · import 0x4c3090ea8722081700f9d99ea7503e43/series.bend as Series

2 imports

import Base
import ./nat.bend as N

Laws

law tri_10 provedsource · line 52 · raw

{trisum(10n) == 55n : Nat}

Closed instances (definitional: the loops normalize on literals). tri(10) = 10*11/2 = 55.

law sq_5 provedsource · line 59 · raw

{sqsum(5n) == 55n : Nat}

sqsum(5) = 1+4+9+16+25 = 55 = 5*6*11/6.

law trisum_go_spec provedsource · line 69 · raw

@n:Nat -> @+acc:Nat -> {trisum_go(n, acc) == Nat.add(acc, trisum(n)) : Nat}

trisum_go_spec: the accumulator holds the partial sum. Proof is induction on n; the step chains the IH (at the extended accumulator) with N.add_assoc and the IH (at 1+p), mirroring nat.bend's mul_succ_r nesting.

law tri2_succ provedsource · line 97 · raw

@+p:Nat -> {tri2(1n+p) == Nat.add(tri2(p), Nat.add(1n+p, 1n+p)) : Nat}

tri2_succ (ATTEMPT 1): one-step growth of the doubled triangular number, tri2(1+p) == tri2(p) + 2*(1+p). Pure rewriting, no induction: distr + one + mul-unfold + succ + assoc + comm, nested like nat.bend mul_succ_r.

law tri_formula provedsource · line 170 · raw

@n:Nat -> {Nat.add(trisum(n), trisum(n)) == tri2(n) : Nat}

tri_formula (ATTEMPT 1): doubled triangular formula, by induction on n. Base is definitional (both sides unfold to 0n). Step chains the accumulator spec (both copies), N.add_shuffle, the IH, and tri2_succ.

law sqsum_go_spec provedsource · line 215 · raw

@n:Nat -> @+acc:Nat -> {sqsum_go(n, acc) == Nat.add(acc, sqsum(n)) : Nat}

sqsum_go_spec: the accumulator holds the partial square sum. Same shape as trisum_go_spec (only the accumulated term differs).

law sqW_grow provedsource · line 246 · raw

@+p:Nat -> {Nat.add(1n+p, Nat.add(1n+p, 1n)) == Nat.add(Nat.add(p, Nat.add(p, 1n)), 2n) : Nat}

sqW_grow (TRY 1 on the sq-formula track): split of the odd factor, (2(1+p)+1) == (2p+1)+2. Pure rewriting: unfold + succ + assoc + comm. Needed by the sq62 growth bridge (NOTE below on why the bridge itself is deferred).

law sq62_distr provedsource · line 293 · raw

@+p:Nat -> {sq62(1n+p) == Nat.add(Nat.mul(tri2(p), Nat.add(1n+p, Nat.add(1n+p, 1n))), Nat.mul(Nat.add(1n+p, 1n+p), Nat.add(1n+p, Nat.add(1n+p, 1n)))) : Nat}

sq62_distr (TRY 2 on the sq-formula track): distr skeleton of the sixfold-square growth, sq62(1+p) == tri2(p)*W + (2(1+p))*W where W = (2(1+p)+1). Nodes mirror the tri2_succ opening (tri2_succ cong + comm-flip + distr + double flip-back); all rewrites are syntactic.