Lax Lean Archive

Explicit Subcubic Expanders and Linear Treewidth

lax-920634·formalized by Édouard Bonnet · Codex 6.1·registered·created ·GitHub @4e1ce66·Lean v4.33.0 epoch · mathlib db584cd6d46c

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this submission may be incorrect.

No flags have been submitted.

    Community review

    Flag this submission

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    Abstract

    We construct arbitrarily large subcubic expanders and deduce subcubic graphs of linear treewidth. The deterministic construction uses a fixed seed, zig-zag products, and path replacement. A uniform word-RAM algorithm outputs an NN-vertex member in O(N)O(N) time using O(log⁡(N+1))O(\log(N+1))-bit words. The fixed constants are enormous.

    Concepts

    Concept map
    22 concepts
    100%
    Proven claimDefinitionThis submissionOther submissionA → B: B builds on ADescendants are omitted for concepts with more than 10 descendants.

    Proofs

    Proof networkview on GitHub

    100%
    assumptions conclusionProven claimClaim from this submissionProof — open large view for details
    Proof list

    Lean sources for these proofs: proofs/ on GitHub

    Proof code is not displayed; the archive records each proof's checked relationship between claims.

    Related submissions

    Submission map

    100%
    This submissionOther submissionA → B: B's concepts build on AA → B: only B's proofs build on A

    Cite this

    This is only the formalizers. The authors of the formalized results may be different (see References).

    @misc{lax-920634,
  author = {Édouard Bonnet and Codex 6.1},
  title = {Explicit Subcubic Expanders and Linear Treewidth},
  year = {2026},
  howpublished = {Lax Archive, lax-920634},
  url = {https://laxarchive.org/lax-920634/},
}

    References

    1. Omer Reingold, Salil Vadhan and Avi Wigderson. Entropy waves, the zig-zag graph product, and new constant-degree expanders. Annals of Mathematics 155(1):157–187, 2002. doi:10.2307/3062153 · annals.math.princeton.edu/2002/155-1/p04
    2. Shlomo Hoory, Nathan Linial and Avi Wigderson. Expander graphs and their applications. Bulletin of the American Mathematical Society 43(4):439–561, 2006. math.ias.edu/~avi/PUBLICATIONS/MYPAPERS/HLW06/hlw06.pdf
    3. Lax323828: registered expander and polynomial-time computation development. 2026. Pinned revision 6902a04ba0c6ba68d1c390a410b2dbc5165cdfdb. github.com/EdouardBonnet/lax-253009/tree/6902a04ba0c6ba68d1c390a410b2dbc5165cdfdb
    4. Lax228581: registered tree-decomposition and treewidth definitions. 2026. Pinned revision 1e200ffac8b69e63b802f0aaf1dfee79561ca39a. github.com/lax-archive/lax-submissions/tree/1e200ffac8b69e63b802f0aaf1dfee79561ca39a/twin-width-treewidth-separation-v433
    5. Jan Dreier and Claude Fable 5. The Word RAM. 2026. Registered Lax808846; pinned revision 9394e531cc51cb67a0214bca3f9264dfe97ba5c7. laxarchive.org/lax-808846

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…