{"license": "CC BY 4.0", "license_url": "https://creativecommons.org/licenses/by/4.0/", "bounds": [{"id": 21, "name": "The recursive bound", "direction": "upper", "scope": "general", "n": null, "value": null, "n0": 1, "formula_latex": "1! + 2! + \\cdots + n!", "formula": null, "formula_note": null, "coefficient": "1", "target_values": [], "values": {}, "superseded": false, "credited": [{"name": "Daniel A. Ashlock", "github_username": null}, {"name": "Jenett Tillotson", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "1993-01-01", "announced_precision": "year", "source_url": "https://www.zbmath.org/?q=an:0801.05004", "notes": null, "proof": "paper", "check_level": "none", "historical": true, "evidence": [{"kind": "paper", "url": "https://www.zbmath.org/?q=an:0801.05004", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Ashlock and Tillotson, 'Construction of small superpermutations and minimal injective superstrings', Congressus Numerantium 93 (1993) 91-98", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "paper", "url": "https://doi.org/10.1080/00029890.2021.1835384", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Engen and Vatter, Amer. Math. Monthly 128 (2021), Proposition 2.2, citing Ashlock and Tillotson, Theorem 3 and Lemma 5", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}]}, {"id": 3, "name": "The 4chan bound", "direction": "lower", "scope": "general", "n": null, "value": null, "n0": 2, "formula_latex": "n! + (n-1)! + (n-2)! + n - 3", "formula": "factorial(n) + factorial(n-1) + factorial(n-2) + n - 3", "formula_note": null, "coefficient": "0", "target_values": [], "values": {"3": 9, "4": 33, "5": 152, "6": 867, "7": 5884, "8": 46085, "9": 408246, "10": 4032007, "11": 43908488, "12": 522547209, "13": 6745939210, "14": 93884313611}, "superseded": false, "credited": [{"name": "Anonymous 4chan poster", "github_username": null}, {"name": "Robin Houston", "github_username": null}, {"name": "Jay Pantone", "github_username": "jaypantone"}, {"name": "Vince Vatter", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2011-09-17", "announced_precision": "day", "source_url": "https://warosu.org/sci/thread/S3751105#p3751197", "notes": null, "proof": "paper", "check_level": "none", "historical": true, "evidence": [{"kind": "preprint", "url": "https://oeis.org/A180632/a180632.pdf", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Anonymous 4chan Poster, Houston, Pantone, Vatter, 'A lower bound on the length of the shortest superpattern', October 25, 2018, hosted at OEIS", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "paper", "url": "https://doi.org/10.1080/00029890.2021.1835384", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Engen and Vatter, 'Containing All Permutations', Amer. Math. Monthly 128 (2021) 4-24, Theorem 2.5 (arXiv:1810.08252)", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "certificate", "url": "https://github.com/ccd0/superpermutations", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Coq formalization of the argument (2015–2018)", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}]}, {"id": 10, "name": "Exhaustive search", "direction": "lower", "scope": "single", "n": 5, "value": 153, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"5": 153}, "superseded": false, "credited": [{"name": "Ben Chaffin", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2014-08-13", "announced_precision": "day", "source_url": "https://njohnston.ca/2014/08/all-minimal-superpermutations-on-five-symbols-have-been-found/", "notes": null, "proof": "certificate", "check_level": "none", "historical": true, "evidence": [{"kind": "certificate", "url": "https://arxiv.org/abs/1408.5108", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Houston's arXiv paper (2014-08-21) reports that Concorde solved the five-symbol instance exactly, 'confirming Chaffin's recent result'; an independent computer check", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}]}, {"id": 22, "name": "The recursive bound minus one", "direction": "upper", "scope": "general", "n": null, "value": null, "n0": 6, "formula_latex": "1! + 2! + \\cdots + n! - 1", "formula": null, "formula_note": null, "coefficient": "1", "target_values": [], "values": {}, "superseded": false, "credited": [{"name": "Robin Houston", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2014-08-21", "announced_precision": "day", "source_url": "https://arxiv.org/abs/1408.5108", "notes": null, "proof": "paper", "check_level": "none", "historical": true, "evidence": [{"kind": "preprint", "url": "https://arxiv.org/abs/1408.5108", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Houston, 'Tackling the minimal superpermutation problem', arXiv v1 2014-08-21", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "paper", "url": "https://doi.org/10.1080/00029890.2021.1835384", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Engen and Vatter, after Theorem 2.3: 'the bound of n! + ... + 3! + 2! implied by Houston's construction and Proposition 2.2'", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}]}, {"id": 23, "name": "Egan's bound", "direction": "upper", "scope": "general", "n": null, "value": null, "n0": 4, "formula_latex": "n! + (n-1)! + (n-2)! + (n-3)! + n - 3", "formula": "factorial(n) + factorial(n-1) + factorial(n-2) + factorial(n-3) + n - 3", "formula_note": null, "coefficient": "1", "target_values": [], "values": {"4": 34, "5": 154, "6": 873, "7": 5908, "8": 46205, "9": 408966, "10": 4037047, "11": 43948808, "12": 522910089, "13": 6749568010, "14": 93924230411}, "superseded": false, "credited": [{"name": "Greg Egan", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": "Egan's construction adapts Aaron Williams's Hamiltonian-cycle construction.", "announced": "2018-10-20", "announced_precision": "day", "source_url": "https://www.gregegan.net/SCIENCE/Superpermutations/Superpermutations.html", "notes": null, "proof": "paper", "check_level": "none", "historical": true, "evidence": [{"kind": "paper", "url": "https://doi.org/10.1080/00029890.2021.1835384", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Engen and Vatter, Amer. Math. Monthly 128 (2021), Theorem 2.3, 'for all n >= 4'", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}]}, {"id": 4, "name": "4chan + 1", "direction": "lower", "scope": "general", "n": null, "value": null, "n0": 5, "formula_latex": "n! + (n-1)! + (n-2)! + n - 2", "formula": "factorial(n) + factorial(n-1) + factorial(n-2) + n - 2", "formula_note": null, "coefficient": "0", "target_values": [], "values": {"5": 153, "6": 868, "7": 5885, "8": 46086, "9": 408247, "10": 4032008, "11": 43908489, "12": 522547210, "13": 6745939211, "14": 93884313612}, "superseded": false, "credited": [{"name": "Robin Houston", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": "Improves the 4chan bound (Anonymous, Houston, Pantone and Vatter) by one.", "announced": "2018-11-02", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/MFtWmIDgvPM/m/TYX1M4xYAwAJ", "notes": null, "proof": "lean", "check_level": "none", "historical": true, "evidence": [{"kind": "paper", "url": "https://doi.org/10.1080/00029890.2021.1835384", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Engen and Vatter (2021), after Theorem 2.5: 'Houston has shown (in the Superpermutators group) that the bound in Theorem 2.5 can be increased by 1'; stated, not reproved", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/urdvr/superperm-coeff2", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "12acadf0069dd4098a6cacec2dff21b6c8096a18", "palomar_id": null, "note": "Raudvere's Lean theorem Coeff2.intromain (2026-07-18) gives S(n) ≥ HPV(n) + ⌈((n−3)! − 1)/(2n − 1)⌉ for n ≥ 5, which is at least this bound; the k = 0 case of its criterion is this bound", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}]}, {"id": 5, "name": "Raudvere's bound", "direction": "lower", "scope": "general", "n": null, "value": null, "n0": 5, "formula_latex": "n! + (n-1)! + (n-2)! + n - 3 + \\left\\lceil \\frac{(n-3)! - 1}{2n-1} \\right\\rceil", "formula": "factorial(n) + factorial(n-1) + factorial(n-2) + n - 3 + ceil((factorial(n-3) - 1) / (2*n - 1))", "formula_note": null, "coefficient": "0", "target_values": [], "values": {"5": 153, "6": 868, "7": 5886, "8": 46093, "9": 408289, "10": 4032273, "11": 43910408, "12": 522562987, "13": 6746084362, "14": 93885792011}, "superseded": false, "credited": [{"name": "Uku Raudvere", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-07-18", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/9fCyufH4jdo/m/cDwI1XWkAgAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/urdvr/superperm-coeff2", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "12acadf0069dd4098a6cacec2dff21b6c8096a18", "palomar_id": null, "note": "Lean 4 formalization and PDF; Miles Gould confirmed it compiles with only the standard axioms (2026-07-23)", "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 6, "name": "The Hunter–Raudvere bound", "direction": "lower", "scope": "general", "n": null, "value": null, "n0": 3, "formula_latex": "n! + (n-1)! + (n-2)! + n - 3 + \\frac{(n-2)! - (n-2)}{n^2 - 3n + 1}", "formula": "factorial(n) + factorial(n-1) + factorial(n-2) + n - 3 + (factorial(n-2) - (n-2)) / (n*n - 3*n + 1)", "formula_note": null, "coefficient": "0", "target_values": [], "values": {"3": 9, "4": 33, "5": 153, "6": 869, "7": 5888, "8": 46103, "9": 408338, "10": 4032575, "11": 43912566, "12": 522580501, "13": 6746243919, "14": 93887403944}, "superseded": false, "credited": [{"name": "Zach Hunter", "github_username": null}, {"name": "Uku Raudvere", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-07-28", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/Uo2-KjoDYbg/m/L3QMbE5SBQAJ", "notes": null, "proof": "lean", "check_level": "reviewed", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/urdvr/superpermutations-hunter", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "d45222190031d162feb1f6f3cf5fe2d11fab726d", "palomar_id": null, "note": "Lean 4 formalization and paper 'A New Lower Bound for Superpermutations' by Zach Hunter and Uku Raudvere; no native_decide", "checked_by": null, "checked_on": null, "check_level": "reviewed", "claim": null, "paper": []}]}, {"id": 24, "name": "Egan's bound minus one", "direction": "upper", "scope": "general", "n": null, "value": null, "n0": 8, "formula_latex": "n! + (n-1)! + (n-2)! + (n-3)! + n - 4", "formula": "factorial(n) + factorial(n-1) + factorial(n-2) + factorial(n-3) + n - 4", "formula_note": null, "coefficient": "1", "target_values": [], "values": {"8": 46204, "9": 408965, "10": 4037046, "11": 43948807, "12": 522910088, "13": 6749568009, "14": 93924230410}, "superseded": false, "credited": [{"name": "Uku Raudvere", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-07-28", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/TBZsctlczM4/m/95le-pxTBQAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/urdvr/superpermutation-examples/tree/62958c6268f728828ed578a171486866b6fe4b20/formal", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "62958c6268f728828ed578a171486866b6fe4b20", "palomar_id": null, "note": "Lean: for all n >= 8 a superpermutation of length E(n) - 1 exists, by a certificate lift from the 46204 word; no sorry or native_decide", "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 11, "name": "S(6) ≥ 872", "direction": "lower", "scope": "single", "n": 6, "value": 872, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"6": 872}, "superseded": false, "credited": [{"name": "Benjamin Grayzel", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-07-29", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/Lv_XD077uNI/m/l3Q7wj7uBQAJ", "notes": null, "proof": "lean", "check_level": "native", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/BGray-wrl/superperm6", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "d8a932d8f61d80b0bcfc737bd0e235a8300449c4", "palomar_id": null, "note": "end-to-end Lean 4 proof that s(6) = 872, uses native_decide; Grayzel reports a two-person audit of the statement (2026-08-14)", "checked_by": null, "checked_on": null, "check_level": "native", "claim": null, "paper": []}, {"kind": "preprint", "url": "https://github.com/BGray-wrl/superperm6/blob/main/paper/superperm6.pdf", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "18-page write-up generated against the Lean proof", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}]}, {"id": 8, "name": "Liu's bound", "direction": "lower", "scope": "general", "n": null, "value": null, "n0": 5, "formula_latex": "H_n + \\Gamma_n", "formula": null, "formula_note": "Hₙ is the Hunter–Raudvere bound. Γₙ is the least layer passing Liu's test, found for each n; his paper shows Γₙ = (1 − 3/n + O(1/n²))(n − 4)!.", "coefficient": "0", "target_values": [], "values": {"5": 153, "6": 869, "7": 5892, "8": 46118, "9": 408418, "10": 4033080, "11": 43916235, "12": 522610764, "13": 6746523219, "14": 93890256441}, "superseded": false, "credited": [{"name": "Xiaolong Liu", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-08-10", "announced_precision": "day", "source_url": "https://github.com/Haruhiyuki/superpermutations-preimage-chain-lower-bounds", "notes": null, "proof": "lean", "check_level": "reviewed", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/Haruhiyuki/superpermutations-preimage-chain-lower-bounds", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "a3852f0de2d84b99cc65d4c281e86892b5f6e911", "palomar_id": null, "note": "Lean 4.31.0 on the Hunter-Raudvere library; release commit a3852f0, published 2026-08-10 (repository created 10:10 UTC); theorem superperm_new_bound_closed", "checked_by": null, "checked_on": null, "check_level": "reviewed", "claim": null, "paper": []}]}, {"id": 12, "name": "S(7) ≥ 5,898", "direction": "lower", "scope": "single", "n": 7, "value": 5898, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"7": 5898}, "superseded": false, "credited": [{"name": "Justin Lebar", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-08-13", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/zNthLnbbfi8/m/7F_gtS6yAAAJ", "notes": null, "proof": "lean", "check_level": "native", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jlebar/superperm7-ge-5898", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "f516e19b232079947027698c1447009f929ed28c", "palomar_id": null, "note": "Superperm7.main_theorem; branch-and-bound over trails with 380 certificates via native_decide; generated with an unreleased Claude model; builds on Grayzel's superperm6", "checked_by": null, "checked_on": null, "check_level": "native", "claim": null, "paper": []}]}, {"id": 13, "name": "S(8) ≥ 46,130", "direction": "lower", "scope": "single", "n": 8, "value": 46130, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"8": 46130}, "superseded": true, "credited": [{"name": "William Echols", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-09-04", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/1HY91Fdwr3o/m/JiT8OHndAgAJ", "notes": null, "proof": "lean", "check_level": "native", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/williamechols/superperm8-ge-46130", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "893ab2d92669ea56d012ceca626bf01ca631e920", "palomar_id": null, "note": "Lean proof generated by GPT-6 Astra (Extra High effort), building on Lebar and Grayzel; uses native_decide", "checked_by": null, "checked_on": null, "check_level": "native", "claim": null, "paper": []}]}, {"id": 25, "name": "The 101/120 bound", "direction": "upper", "scope": "general", "n": null, "value": null, "n0": 8, "formula_latex": "n! + (n-1)! + (n-2)! + \\tfrac{101}{120}(n-3)!", "formula": "factorial(n) + factorial(n-1) + factorial(n-2) + 101 * factorial(n-3) / 120", "formula_note": null, "coefficient": "101/120", "target_values": [], "values": {"8": 46181, "9": 408846, "10": 4036242, "11": 43942416, "12": 522852624, "13": 6748993440, "14": 93917910240}, "superseded": false, "credited": [{"name": "Jay Pantone", "github_username": "jaypantone"}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-09-29", "announced_precision": "day", "source_url": "https://github.com/jaypantone/superperm-upper-43-80/blob/c8fb7ffdd69be1375580710ae11b47a295b1f0f6/README.md", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jaypantone/superperm-upper-43-80", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "c8fb7ffdd69be1375580710ae11b47a295b1f0f6", "palomar_id": null, "note": "'earlier uniform bound' proved in the repository's Lean library", "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 26, "name": "The 3/5 bound", "direction": "upper", "scope": "general", "n": null, "value": null, "n0": 10, "formula_latex": "n! + (n-1)! + (n-2)! + \\tfrac{3}{5}(n-3)!", "formula": "factorial(n) + factorial(n-1) + factorial(n-2) + 3 * factorial(n-3) / 5", "formula_note": null, "coefficient": "3/5", "target_values": [], "values": {"10": 4035024, "11": 43932672, "12": 522764928, "13": 6748116480, "14": 93908263680}, "superseded": false, "credited": [{"name": "Jay Pantone", "github_username": "jaypantone"}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-09-29", "announced_precision": "day", "source_url": "https://github.com/jaypantone/superperm-upper-43-80/blob/c8fb7ffdd69be1375580710ae11b47a295b1f0f6/README.md", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jaypantone/superperm-upper-43-80", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "c8fb7ffdd69be1375580710ae11b47a295b1f0f6", "palomar_id": null, "note": "'earlier uniform bound' proved in the repository's Lean library", "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 27, "name": "The 43/80 bound", "direction": "upper", "scope": "general", "n": null, "value": null, "n0": null, "formula_latex": "n! + (n-1)! + (n-2)! + \\left(\\tfrac{43}{80} + o(1)\\right)(n-3)!", "formula": null, "formula_note": null, "coefficient": "43/80", "target_values": [], "values": {}, "superseded": false, "credited": [{"name": "Jay Pantone", "github_username": "jaypantone"}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-09-29", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/X-68bMLHARc/m/6gbP9rlaEQAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jaypantone/superperm-upper-43-80", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "c8fb7ffdd69be1375580710ae11b47a295b1f0f6", "palomar_id": null, "note": "Lean proof of the main theorem and of an explicit finite bound for every K >= 11 (computed by tools/finite_bound.py)", "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 7, "name": "Kisic's bound", "direction": "lower", "scope": "general", "n": null, "value": null, "n0": 5, "formula_latex": "n! + (n-1)! + (n-2)! + n - 3 + \\left\\lceil \\frac{2((n-2)! - (n-2))}{n(n-3)} \\right\\rceil", "formula": "factorial(n) + factorial(n-1) + factorial(n-2) + n - 3 + ceil(2*(factorial(n-2) - (n-2)) / (n*(n-3)))", "formula_note": null, "coefficient": "0", "target_values": [], "values": {"5": 153, "6": 870, "7": 5893, "8": 46121, "9": 408433, "10": 4033159, "11": 43916736, "12": 522614409, "13": 6746553315, "14": 93890534411}, "superseded": false, "credited": [{"name": "Marin Kisic", "github_username": null}, {"name": "Jakub Halfar", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": "Posted by Kisic as unverified (2026-08-07); proved in Lean by Halfar (2026-10-06).", "announced": "2026-10-06", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/6ozhk3faHDA/m/mu7tukD6AQAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "preprint", "url": "https://github.com/mkisic/superpermutations", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "lower_bound_unverified.pdf, produced with GPT 5.6 Sol Pro; posted by Kisic as unverified", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditA.lean", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Theorem A, proved in Lean by Jakub Halfar on 2026-10-06 (no native_decide)", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "cc5c763bd5854317b20dadb138990802656e6f03", "palomar_id": null, "note": null, "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 9, "name": "Halfar's general bound", "direction": "lower", "scope": "general", "n": null, "value": null, "n0": 7, "formula_latex": "n! + (n-1)! + (n-2)! + n - 3 + \\left\\lceil \\frac{2((n-2)! - (n-2))}{n^2 - 4n + 1} \\right\\rceil", "formula": "factorial(n) + factorial(n-1) + factorial(n-2) + n - 3 + ceil(2*(factorial(n-2) - (n-2)) / (n*n - 4*n + 1))", "formula_note": null, "coefficient": "0", "target_values": [], "values": {"7": 5895, "8": 46129, "9": 408465, "10": 4033329, "11": 43917793, "12": 522622030, "13": 6746615766, "14": 93891107960}, "superseded": false, "credited": [{"name": "Jakub Halfar", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-06", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/6ozhk3faHDA/m/mu7tukD6AQAJ", "notes": null, "proof": "lean", "check_level": "reviewed", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditB.lean", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Theorem B, on Liu's library; no native_decide; Lean files first pushed 2026-10-06 20:48 UTC", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "cc5c763bd5854317b20dadb138990802656e6f03", "palomar_id": null, "note": null, "checked_by": null, "checked_on": null, "check_level": "reviewed", "claim": null, "paper": []}]}, {"id": 14, "name": "S(8) ≥ 46,133", "direction": "lower", "scope": "single", "n": 8, "value": 46133, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"8": 46133}, "superseded": false, "credited": [{"name": "Jakub Halfar", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-06", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/6ozhk3faHDA/m/mu7tukD6AQAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditCFinal.lean", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Theorem C: kernel-checked finite search (827,022 states at n = 8), no native_decide", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "cc5c763bd5854317b20dadb138990802656e6f03", "palomar_id": null, "note": null, "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 15, "name": "S(9) ≥ 408,469", "direction": "lower", "scope": "single", "n": 9, "value": 408469, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"9": 408469}, "superseded": false, "credited": [{"name": "Jakub Halfar", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-06", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/6ozhk3faHDA/m/mu7tukD6AQAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditCFinal.lean", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Theorem C with a kernel-checked finite search", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "cc5c763bd5854317b20dadb138990802656e6f03", "palomar_id": null, "note": null, "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 16, "name": "S(10) ≥ 4,033,378", "direction": "lower", "scope": "single", "n": 10, "value": 4033378, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"10": 4033378}, "superseded": true, "credited": [{"name": "Jakub Halfar", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-06", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/6ozhk3faHDA/m/mu7tukD6AQAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditCFinal.lean", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Theorem C with a kernel-checked finite search", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "cc5c763bd5854317b20dadb138990802656e6f03", "palomar_id": null, "note": null, "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 17, "name": "S(11) ≥ 43,917,903", "direction": "lower", "scope": "single", "n": 11, "value": 43917903, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"11": 43917903}, "superseded": false, "credited": [{"name": "Jakub Halfar", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-06", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/6ozhk3faHDA/m/mu7tukD6AQAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditCFinal.lean", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Theorem C with a kernel-checked finite search", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "cc5c763bd5854317b20dadb138990802656e6f03", "palomar_id": null, "note": null, "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 18, "name": "S(12) ≥ 522,622,378", "direction": "lower", "scope": "single", "n": 12, "value": 522622378, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"12": 522622378}, "superseded": true, "credited": [{"name": "Jakub Halfar", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-06", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/6ozhk3faHDA/m/mu7tukD6AQAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditCFinal.lean", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Theorem C with a kernel-checked finite search", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "cc5c763bd5854317b20dadb138990802656e6f03", "palomar_id": null, "note": null, "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 19, "name": "S(13) ≥ 6,746,626,957", "direction": "lower", "scope": "single", "n": 13, "value": 6746626957, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"13": 6746626957}, "superseded": false, "credited": [{"name": "Jakub Halfar", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-06", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/6ozhk3faHDA/m/mu7tukD6AQAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditCFinal.lean", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Theorem C with a kernel-checked finite search", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "cc5c763bd5854317b20dadb138990802656e6f03", "palomar_id": null, "note": null, "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 20, "name": "S(14) ≥ 93,891,141,008", "direction": "lower", "scope": "single", "n": 14, "value": 93891141008, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"14": 93891141008}, "superseded": true, "credited": [{"name": "Jakub Halfar", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-06", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/6ozhk3faHDA/m/mu7tukD6AQAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/blob/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower/AuditCFinal.lean", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "Theorem C with a kernel-checked finite search", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/lower", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "cc5c763bd5854317b20dadb138990802656e6f03", "palomar_id": null, "note": null, "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 28, "name": "The 1771/3456 bound", "direction": "upper", "scope": "general", "n": null, "value": null, "n0": null, "formula_latex": "n! + (n-1)! + (n-2)! + \\left(\\tfrac{1771}{3456} + o(1)\\right)(n-3)!", "formula": null, "formula_note": null, "coefficient": "1771/3456", "target_values": [], "values": {}, "superseded": false, "credited": [{"name": "Jakub Halfar", "github_username": null}], "credits_pending": false, "attribution_pending": [], "credit_note": "Applies Pantone's 43/80 construction and Lean library with a new selection.", "announced": "2026-10-06", "announced_precision": "day", "source_url": "https://groups.google.com/g/superpermutators/c/6ozhk3faHDA/m/mu7tukD6AQAJ", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": null, "palomar_id": null, "note": "constant/: Pantone's argument with a new selection; no native_decide; finite version from n = 13", "checked_by": null, "checked_on": null, "check_level": "none", "claim": null, "paper": []}, {"kind": "lean", "url": "https://github.com/jhalfar/superpermutations/tree/cc5c763bd5854317b20dadb138990802656e6f03/proofs/lean/constant", "doi": null, "arxiv_id": null, "repository": null, "commit_sha": "cc5c763bd5854317b20dadb138990802656e6f03", "palomar_id": null, "note": null, "checked_by": null, "checked_on": null, "check_level": "kernel", "claim": null, "paper": []}]}, {"id": 29, "name": "The 926683/1814400 bound", "direction": "upper", "scope": "general", "n": null, "value": null, "n0": null, "formula_latex": "n! + (n-1)! + (n-2)! + \\left(926683/1814400 + \\varepsilon\\right)(n-3)!", "formula": null, "formula_note": null, "coefficient": "926683/1814400", "target_values": [], "values": {}, "superseded": false, "credited": [{"name": "Jay Pantone", "github_username": "jaypantone"}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-28", "announced_precision": "day", "source_url": "https://github.com/jaypantone/2026-10-superpermutation-upper-palomar/blob/d771f355ab604950ceb417346764707952e0b9e7/AlmanacSolution.lean#L9-L10", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": null, "doi": null, "arxiv_id": null, "repository": "https://github.com/jaypantone/2026-10-superpermutation-upper-palomar", "commit_sha": "d771f355ab604950ceb417346764707952e0b9e7", "palomar_id": null, "note": null, "checked_by": null, "checked_on": "2026-10-29", "check_level": "kernel", "claim": {"submission": "L-0014", "ordinal": 1, "name": "asymptotic_upper", "lean_name": ["AlmanacSubmission", "asymptotic_upper"], "classification": "template", "template": "asymptotic_upper", "source_url": "https://github.com/jaypantone/2026-10-superpermutation-upper-palomar/blob/d771f355ab604950ceb417346764707952e0b9e7/AlmanacSolution.lean#L9-L10"}, "paper": [{"name": "upper/upper-bounds.pdf", "path": "paper/upper/upper-bounds.pdf", "size": 281148, "sha256": "1811f372636ea886a507f217b8a8df8d506fae5bbec911d4ec3c0d7642c5ccf7", "media_type": "application/pdf", "url": "https://superpermutations.com/lean/L-0014/paper/upper/upper-bounds.pdf", "text_url": null}, {"name": "upper/upper-bounds.tex", "path": "paper/upper/upper-bounds.tex", "size": 30341, "sha256": "eb6e26b74f29f3701c1ed6f3c34651c60d441a18c64925eac521d85b5b29cb33", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0014/paper/upper/upper-bounds.tex", "text_url": "https://superpermutations.com/lean/L-0014/paper-text/upper/upper-bounds.tex"}]}]}, {"id": 30, "name": "S(10) ≥ 4,033,379", "direction": "lower", "scope": "single", "n": 10, "value": 4033379, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"10": 4033379}, "superseded": false, "credited": [{"name": "Jay Pantone", "github_username": "jaypantone"}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-29", "announced_precision": "day", "source_url": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar/blob/ad72ab5010e945b5c8768a918281778c834dcc40/AlmanacSolution.lean#L13", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": null, "doi": null, "arxiv_id": null, "repository": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar", "commit_sha": "ad72ab5010e945b5c8768a918281778c834dcc40", "palomar_id": null, "note": null, "checked_by": null, "checked_on": "2026-10-29", "check_level": "kernel", "claim": {"submission": "L-0015", "ordinal": 2, "name": "lower10", "lean_name": ["AlmanacSubmission", "lower10"], "classification": "template", "template": "lower_at", "source_url": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar/blob/ad72ab5010e945b5c8768a918281778c834dcc40/AlmanacSolution.lean#L13"}, "paper": [{"name": "finite/finite-lower-bounds.pdf", "path": "paper/finite/finite-lower-bounds.pdf", "size": 278626, "sha256": "7042e5293edc3cdaff0470fcb38c4cd01d79a07e349065d62c05b08b32ca8024", "media_type": "application/pdf", "url": "https://superpermutations.com/lean/L-0015/paper/finite/finite-lower-bounds.pdf", "text_url": null}, {"name": "lower/lower-bounds.pdf", "path": "paper/lower/lower-bounds.pdf", "size": 399492, "sha256": "3c8c7114dec14794d2fd4260cb8bf8274f73fbf3327cdd033a9da47d3d235737", "media_type": "application/pdf", "url": "https://superpermutations.com/lean/L-0015/paper/lower/lower-bounds.pdf", "text_url": null}, {"name": "finite/finite-lower-bounds.tex", "path": "paper/finite/finite-lower-bounds.tex", "size": 25106, "sha256": "41b3f2d1f5ad454a0faf6e68da9dc3923c16eb3a9b96597b9225f0b55b8d74f8", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/finite/finite-lower-bounds.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/finite/finite-lower-bounds.tex"}, {"name": "lower/alternation.tex", "path": "paper/lower/alternation.tex", "size": 7510, "sha256": "53d4213ad7fe9894aa35422352a2e4ccfc3653e94cd731c4ab22300fa0411ca9", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/alternation.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/alternation.tex"}, {"name": "lower/bound-statement.tex", "path": "paper/lower/bound-statement.tex", "size": 651, "sha256": "a93b424afccefc4933a7e19b0dfebcf2e6afa1724d3b63f772bddc37a19433c5", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/bound-statement.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/bound-statement.tex"}, {"name": "lower/consequences.tex", "path": "paper/lower/consequences.tex", "size": 6424, "sha256": "6f4dc5d1f9de03e58150381a45a628e8e7c3d96070a3b2e83bb38cffb567cbe4", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/consequences.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/consequences.tex"}, {"name": "lower/cycle-calculation.tex", "path": "paper/lower/cycle-calculation.tex", "size": 3470, "sha256": "bd39af63b13aad005d3d98fbd5b4577154f7ae5ba90de4ee87dddc0e8c07785a", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/cycle-calculation.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/cycle-calculation.tex"}, {"name": "lower/forest-assembly.tex", "path": "paper/lower/forest-assembly.tex", "size": 7362, "sha256": "8907261f6e0787c001b41c2e1e6690005d5ddb2e6aadefa9e84feca14e3031ad", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/forest-assembly.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/forest-assembly.tex"}, {"name": "lower/formalization.tex", "path": "paper/lower/formalization.tex", "size": 3112, "sha256": "48371af32e026632c21818038a970a693bdf2a2adef5941a7c027fa747936613", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/formalization.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/formalization.tex"}, {"name": "lower/full-run-collision.tex", "path": "paper/lower/full-run-collision.tex", "size": 2262, "sha256": "156a6220d525a2ec2c232d05f57a72d5ef3a25b681017c272a42c937dfac3c1f", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/full-run-collision.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/full-run-collision.tex"}, {"name": "lower/introduction.tex", "path": "paper/lower/introduction.tex", "size": 4436, "sha256": "3041dad9961a1f2f9dc2266e0c0280bd70de7fdfb21dbcdb845b78c7586b4acb", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/introduction.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/introduction.tex"}, {"name": "lower/lower-bounds.tex", "path": "paper/lower/lower-bounds.tex", "size": 1247, "sha256": "d2ff485000a7a068a4b150a40e53b832be63c04bd7a02d20a1b0aa51e3ade6de", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/lower-bounds.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/lower-bounds.tex"}, {"name": "lower/numerical-details.tex", "path": "paper/lower/numerical-details.tex", "size": 3219, "sha256": "92e8a834c15ba556b2c90d38ce6abc32cf5ff653c60c6c53a9852b0f303575d2", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/numerical-details.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/numerical-details.tex"}, {"name": "lower/overlaps-and-chains.tex", "path": "paper/lower/overlaps-and-chains.tex", "size": 12641, "sha256": "e93c5477eeae0e2618b270d119ed342335f880b0a5fc1c45e11ed89d7f72dd56", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/overlaps-and-chains.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/overlaps-and-chains.tex"}, {"name": "lower/paid-pairs.tex", "path": "paper/lower/paid-pairs.tex", "size": 9561, "sha256": "1758c83a3c3575558f8b1123f29a1d4a4d07dc1217a53efbcd23a53b58c15ea9", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/paid-pairs.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/paid-pairs.tex"}, {"name": "lower/references.tex", "path": "paper/lower/references.tex", "size": 1277, "sha256": "9db35040ab2be0686725d23a09af08d90255094babb29ac8c8c965524c04fe33", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/references.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/references.tex"}, {"name": "lower/scalar-conversion.tex", "path": "paper/lower/scalar-conversion.tex", "size": 3609, "sha256": "5c19b2156b28d1928243fe8c6a3ccb780a85eaa49dbda544622a11039c971fc0", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/scalar-conversion.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/scalar-conversion.tex"}, {"name": "lower/transfer-proof.tex", "path": "paper/lower/transfer-proof.tex", "size": 817, "sha256": "1288fbb2e2a7b01f3c2493eefbc18032c7cacdc830429cc0b8d33854724cd21e", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/transfer-proof.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/transfer-proof.tex"}, {"name": "lower/transfer-statement.tex", "path": "paper/lower/transfer-statement.tex", "size": 248, "sha256": "57895e6f188d4fbde543d5e726d302c42d4bc8480b7e99c4939235b2e07ba931", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/transfer-statement.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/transfer-statement.tex"}]}]}, {"id": 31, "name": "S(12) ≥ 522,622,380", "direction": "lower", "scope": "single", "n": 12, "value": 522622380, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"12": 522622380}, "superseded": false, "credited": [{"name": "Jay Pantone", "github_username": "jaypantone"}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-29", "announced_precision": "day", "source_url": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar/blob/ad72ab5010e945b5c8768a918281778c834dcc40/AlmanacSolution.lean#L16", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": null, "doi": null, "arxiv_id": null, "repository": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar", "commit_sha": "ad72ab5010e945b5c8768a918281778c834dcc40", "palomar_id": null, "note": null, "checked_by": null, "checked_on": "2026-10-29", "check_level": "kernel", "claim": {"submission": "L-0015", "ordinal": 3, "name": "lower12", "lean_name": ["AlmanacSubmission", "lower12"], "classification": "template", "template": "lower_at", "source_url": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar/blob/ad72ab5010e945b5c8768a918281778c834dcc40/AlmanacSolution.lean#L16"}, "paper": [{"name": "finite/finite-lower-bounds.pdf", "path": "paper/finite/finite-lower-bounds.pdf", "size": 278626, "sha256": "7042e5293edc3cdaff0470fcb38c4cd01d79a07e349065d62c05b08b32ca8024", "media_type": "application/pdf", "url": "https://superpermutations.com/lean/L-0015/paper/finite/finite-lower-bounds.pdf", "text_url": null}, {"name": "lower/lower-bounds.pdf", "path": "paper/lower/lower-bounds.pdf", "size": 399492, "sha256": "3c8c7114dec14794d2fd4260cb8bf8274f73fbf3327cdd033a9da47d3d235737", "media_type": "application/pdf", "url": "https://superpermutations.com/lean/L-0015/paper/lower/lower-bounds.pdf", "text_url": null}, {"name": "finite/finite-lower-bounds.tex", "path": "paper/finite/finite-lower-bounds.tex", "size": 25106, "sha256": "41b3f2d1f5ad454a0faf6e68da9dc3923c16eb3a9b96597b9225f0b55b8d74f8", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/finite/finite-lower-bounds.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/finite/finite-lower-bounds.tex"}, {"name": "lower/alternation.tex", "path": "paper/lower/alternation.tex", "size": 7510, "sha256": "53d4213ad7fe9894aa35422352a2e4ccfc3653e94cd731c4ab22300fa0411ca9", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/alternation.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/alternation.tex"}, {"name": "lower/bound-statement.tex", "path": "paper/lower/bound-statement.tex", "size": 651, "sha256": "a93b424afccefc4933a7e19b0dfebcf2e6afa1724d3b63f772bddc37a19433c5", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/bound-statement.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/bound-statement.tex"}, {"name": "lower/consequences.tex", "path": "paper/lower/consequences.tex", "size": 6424, "sha256": "6f4dc5d1f9de03e58150381a45a628e8e7c3d96070a3b2e83bb38cffb567cbe4", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/consequences.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/consequences.tex"}, {"name": "lower/cycle-calculation.tex", "path": "paper/lower/cycle-calculation.tex", "size": 3470, "sha256": "bd39af63b13aad005d3d98fbd5b4577154f7ae5ba90de4ee87dddc0e8c07785a", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/cycle-calculation.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/cycle-calculation.tex"}, {"name": "lower/forest-assembly.tex", "path": "paper/lower/forest-assembly.tex", "size": 7362, "sha256": "8907261f6e0787c001b41c2e1e6690005d5ddb2e6aadefa9e84feca14e3031ad", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/forest-assembly.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/forest-assembly.tex"}, {"name": "lower/formalization.tex", "path": "paper/lower/formalization.tex", "size": 3112, "sha256": "48371af32e026632c21818038a970a693bdf2a2adef5941a7c027fa747936613", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/formalization.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/formalization.tex"}, {"name": "lower/full-run-collision.tex", "path": "paper/lower/full-run-collision.tex", "size": 2262, "sha256": "156a6220d525a2ec2c232d05f57a72d5ef3a25b681017c272a42c937dfac3c1f", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/full-run-collision.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/full-run-collision.tex"}, {"name": "lower/introduction.tex", "path": "paper/lower/introduction.tex", "size": 4436, "sha256": "3041dad9961a1f2f9dc2266e0c0280bd70de7fdfb21dbcdb845b78c7586b4acb", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/introduction.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/introduction.tex"}, {"name": "lower/lower-bounds.tex", "path": "paper/lower/lower-bounds.tex", "size": 1247, "sha256": "d2ff485000a7a068a4b150a40e53b832be63c04bd7a02d20a1b0aa51e3ade6de", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/lower-bounds.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/lower-bounds.tex"}, {"name": "lower/numerical-details.tex", "path": "paper/lower/numerical-details.tex", "size": 3219, "sha256": "92e8a834c15ba556b2c90d38ce6abc32cf5ff653c60c6c53a9852b0f303575d2", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/numerical-details.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/numerical-details.tex"}, {"name": "lower/overlaps-and-chains.tex", "path": "paper/lower/overlaps-and-chains.tex", "size": 12641, "sha256": "e93c5477eeae0e2618b270d119ed342335f880b0a5fc1c45e11ed89d7f72dd56", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/overlaps-and-chains.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/overlaps-and-chains.tex"}, {"name": "lower/paid-pairs.tex", "path": "paper/lower/paid-pairs.tex", "size": 9561, "sha256": "1758c83a3c3575558f8b1123f29a1d4a4d07dc1217a53efbcd23a53b58c15ea9", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/paid-pairs.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/paid-pairs.tex"}, {"name": "lower/references.tex", "path": "paper/lower/references.tex", "size": 1277, "sha256": "9db35040ab2be0686725d23a09af08d90255094babb29ac8c8c965524c04fe33", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/references.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/references.tex"}, {"name": "lower/scalar-conversion.tex", "path": "paper/lower/scalar-conversion.tex", "size": 3609, "sha256": "5c19b2156b28d1928243fe8c6a3ccb780a85eaa49dbda544622a11039c971fc0", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/scalar-conversion.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/scalar-conversion.tex"}, {"name": "lower/transfer-proof.tex", "path": "paper/lower/transfer-proof.tex", "size": 817, "sha256": "1288fbb2e2a7b01f3c2493eefbc18032c7cacdc830429cc0b8d33854724cd21e", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/transfer-proof.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/transfer-proof.tex"}, {"name": "lower/transfer-statement.tex", "path": "paper/lower/transfer-statement.tex", "size": 248, "sha256": "57895e6f188d4fbde543d5e726d302c42d4bc8480b7e99c4939235b2e07ba931", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/transfer-statement.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/transfer-statement.tex"}]}]}, {"id": 32, "name": "S(14) ≥ 93,891,141,150", "direction": "lower", "scope": "single", "n": 14, "value": 93891141150, "n0": null, "formula_latex": null, "formula": null, "formula_note": null, "coefficient": null, "target_values": [], "values": {"14": 93891141150}, "superseded": false, "credited": [{"name": "Jay Pantone", "github_username": "jaypantone"}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-29", "announced_precision": "day", "source_url": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar/blob/ad72ab5010e945b5c8768a918281778c834dcc40/AlmanacSolution.lean#L19", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": null, "doi": null, "arxiv_id": null, "repository": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar", "commit_sha": "ad72ab5010e945b5c8768a918281778c834dcc40", "palomar_id": null, "note": null, "checked_by": null, "checked_on": "2026-10-29", "check_level": "kernel", "claim": {"submission": "L-0015", "ordinal": 4, "name": "lower14", "lean_name": ["AlmanacSubmission", "lower14"], "classification": "template", "template": "lower_at", "source_url": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar/blob/ad72ab5010e945b5c8768a918281778c834dcc40/AlmanacSolution.lean#L19"}, "paper": [{"name": "finite/finite-lower-bounds.pdf", "path": "paper/finite/finite-lower-bounds.pdf", "size": 278626, "sha256": "7042e5293edc3cdaff0470fcb38c4cd01d79a07e349065d62c05b08b32ca8024", "media_type": "application/pdf", "url": "https://superpermutations.com/lean/L-0015/paper/finite/finite-lower-bounds.pdf", "text_url": null}, {"name": "lower/lower-bounds.pdf", "path": "paper/lower/lower-bounds.pdf", "size": 399492, "sha256": "3c8c7114dec14794d2fd4260cb8bf8274f73fbf3327cdd033a9da47d3d235737", "media_type": "application/pdf", "url": "https://superpermutations.com/lean/L-0015/paper/lower/lower-bounds.pdf", "text_url": null}, {"name": "finite/finite-lower-bounds.tex", "path": "paper/finite/finite-lower-bounds.tex", "size": 25106, "sha256": "41b3f2d1f5ad454a0faf6e68da9dc3923c16eb3a9b96597b9225f0b55b8d74f8", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/finite/finite-lower-bounds.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/finite/finite-lower-bounds.tex"}, {"name": "lower/alternation.tex", "path": "paper/lower/alternation.tex", "size": 7510, "sha256": "53d4213ad7fe9894aa35422352a2e4ccfc3653e94cd731c4ab22300fa0411ca9", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/alternation.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/alternation.tex"}, {"name": "lower/bound-statement.tex", "path": "paper/lower/bound-statement.tex", "size": 651, "sha256": "a93b424afccefc4933a7e19b0dfebcf2e6afa1724d3b63f772bddc37a19433c5", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/bound-statement.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/bound-statement.tex"}, {"name": "lower/consequences.tex", "path": "paper/lower/consequences.tex", "size": 6424, "sha256": "6f4dc5d1f9de03e58150381a45a628e8e7c3d96070a3b2e83bb38cffb567cbe4", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/consequences.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/consequences.tex"}, {"name": "lower/cycle-calculation.tex", "path": "paper/lower/cycle-calculation.tex", "size": 3470, "sha256": "bd39af63b13aad005d3d98fbd5b4577154f7ae5ba90de4ee87dddc0e8c07785a", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/cycle-calculation.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/cycle-calculation.tex"}, {"name": "lower/forest-assembly.tex", "path": "paper/lower/forest-assembly.tex", "size": 7362, "sha256": "8907261f6e0787c001b41c2e1e6690005d5ddb2e6aadefa9e84feca14e3031ad", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/forest-assembly.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/forest-assembly.tex"}, {"name": "lower/formalization.tex", "path": "paper/lower/formalization.tex", "size": 3112, "sha256": "48371af32e026632c21818038a970a693bdf2a2adef5941a7c027fa747936613", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/formalization.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/formalization.tex"}, {"name": "lower/full-run-collision.tex", "path": "paper/lower/full-run-collision.tex", "size": 2262, "sha256": "156a6220d525a2ec2c232d05f57a72d5ef3a25b681017c272a42c937dfac3c1f", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/full-run-collision.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/full-run-collision.tex"}, {"name": "lower/introduction.tex", "path": "paper/lower/introduction.tex", "size": 4436, "sha256": "3041dad9961a1f2f9dc2266e0c0280bd70de7fdfb21dbcdb845b78c7586b4acb", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/introduction.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/introduction.tex"}, {"name": "lower/lower-bounds.tex", "path": "paper/lower/lower-bounds.tex", "size": 1247, "sha256": "d2ff485000a7a068a4b150a40e53b832be63c04bd7a02d20a1b0aa51e3ade6de", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/lower-bounds.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/lower-bounds.tex"}, {"name": "lower/numerical-details.tex", "path": "paper/lower/numerical-details.tex", "size": 3219, "sha256": "92e8a834c15ba556b2c90d38ce6abc32cf5ff653c60c6c53a9852b0f303575d2", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/numerical-details.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/numerical-details.tex"}, {"name": "lower/overlaps-and-chains.tex", "path": "paper/lower/overlaps-and-chains.tex", "size": 12641, "sha256": "e93c5477eeae0e2618b270d119ed342335f880b0a5fc1c45e11ed89d7f72dd56", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/overlaps-and-chains.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/overlaps-and-chains.tex"}, {"name": "lower/paid-pairs.tex", "path": "paper/lower/paid-pairs.tex", "size": 9561, "sha256": "1758c83a3c3575558f8b1123f29a1d4a4d07dc1217a53efbcd23a53b58c15ea9", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/paid-pairs.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/paid-pairs.tex"}, {"name": "lower/references.tex", "path": "paper/lower/references.tex", "size": 1277, "sha256": "9db35040ab2be0686725d23a09af08d90255094babb29ac8c8c965524c04fe33", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/references.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/references.tex"}, {"name": "lower/scalar-conversion.tex", "path": "paper/lower/scalar-conversion.tex", "size": 3609, "sha256": "5c19b2156b28d1928243fe8c6a3ccb780a85eaa49dbda544622a11039c971fc0", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/scalar-conversion.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/scalar-conversion.tex"}, {"name": "lower/transfer-proof.tex", "path": "paper/lower/transfer-proof.tex", "size": 817, "sha256": "1288fbb2e2a7b01f3c2493eefbc18032c7cacdc830429cc0b8d33854724cd21e", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/transfer-proof.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/transfer-proof.tex"}, {"name": "lower/transfer-statement.tex", "path": "paper/lower/transfer-statement.tex", "size": 248, "sha256": "57895e6f188d4fbde543d5e726d302c42d4bc8480b7e99c4939235b2e07ba931", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/transfer-statement.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/transfer-statement.tex"}]}]}, {"id": 33, "name": "Jay Pantone's bound", "direction": "lower", "scope": "general", "n": null, "value": null, "n0": null, "formula_latex": "n! + (n-1)! + (n-2)! + \\left(2 - \\varepsilon\\right)(n-4)!", "formula": null, "formula_note": null, "coefficient": null, "target_values": [{"target": "c4", "side": "lower", "value": "2", "mode": "asymptotic", "basis": "claim"}], "values": {}, "superseded": false, "credited": [{"name": "Jay Pantone", "github_username": "jaypantone"}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-29", "announced_precision": "day", "source_url": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar/blob/ad72ab5010e945b5c8768a918281778c834dcc40/AlmanacSolution.lean#L22-L23", "notes": null, "proof": "lean", "check_level": "kernel", "historical": false, "evidence": [{"kind": "lean", "url": null, "doi": null, "arxiv_id": null, "repository": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar", "commit_sha": "ad72ab5010e945b5c8768a918281778c834dcc40", "palomar_id": null, "note": null, "checked_by": null, "checked_on": "2026-10-29", "check_level": "kernel", "claim": {"submission": "L-0015", "ordinal": 5, "name": "asymptotic_lower_four", "lean_name": ["AlmanacSubmission", "asymptotic_lower_four"], "classification": "template", "template": "asymptotic_lower_at", "source_url": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar/blob/ad72ab5010e945b5c8768a918281778c834dcc40/AlmanacSolution.lean#L22-L23"}, "paper": [{"name": "finite/finite-lower-bounds.pdf", "path": "paper/finite/finite-lower-bounds.pdf", "size": 278626, "sha256": "7042e5293edc3cdaff0470fcb38c4cd01d79a07e349065d62c05b08b32ca8024", "media_type": "application/pdf", "url": "https://superpermutations.com/lean/L-0015/paper/finite/finite-lower-bounds.pdf", "text_url": null}, {"name": "lower/lower-bounds.pdf", "path": "paper/lower/lower-bounds.pdf", "size": 399492, "sha256": "3c8c7114dec14794d2fd4260cb8bf8274f73fbf3327cdd033a9da47d3d235737", "media_type": "application/pdf", "url": "https://superpermutations.com/lean/L-0015/paper/lower/lower-bounds.pdf", "text_url": null}, {"name": "finite/finite-lower-bounds.tex", "path": "paper/finite/finite-lower-bounds.tex", "size": 25106, "sha256": "41b3f2d1f5ad454a0faf6e68da9dc3923c16eb3a9b96597b9225f0b55b8d74f8", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/finite/finite-lower-bounds.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/finite/finite-lower-bounds.tex"}, {"name": "lower/alternation.tex", "path": "paper/lower/alternation.tex", "size": 7510, "sha256": "53d4213ad7fe9894aa35422352a2e4ccfc3653e94cd731c4ab22300fa0411ca9", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/alternation.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/alternation.tex"}, {"name": "lower/bound-statement.tex", "path": "paper/lower/bound-statement.tex", "size": 651, "sha256": "a93b424afccefc4933a7e19b0dfebcf2e6afa1724d3b63f772bddc37a19433c5", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/bound-statement.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/bound-statement.tex"}, {"name": "lower/consequences.tex", "path": "paper/lower/consequences.tex", "size": 6424, "sha256": "6f4dc5d1f9de03e58150381a45a628e8e7c3d96070a3b2e83bb38cffb567cbe4", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/consequences.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/consequences.tex"}, {"name": "lower/cycle-calculation.tex", "path": "paper/lower/cycle-calculation.tex", "size": 3470, "sha256": "bd39af63b13aad005d3d98fbd5b4577154f7ae5ba90de4ee87dddc0e8c07785a", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/cycle-calculation.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/cycle-calculation.tex"}, {"name": "lower/forest-assembly.tex", "path": "paper/lower/forest-assembly.tex", "size": 7362, "sha256": "8907261f6e0787c001b41c2e1e6690005d5ddb2e6aadefa9e84feca14e3031ad", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/forest-assembly.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/forest-assembly.tex"}, {"name": "lower/formalization.tex", "path": "paper/lower/formalization.tex", "size": 3112, "sha256": "48371af32e026632c21818038a970a693bdf2a2adef5941a7c027fa747936613", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/formalization.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/formalization.tex"}, {"name": "lower/full-run-collision.tex", "path": "paper/lower/full-run-collision.tex", "size": 2262, "sha256": "156a6220d525a2ec2c232d05f57a72d5ef3a25b681017c272a42c937dfac3c1f", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/full-run-collision.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/full-run-collision.tex"}, {"name": "lower/introduction.tex", "path": "paper/lower/introduction.tex", "size": 4436, "sha256": "3041dad9961a1f2f9dc2266e0c0280bd70de7fdfb21dbcdb845b78c7586b4acb", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/introduction.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/introduction.tex"}, {"name": "lower/lower-bounds.tex", "path": "paper/lower/lower-bounds.tex", "size": 1247, "sha256": "d2ff485000a7a068a4b150a40e53b832be63c04bd7a02d20a1b0aa51e3ade6de", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/lower-bounds.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/lower-bounds.tex"}, {"name": "lower/numerical-details.tex", "path": "paper/lower/numerical-details.tex", "size": 3219, "sha256": "92e8a834c15ba556b2c90d38ce6abc32cf5ff653c60c6c53a9852b0f303575d2", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/numerical-details.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/numerical-details.tex"}, {"name": "lower/overlaps-and-chains.tex", "path": "paper/lower/overlaps-and-chains.tex", "size": 12641, "sha256": "e93c5477eeae0e2618b270d119ed342335f880b0a5fc1c45e11ed89d7f72dd56", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/overlaps-and-chains.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/overlaps-and-chains.tex"}, {"name": "lower/paid-pairs.tex", "path": "paper/lower/paid-pairs.tex", "size": 9561, "sha256": "1758c83a3c3575558f8b1123f29a1d4a4d07dc1217a53efbcd23a53b58c15ea9", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/paid-pairs.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/paid-pairs.tex"}, {"name": "lower/references.tex", "path": "paper/lower/references.tex", "size": 1277, "sha256": "9db35040ab2be0686725d23a09af08d90255094babb29ac8c8c965524c04fe33", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/references.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/references.tex"}, {"name": "lower/scalar-conversion.tex", "path": "paper/lower/scalar-conversion.tex", "size": 3609, "sha256": "5c19b2156b28d1928243fe8c6a3ccb780a85eaa49dbda544622a11039c971fc0", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/scalar-conversion.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/scalar-conversion.tex"}, {"name": "lower/transfer-proof.tex", "path": "paper/lower/transfer-proof.tex", "size": 817, "sha256": "1288fbb2e2a7b01f3c2493eefbc18032c7cacdc830429cc0b8d33854724cd21e", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/transfer-proof.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/transfer-proof.tex"}, {"name": "lower/transfer-statement.tex", "path": "paper/lower/transfer-statement.tex", "size": 248, "sha256": "57895e6f188d4fbde543d5e726d302c42d4bc8480b7e99c4939235b2e07ba931", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/transfer-statement.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/transfer-statement.tex"}]}]}, {"id": 34, "name": "Pantone's bound", "direction": "lower", "scope": "general", "n": null, "value": null, "n0": 8, "formula_latex": "n! + (n-1)! + (n-2)! + n - 3 + \\left\\lceil \\frac{2(n-2)! - 2(n-2) - 4p_n/t_n}{n^2 - 4n + 1 - 2(n-1)/t_n} \\right\\rceil", "formula": null, "formula_note": "For n = 8 to 12, (pₙ, tₙ) = (10, 46/3), (15, 287/12), (521/80, 359/40), (21, 263/12), (28, 195/4). For n ≥ 13, write n − 1 = 3m + r. If r = 0, (pₙ, tₙ) = (2m + 1/2 + 1/(4R₀), 4m − 3 − 1/(2R₀)); if r = 1, (m(2m + 1), 2m² + 2m − 2 − 1/R₁); if r = 2, ((m + 1)(2m + 1), 4m² + 5m − 5/2). R₀ = 2(n − 1)/7 if 7 divides n − 1, else u(n − 1 − u) with 7u ≡ 1 mod n − 1. R₁ is an LCM of cycle lengths set by m mod 6 (see the paper).", "coefficient": "0", "target_values": [], "values": {"8": 46130, "9": 408469, "10": 4033374, "11": 43917903, "12": 522622380, "13": 6746626531, "14": 93891141149}, "superseded": false, "credited": [{"name": "Jay Pantone", "github_username": "jaypantone"}], "credits_pending": false, "attribution_pending": [], "credit_note": null, "announced": "2026-10-29", "announced_precision": "day", "source_url": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar/blob/ad72ab5010e945b5c8768a918281778c834dcc40/AlmanacSolution.lean#L10", "notes": null, "proof": "lean", "check_level": "reviewed", "historical": false, "evidence": [{"kind": "lean", "url": null, "doi": null, "arxiv_id": null, "repository": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar", "commit_sha": "ad72ab5010e945b5c8768a918281778c834dcc40", "palomar_id": null, "note": null, "checked_by": null, "checked_on": "2026-10-29", "check_level": "reviewed", "claim": {"submission": "L-0015", "ordinal": 1, "name": "general_lower", "lean_name": ["AlmanacSubmission", "general_lower"], "classification": "custom", "template": null, "source_url": "https://github.com/jaypantone/2026-10-superpermutation-lower-palomar/blob/ad72ab5010e945b5c8768a918281778c834dcc40/AlmanacSolution.lean#L10"}, "paper": [{"name": "finite/finite-lower-bounds.pdf", "path": "paper/finite/finite-lower-bounds.pdf", "size": 278626, "sha256": "7042e5293edc3cdaff0470fcb38c4cd01d79a07e349065d62c05b08b32ca8024", "media_type": "application/pdf", "url": "https://superpermutations.com/lean/L-0015/paper/finite/finite-lower-bounds.pdf", "text_url": null}, {"name": "lower/lower-bounds.pdf", "path": "paper/lower/lower-bounds.pdf", "size": 399492, "sha256": "3c8c7114dec14794d2fd4260cb8bf8274f73fbf3327cdd033a9da47d3d235737", "media_type": "application/pdf", "url": "https://superpermutations.com/lean/L-0015/paper/lower/lower-bounds.pdf", "text_url": null}, {"name": "finite/finite-lower-bounds.tex", "path": "paper/finite/finite-lower-bounds.tex", "size": 25106, "sha256": "41b3f2d1f5ad454a0faf6e68da9dc3923c16eb3a9b96597b9225f0b55b8d74f8", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/finite/finite-lower-bounds.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/finite/finite-lower-bounds.tex"}, {"name": "lower/alternation.tex", "path": "paper/lower/alternation.tex", "size": 7510, "sha256": "53d4213ad7fe9894aa35422352a2e4ccfc3653e94cd731c4ab22300fa0411ca9", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/alternation.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/alternation.tex"}, {"name": "lower/bound-statement.tex", "path": "paper/lower/bound-statement.tex", "size": 651, "sha256": "a93b424afccefc4933a7e19b0dfebcf2e6afa1724d3b63f772bddc37a19433c5", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/bound-statement.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/bound-statement.tex"}, {"name": "lower/consequences.tex", "path": "paper/lower/consequences.tex", "size": 6424, "sha256": "6f4dc5d1f9de03e58150381a45a628e8e7c3d96070a3b2e83bb38cffb567cbe4", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/consequences.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/consequences.tex"}, {"name": "lower/cycle-calculation.tex", "path": "paper/lower/cycle-calculation.tex", "size": 3470, "sha256": "bd39af63b13aad005d3d98fbd5b4577154f7ae5ba90de4ee87dddc0e8c07785a", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/cycle-calculation.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/cycle-calculation.tex"}, {"name": "lower/forest-assembly.tex", "path": "paper/lower/forest-assembly.tex", "size": 7362, "sha256": "8907261f6e0787c001b41c2e1e6690005d5ddb2e6aadefa9e84feca14e3031ad", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/forest-assembly.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/forest-assembly.tex"}, {"name": "lower/formalization.tex", "path": "paper/lower/formalization.tex", "size": 3112, "sha256": "48371af32e026632c21818038a970a693bdf2a2adef5941a7c027fa747936613", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/formalization.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/formalization.tex"}, {"name": "lower/full-run-collision.tex", "path": "paper/lower/full-run-collision.tex", "size": 2262, "sha256": "156a6220d525a2ec2c232d05f57a72d5ef3a25b681017c272a42c937dfac3c1f", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/full-run-collision.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/full-run-collision.tex"}, {"name": "lower/introduction.tex", "path": "paper/lower/introduction.tex", "size": 4436, "sha256": "3041dad9961a1f2f9dc2266e0c0280bd70de7fdfb21dbcdb845b78c7586b4acb", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/introduction.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/introduction.tex"}, {"name": "lower/lower-bounds.tex", "path": "paper/lower/lower-bounds.tex", "size": 1247, "sha256": "d2ff485000a7a068a4b150a40e53b832be63c04bd7a02d20a1b0aa51e3ade6de", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/lower-bounds.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/lower-bounds.tex"}, {"name": "lower/numerical-details.tex", "path": "paper/lower/numerical-details.tex", "size": 3219, "sha256": "92e8a834c15ba556b2c90d38ce6abc32cf5ff653c60c6c53a9852b0f303575d2", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/numerical-details.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/numerical-details.tex"}, {"name": "lower/overlaps-and-chains.tex", "path": "paper/lower/overlaps-and-chains.tex", "size": 12641, "sha256": "e93c5477eeae0e2618b270d119ed342335f880b0a5fc1c45e11ed89d7f72dd56", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/overlaps-and-chains.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/overlaps-and-chains.tex"}, {"name": "lower/paid-pairs.tex", "path": "paper/lower/paid-pairs.tex", "size": 9561, "sha256": "1758c83a3c3575558f8b1123f29a1d4a4d07dc1217a53efbcd23a53b58c15ea9", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/paid-pairs.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/paid-pairs.tex"}, {"name": "lower/references.tex", "path": "paper/lower/references.tex", "size": 1277, "sha256": "9db35040ab2be0686725d23a09af08d90255094babb29ac8c8c965524c04fe33", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/references.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/references.tex"}, {"name": "lower/scalar-conversion.tex", "path": "paper/lower/scalar-conversion.tex", "size": 3609, "sha256": "5c19b2156b28d1928243fe8c6a3ccb780a85eaa49dbda544622a11039c971fc0", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/scalar-conversion.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/scalar-conversion.tex"}, {"name": "lower/transfer-proof.tex", "path": "paper/lower/transfer-proof.tex", "size": 817, "sha256": "1288fbb2e2a7b01f3c2493eefbc18032c7cacdc830429cc0b8d33854724cd21e", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/transfer-proof.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/transfer-proof.tex"}, {"name": "lower/transfer-statement.tex", "path": "paper/lower/transfer-statement.tex", "size": 248, "sha256": "57895e6f188d4fbde543d5e726d302c42d4bc8480b7e99c4939235b2e07ba931", "media_type": "text/plain; charset=utf-8", "url": "https://superpermutations.com/lean/L-0015/paper/lower/transfer-statement.tex", "text_url": "https://superpermutations.com/lean/L-0015/paper-text/lower/transfer-statement.tex"}]}]}]}