# Lean-certified lower-memory schedule for a public rank-49 circuit

The public 49-product, 156-addition circuit for 4×4 matrix multiplication can
be executed in a different topological order with lower peak live-intermediate
counts in the stated scalar storage model.

| Circuit | Public order | Reordered |
| --- | ---: | ---: |
| Left linear map | 20 | 7 |
| Right linear map | 19 | 6 |
| Post-processing map | 17 | 8 |
| Complete 205-operation DAG | 80 | 38 |

The arithmetic is unchanged: 41 left additions, 41 right additions, 74 post
additions, and 49 coefficient products. The reordered algorithm satisfies all
4,096 Brent identities exactly.

The storage model excludes matrix inputs, caller-provided output slots,
instruction bytes, immutable coefficients, cache lines, SIMD packing, and
platform-specific spills. An intermediate remains live through its final use;
the consuming gate may overwrite it on that final use.

This is a fixed-DAG scheduling result. It does not improve tensor rank,
addition count, parallel depth, or the asymptotic arithmetic exponent. Caps of
6 and 5 were exhaustively ruled out for the fixed left and right DAGs,
respectively. No global optimality claim is made across different circuits.

`lean-certificates.tar.gz` contains the Lean sources, the pinned Lean
toolchain, the three reordered circuits, and the exact verification reports.
Its SHA-256 digest is
`8aab50ea9b0fb787211e10d637708b9412c5676fecdde1364598d468ede76755`.

The archive was rebuilt and checked on 2026-08-29 with Lean 4.30.0-rc2. An
independent exact Python replay confirmed the 156 additions, rank 49, 205
scalar operations, and all 4,096 Brent identities.

Related low-memory scheduling work includes the pebble-game and
Strassen–Winograd literature. The search performed for this record found no
published schedule at 38 or lower for this exact public DAG; that search is
not a formal novelty proof.