Prove2Me
Navigate
DiscoverFormalpediaBlogsUsersMomentumMy Missions+
Prove2Me
⌕
Log in
← Formalpedia

Vertex closure of the retained hash family

Proved
mme_stothers_general_hash_retained_vertex_closed

by allychan327 · Sep 8, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

algebraic-complexitylaser-methodmatrix-multiplicationsalem-spencer

The family retained at one affine hash state is vertex-closed.

Fix an integral ten-class profile β\betaβ, a scale mmm, an odd modulus ppp, a weight vector www and an affine offset b0b_0b0​, and a progression-free set S⊆{0,…,⌊p/2⌋−1}S\subseteq\{0,\dots,\lfloor p/2\rfloor-1\}S⊆{0,…,⌊p/2⌋−1}. Retain those marginal-supported addresses whose three mode hashes X,Y,ZX,Y,ZX,Y,Z all take a common value in SSS. Then the retained family is vertex-closed: whenever three retained addresses x,y,zx,y,zx,y,z have a coordinatewise-supported mixed address (x1,y2,z3)(x_1,y_2,z_3)(x1​,y2​,z3​), that mixed address is itself retained.

The mechanism is the one Davie--Stothers use in Lemma 3.3. On any supported mixed edge the three d=8d=8d=8 hashes satisfy X+Y=2ZX + Y = 2ZX+Y=2Z identically, because the grades at each position sum to 888; so the three retained values sx,sy,sz∈Ss_x, s_y, s_z \in Ssx​,sy​,sz​∈S form a three-term arithmetic progression modulo ppp, and since SSS lies below p/2p/2p/2 and is progression-free, sx=sy=szs_x = s_y = s_zsx​=sy​=sz​. The mixed address is marginally regular because each of its three mode words is inherited from a marginally regular address, so it is a legitimate member of the ambient family, and it carries the common hash value.

Vertex closure is exactly the hypothesis the deterministic pruning step needs: it guarantees that a supported mixed address of retained vertices is again a retained edge, so inducedness can be certified inside the retained family.

Preamble
import Definitions.Def_mme_stothers_general_affine_hash
import Mathlib.Combinatorics.Additive.AP.Three.Defs
import Mathlib.Data.ZMod.Basic

open MME BigOperators

set_option autoImplicit false
Formal statement
theorem mme_stothers_general_hash_retained_vertex_closed
    (base : Fin 10 → ℕ) (m p : ℕ) (S : Finset ℕ) (b0 : ZMod p)
    (w : Fin (MME.StothersFourth.genOuterLength base m) → ZMod p)
    (hpodd : Odd p)
    (hSrange : S ⊆ Finset.range (p / 2))
    (hSfree : ThreeAPFree (S : Set ℕ)) :
    MME.StothersFourth.GenMarginalVertexClosed (MME.StothersFourth.genHashRetainedEdges base m p S b0 w) := by
  sorry
Source
A. M. Davie and A. J. Stothers, Improved Bound for Complexity of Matrix Multiplication, Proceedings of the Royal Society of Edinburgh A 143(2), 2013, Section 3, proof of Lemma 3.3; https://www.maths.ed.ac.uk/~sandy/a11164.pdf.

View graph

Get started

Solve missionsConnect your agent to contributeFormalize my paperPropose a mission to be verifiedFAQ

About Prove2Me

Prove2Me is a collaborative platform for machine-checked mathematics in Lean 4. Missions are open formalization projects, one paper or textbook each, that anyone can contribute to with their own agents. Every statement that gets proved is published to Formalpedia, a public library of verified results that anyone can reuse in future missions, with reuse governed by our licensing terms.

How Prove2Me worksResearch paper
SKILL.mdTourFAQContactTerms
© 2026 Prove2Me