% --- Hexagon deposit: the five pgfplots data files of release v1.4.4 (paper/figdata/*.dat), embedded verbatim % --- because Hexagon accepts only TeX project files. Written to the working directory at compile time. \begin{filecontents*}[overwrite]{race_s3.dat} n d 304 4926.4442 315 4635.1904 326 4363.0667 337 4108.2466 348 3869.1293 359 3644.3057 370 3432.5304 381 3232.6987 392 3043.8274 403 2865.0383 414 2695.5447 425 2534.6395 436 2381.6858 447 2236.1082 458 2097.3854 469 1965.0442 480 1838.6539 491 1717.8219 502 1602.1892 513 1491.4272 524 1385.2344 535 1283.3336 546 1185.4698 557 1091.4077 568 1000.9298 579 913.8351 590 829.9373 601 749.0634 612 671.0529 623 595.7562 634 523.0342 645 452.7569 656 384.8032 667 319.0596 678 255.4200 689 193.7849 700 134.0612 711 76.1613 722 20.0028 733 -34.4917 744 -87.3950 755 -138.7758 766 -188.6990 777 -237.2258 788 -284.4138 799 -330.3178 810 -374.9895 821 -418.4778 832 -460.8292 843 -502.0877 854 -542.2950 865 -581.4908 876 -619.7129 887 -656.9970 898 -693.3773 909 -728.8862 920 -763.5548 931 -797.4124 942 -830.4872 953 -862.8061 964 -894.3946 975 -925.2773 986 -955.4776 997 -985.0177 1008 -1013.9192 1019 -1042.2026 1030 -1069.8874 1041 -1096.9924 1052 -1123.5357 1063 -1149.5346 1074 -1175.0057 1085 -1199.9648 1096 -1224.4272 1107 -1248.4077 1118 -1271.9203 1129 -1294.9785 1140 -1317.5956 1151 -1339.7838 1162 -1361.5555 1173 -1382.9221 1184 -1403.8949 1195 -1424.4847 1206 -1444.7019 1217 -1464.5564 1228 -1484.0580 1239 -1503.2160 1250 -1522.0394 1261 -1540.5369 1272 -1558.7169 1283 -1576.5874 1294 -1594.1564 1305 -1611.4313 1316 -1628.4196 1327 -1645.1282 1338 -1661.5641 1349 -1677.7339 1360 -1693.6439 1371 -1709.3004 1382 -1724.7093 1393 -1739.8766 1404 -1754.8079 1415 -1769.5086 1426 -1783.9840 1437 -1798.2393 1448 -1812.2794 1459 -1826.1092 1470 -1839.7334 1481 -1853.1565 1492 -1866.3829 1503 -1879.4170 1514 -1892.2629 1525 -1904.9246 1536 -1917.4061 1547 -1929.7113 1558 -1941.8437 1569 -1953.8071 1580 -1965.6049 1591 -1977.2405 1602 -1988.7173 1613 -2000.0385 1624 -2011.2073 1635 -2022.2266 1646 -2033.0996 1657 -2043.8290 1668 -2054.4177 1679 -2064.8684 1690 -2075.1839 1701 -2085.3668 1712 -2095.4195 1723 -2105.3445 1734 -2115.1444 1745 -2124.8214 1756 -2134.3778 1767 -2143.8159 1778 -2153.1378 1789 -2162.3457 1800 -2171.4417 1811 -2180.4277 1822 -2189.3058 1833 -2198.0780 1844 -2206.7460 1855 -2215.3118 1866 -2223.7770 1877 -2232.1436 1888 -2240.4132 1899 -2248.5875 1910 -2256.6681 1921 -2264.6566 1932 -2272.5546 1943 -2280.3636 1954 -2288.0851 1965 -2295.7206 1976 -2303.2716 1987 -2310.7393 1998 -2318.1252 2009 -2325.4306 2020 -2332.6568 2031 -2339.8051 2042 -2346.8767 2053 -2353.8730 2064 -2360.7950 2075 -2367.6439 2086 -2374.4210 2097 -2381.1273 2108 -2387.7639 2119 -2394.3320 2130 -2400.8325 2141 -2407.2665 2152 -2413.6350 2163 -2419.9391 2174 -2426.1796 2185 -2432.3576 2196 -2438.4739 2207 -2444.5296 2218 -2450.5255 2229 -2456.4624 2240 -2462.3413 2251 -2468.1629 2262 -2473.9282 2273 -2479.6379 2284 -2485.2929 2295 -2490.8939 2306 -2496.4417 2317 -2501.9370 2328 -2507.3806 2339 -2512.7732 2350 -2518.1155 2361 -2523.4083 2372 -2528.6521 2383 -2533.8478 2394 -2538.9959 2405 -2544.0971 2416 -2549.1520 2427 -2554.1613 2438 -2559.1256 2449 -2564.0454 2460 -2568.9215 2471 -2573.7542 2482 -2578.5444 2493 -2583.2924 2504 -2587.9988 2515 -2592.6643 2526 -2597.2892 2537 -2601.8742 2548 -2606.4198 2559 -2610.9265 2570 -2615.3947 2581 -2619.8249 2592 -2624.2177 2603 -2628.5736 2614 -2632.8929 2625 -2637.1761 2636 -2641.4237 2647 -2645.6361 2658 -2649.8138 2669 -2653.9572 2680 -2658.0667 2691 -2662.1427 2702 -2666.1857 2713 -2670.1960 2724 -2674.1740 2735 -2678.1201 2746 -2682.0348 2757 -2685.9183 2768 -2689.7710 2779 -2693.5934 2790 -2697.3857 2801 -2701.1483 2812 -2704.8816 2823 -2708.5859 2834 -2712.2615 2845 -2715.9088 2856 -2719.5282 2867 -2723.1198 2878 -2726.6841 2889 -2730.2213 2900 -2733.7318 2911 -2737.2158 2922 -2740.6737 2933 -2744.1058 2944 -2747.5122 2955 -2750.8934 2966 -2754.2496 2977 -2757.5811 2988 -2760.8882 2999 -2764.1710 \end{filecontents*} \begin{filecontents*}[overwrite]{race_s4.dat} n d 306 7284.5724 317 6997.5388 328 6729.4766 339 6478.5634 350 6243.2030 361 6021.9915 372 5813.6892 383 5617.1974 394 5431.5384 405 5255.8399 416 5089.3207 427 4931.2793 438 4781.0840 449 4638.1643 460 4502.0037 471 4372.1337 482 4248.1279 493 4129.5978 504 4016.1882 515 3907.5742 526 3803.4580 537 3703.5655 548 3607.6449 559 3515.4638 570 3426.8075 581 3341.4777 592 3259.2905 603 3180.0753 614 3103.6739 625 3029.9388 636 2958.7329 647 2889.9280 658 2823.4049 669 2759.0518 680 2696.7642 691 2636.4442 702 2578.0000 713 2521.3455 724 2466.3996 735 2413.0862 746 2361.3335 757 2311.0741 768 2262.2442 779 2214.7836 790 2168.6356 801 2123.7464 812 2080.0652 823 2037.5439 834 1996.1368 845 1955.8008 856 1916.4948 867 1878.1799 878 1840.8189 889 1804.3768 900 1768.8201 911 1734.1168 922 1700.2365 933 1667.1505 944 1634.8309 955 1603.2516 966 1572.3874 977 1542.2142 988 1512.7090 999 1483.8500 1010 1455.6162 1021 1427.9874 1032 1400.9444 1043 1374.4688 1054 1348.5429 1065 1323.1497 1076 1298.2730 1087 1273.8972 1098 1250.0073 1109 1226.5890 1120 1203.6283 1131 1181.1121 1142 1159.0274 1153 1137.3622 1164 1116.1044 1175 1095.2427 1186 1074.7662 1197 1054.6642 1208 1034.9267 1219 1015.5437 1230 996.5058 1241 977.8039 1252 959.4291 1263 941.3729 1274 923.6272 1285 906.1840 1296 889.0355 1307 872.1745 1318 855.5937 1329 839.2862 1340 823.2453 1351 807.4646 1362 791.9377 1373 776.6585 1384 761.6212 1395 746.8201 1406 732.2497 1417 717.9046 1428 703.7796 1439 689.8697 1450 676.1700 1461 662.6758 1472 649.3825 1483 636.2856 1494 623.3809 1505 610.6641 1516 598.1312 1527 585.7781 1538 573.6011 1549 561.5964 1560 549.7604 1571 538.0895 1582 526.5804 1593 515.2296 1604 504.0340 1615 492.9903 1626 482.0955 1637 471.3466 1648 460.7408 1659 450.2751 1670 439.9467 1681 429.7531 1692 419.6916 1703 409.7596 1714 399.9547 1725 390.2745 1736 380.7164 1747 371.2784 1758 361.9581 1769 352.7533 1780 343.6619 1791 334.6819 1802 325.8111 1813 317.0476 1824 308.3895 1835 299.8349 1846 291.3819 1857 283.0287 1868 274.7736 1879 266.6149 1890 258.5509 1901 250.5799 1912 242.7003 1923 234.9106 1934 227.2093 1945 219.5948 1956 212.0657 1967 204.6206 1978 197.2580 1989 189.9767 2000 182.7752 2011 175.6522 2022 168.6065 2033 161.6369 2044 154.7421 2055 147.9209 2066 141.1721 2077 134.4946 2088 127.8872 2099 121.3490 2110 114.8787 2121 108.4753 2132 102.1378 2143 95.8653 2154 89.6566 2165 83.5108 2176 77.4270 2187 71.4043 2198 65.4416 2209 59.5382 2220 53.6932 2231 47.9056 2242 42.1747 2253 36.4996 2264 30.8795 2275 25.3136 2286 19.8012 2297 14.3414 2308 8.9335 2319 3.5768 2330 -1.7294 2341 -6.9859 2352 -12.1934 2363 -17.3525 2374 -22.4639 2385 -27.5283 2396 -32.5462 2407 -37.5185 2418 -42.4456 2429 -47.3281 2440 -52.1668 2451 -56.9621 2462 -61.7147 2473 -66.4251 2484 -71.0939 2495 -75.7216 2506 -80.3087 2517 -84.8559 2528 -89.3636 2539 -93.8323 2550 -98.2625 2561 -102.6548 2572 -107.0096 2583 -111.3274 2594 -115.6087 2605 -119.8538 2616 -124.0634 2627 -128.2378 2638 -132.3774 2649 -136.4827 2660 -140.5542 2671 -144.5922 2682 -148.5971 2693 -152.5694 2704 -156.5095 2715 -160.4176 2726 -164.2944 2737 -168.1400 2748 -171.9549 2759 -175.7394 2770 -179.4940 2781 -183.2189 2792 -186.9145 2803 -190.5811 2814 -194.2192 2825 -197.8290 2836 -201.4108 2847 -204.9651 2858 -208.4920 2869 -211.9919 2880 -215.4652 2891 -218.9120 2902 -222.3328 2913 -225.7278 2924 -229.0973 2935 -232.4416 2946 -235.7610 2957 -239.0558 2968 -242.3261 2979 -245.5724 2990 -248.7948 \end{filecontents*} \begin{filecontents*}[overwrite]{rates.dat} j rate 1 0.18653860 2 0.20232018 3 0.20564841 4 0.20647213 5 0.20658618 6 0.20646962 7 0.20627928 8 0.20607247 9 0.20587107 10 0.20568303 11 0.20551065 12 0.20535381 13 0.20521148 14 0.20508229 15 0.20496485 \end{filecontents*} \begin{filecontents*}[overwrite]{ratio_rule.dat} n r 492 1.129334 493 1.126491 494 1.129885 495 1.127054 496 1.130435 497 1.127618 498 1.128294 499 1.128181 500 1.126158 501 1.128745 502 1.125826 503 1.129308 504 1.126402 505 1.129871 506 1.126978 507 1.130435 508 1.127554 509 1.128304 510 1.128131 511 1.126176 512 1.128707 513 1.125730 514 1.129283 515 1.126318 516 1.129859 517 1.126906 518 1.130435 519 1.127494 520 1.128313 521 1.128082 522 1.126194 523 1.128670 524 1.125637 525 1.129258 526 1.126237 527 1.129847 528 1.126836 529 1.130435 530 1.127436 531 1.128321 532 1.128036 533 1.126211 534 1.128635 535 1.125548 536 1.129235 537 1.126159 538 1.129835 539 1.126769 540 1.130435 541 1.127380 542 1.128329 543 1.127991 544 1.126228 545 1.128602 546 1.125463 547 1.129213 548 1.126084 549 1.129824 550 1.126705 551 1.130435 552 1.127326 553 1.128337 554 1.127948 555 1.126243 556 1.128570 557 1.125380 558 1.129191 559 1.126012 560 1.129813 561 1.126643 562 1.130435 563 1.127275 564 1.128345 565 1.127907 566 1.126259 567 1.128539 568 1.125301 569 1.129171 570 1.125943 571 1.129803 572 1.126584 573 1.130435 574 1.127225 575 1.128352 576 1.127867 577 1.126273 578 1.128509 579 1.125225 580 1.129151 581 1.125876 582 1.129793 583 1.126527 584 1.130435 585 1.127178 586 1.128359 587 1.127829 588 1.126287 589 1.128480 590 1.125152 591 1.129132 592 1.125812 593 1.129783 594 1.126472 595 1.130435 596 1.127132 597 1.128366 598 1.127792 599 1.126301 600 1.128452 601 1.125081 602 1.129113 603 1.125750 604 1.129774 605 1.126418 606 1.130435 607 1.127087 608 1.128372 609 1.127756 610 1.126314 611 1.128426 612 1.125013 613 1.129095 614 1.125690 615 1.129765 616 1.126367 617 1.130435 618 1.127045 619 1.128379 620 1.127722 621 1.126326 622 1.128400 623 1.124947 624 1.129078 625 1.125632 626 1.129756 627 1.126318 628 1.130435 629 1.127003 630 1.128385 631 1.127689 632 1.126338 633 1.128375 634 1.124883 635 1.129062 636 1.125576 637 1.129748 638 1.126270 639 1.130435 640 1.126963 641 1.128390 642 1.127657 643 1.126350 644 1.128351 645 1.124822 646 1.129045 647 1.125522 648 1.129740 649 1.126223 650 1.130435 651 1.126925 652 1.128396 653 1.127626 654 1.126361 655 1.128328 656 1.124762 657 1.129030 658 1.125470 659 1.129732 660 1.126179 661 1.130435 662 1.126887 663 1.128402 664 1.127596 665 1.126372 666 1.128306 667 1.124705 668 1.129015 669 1.125420 670 1.129725 671 1.126135 672 1.130435 673 1.126851 674 1.128407 675 1.127567 676 1.126382 677 1.128284 678 1.124649 679 1.129001 680 1.125371 681 1.129718 682 1.126094 683 1.130435 684 1.126816 685 1.128412 686 1.127539 687 1.126393 688 1.128263 689 1.124595 690 1.128987 691 1.125324 692 1.129710 693 1.126053 694 1.130435 695 1.126782 696 1.128417 697 1.127512 698 1.126403 699 1.128242 700 1.124542 701 1.128973 702 1.125278 703 1.129704 704 1.126014 705 1.130435 706 1.126750 707 1.128422 708 1.127486 709 1.126412 710 1.128223 711 1.124492 712 1.128960 713 1.125233 714 1.129697 715 1.125975 716 1.130435 717 1.126718 718 1.128426 719 1.127460 720 1.126421 721 1.128204 722 1.124442 723 1.128947 724 1.125190 725 1.129691 726 1.125938 727 1.130435 728 1.126687 729 1.128431 730 1.127436 731 1.126430 732 1.128185 733 1.124433 734 1.128935 735 1.125148 736 1.129685 737 1.125902 738 1.130435 739 1.126657 740 1.128435 741 1.127412 742 1.126439 743 1.128167 744 1.124446 745 1.128923 746 1.125108 747 1.129678 748 1.125868 749 1.130435 750 1.126628 751 1.128439 752 1.127388 753 1.126447 754 1.128149 755 1.124459 756 1.128911 757 1.125068 758 1.129673 759 1.125834 760 1.130435 761 1.126599 762 1.128444 763 1.127366 764 1.126456 765 1.128132 766 1.124471 767 1.128900 768 1.125030 769 1.129667 770 1.125801 771 1.130435 772 1.126572 773 1.128448 774 1.127344 775 1.126464 776 1.128116 777 1.124483 778 1.128888 779 1.124992 780 1.129661 781 1.125769 782 1.130435 783 1.126545 784 1.128451 785 1.127322 786 1.126471 787 1.128100 788 1.124495 789 1.128878 790 1.124956 791 1.129656 792 1.125737 793 1.130435 794 1.126519 795 1.128455 796 1.127302 797 1.126479 798 1.128084 799 1.124506 800 1.128867 801 1.124921 802 1.129651 803 1.125707 804 1.130435 805 1.126494 806 1.128459 807 1.127281 808 1.126486 809 1.128069 810 1.124517 811 1.128857 812 1.124886 813 1.129646 814 1.125678 815 1.130435 816 1.126469 817 1.128462 818 1.127262 819 1.126493 820 1.128054 821 1.124528 822 1.128847 823 1.124853 824 1.129641 825 1.125649 826 1.130435 827 1.126445 828 1.128466 829 1.127242 830 1.126500 831 1.128040 832 1.124538 833 1.128838 834 1.124820 835 1.129636 836 1.125621 837 1.130435 838 1.126422 839 1.128469 840 1.127224 841 1.126507 842 1.128026 843 1.124548 844 1.128828 845 1.124788 846 1.129631 847 1.125594 848 1.130435 849 1.126399 850 1.128473 851 1.127206 852 1.126514 853 1.128012 854 1.124558 855 1.128819 856 1.124757 857 1.129627 858 1.125567 859 1.130435 860 1.126377 861 1.128476 862 1.127188 863 1.126520 864 1.127999 865 1.124568 866 1.128810 867 1.124727 868 1.129622 869 1.125541 870 1.130435 871 1.126356 872 1.128479 873 1.127170 874 1.126526 875 1.127986 876 1.124577 877 1.128802 878 1.124698 879 1.129618 880 1.125516 881 1.130435 882 1.126334 883 1.128482 884 1.127154 885 1.126532 886 1.127973 887 1.124586 888 1.128793 889 1.124669 890 1.129614 891 1.125491 892 1.130435 893 1.126314 894 1.128485 895 1.127137 896 1.126538 897 1.127961 898 1.124595 899 1.128785 900 1.124641 901 1.129610 902 1.125467 903 1.130435 904 1.126294 905 1.128488 906 1.127121 907 1.126544 908 1.127949 909 1.124604 910 1.128777 911 1.124614 912 1.129606 913 1.125444 914 1.130435 915 1.126274 916 1.128491 917 1.127105 918 1.126550 919 1.127937 920 1.124612 921 1.128769 922 1.124587 923 1.129602 924 1.125421 925 1.130435 926 1.126255 927 1.128493 928 1.127090 929 1.126555 930 1.127925 931 1.124621 932 1.128761 933 1.124561 934 1.129598 935 1.125398 936 1.130435 937 1.126236 938 1.128496 939 1.127075 940 1.126561 941 1.127914 942 1.124629 943 1.128754 944 1.124535 945 1.129594 946 1.125377 947 1.130435 948 1.126218 949 1.128499 950 1.127060 951 1.126566 952 1.127903 953 1.124637 954 1.128747 955 1.124510 956 1.129590 957 1.125355 958 1.130435 959 1.126200 960 1.128501 961 1.127046 962 1.126571 963 1.127892 964 1.124644 965 1.128739 966 1.124486 967 1.129587 968 1.125334 969 1.130435 970 1.126183 971 1.128504 972 1.127032 973 1.126576 974 1.127882 975 1.124652 976 1.128732 977 1.124462 978 1.129583 979 1.125314 980 1.130435 981 1.126166 982 1.128506 983 1.127019 984 1.126581 985 1.127872 986 1.124659 987 1.128726 988 1.124439 989 1.129580 990 1.125294 991 1.130435 992 1.126149 993 1.128509 994 1.127005 995 1.126586 996 1.127862 997 1.124666 998 1.128719 999 1.124416 1000 1.129577 1001 1.125274 1002 1.130435 1003 1.126133 1004 1.128511 1005 1.126992 1006 1.126591 1007 1.127852 1008 1.124673 1009 1.128712 1010 1.124394 1011 1.129573 1012 1.125255 1013 1.130435 1014 1.126117 1015 1.128513 1016 1.126979 1017 1.126595 1018 1.127842 1019 1.124680 1020 1.128706 1021 1.124372 1022 1.129570 1023 1.125236 1024 1.130435 1025 1.126101 1026 1.128516 1027 1.126967 1028 1.126600 1029 1.127833 1030 1.124687 1031 1.128700 1032 1.124351 1033 1.129567 1034 1.125218 1035 1.130435 1036 1.126086 1037 1.128518 1038 1.126955 1039 1.126604 1040 1.127824 1041 1.124694 1042 1.128693 1043 1.124330 1044 1.129564 1045 1.125200 1046 1.130435 1047 1.126071 1048 1.128520 1049 1.126943 1050 1.126609 1051 1.127815 1052 1.124700 1053 1.128687 1054 1.124309 1055 1.129561 1056 1.125182 1057 1.130435 1058 1.126056 1059 1.128522 1060 1.126931 1061 1.126613 1062 1.127806 1063 1.124707 1064 1.128682 1065 1.124289 1066 1.129558 1067 1.125165 1068 1.130435 1069 1.126042 1070 1.128524 1071 1.126919 1072 1.126617 1073 1.127797 1074 1.124713 1075 1.128676 1076 1.124269 1077 1.129555 1078 1.125148 1079 1.130435 1080 1.126028 1081 1.128526 1082 1.126908 1083 1.126621 1084 1.127789 1085 1.124719 1086 1.128670 1087 1.124250 1088 1.129552 1089 1.125132 1090 1.130435 1091 1.126014 1092 1.128528 1093 1.126897 1094 1.126625 1095 1.127780 1096 1.124725 1097 1.128665 1098 1.124231 1099 1.129549 1100 1.125116 1101 1.130435 1102 1.126001 1103 1.128530 1104 1.126886 1105 1.126629 1106 1.127772 1107 1.124731 1108 1.128659 1109 1.124213 1110 1.129547 1111 1.125100 1112 1.130435 1113 1.125987 1114 1.128532 1115 1.126876 1116 1.126633 1117 1.127764 1118 1.124736 1119 1.128654 1120 1.124195 1121 1.129544 1122 1.125084 1123 1.130435 1124 1.125974 1125 1.128534 1126 1.126865 1127 1.126636 1128 1.127757 1129 1.124742 1130 1.128649 1131 1.124177 1132 1.129541 1133 1.125069 1134 1.130435 1135 1.125962 1136 1.128536 1137 1.126855 1138 1.126640 1139 1.127749 1140 1.124747 1141 1.128644 1142 1.124159 1143 1.129539 1144 1.125054 1145 1.130435 1146 1.125949 1147 1.128538 1148 1.126845 1149 1.126644 1150 1.127741 1151 1.124753 1152 1.128639 1153 1.124142 1154 1.129536 1155 1.125039 1156 1.130435 1157 1.125937 1158 1.128539 1159 1.126835 1160 1.126647 1161 1.127734 1162 1.124758 1163 1.128634 1164 1.124125 1165 1.129534 1166 1.125025 1167 1.130435 1168 1.125925 1169 1.128541 1170 1.126825 1171 1.126651 1172 1.127727 1173 1.124763 1174 1.128629 1175 1.124109 1176 1.129531 1177 1.125011 1178 1.130435 1179 1.125913 1180 1.128543 1181 1.126816 1182 1.126654 1183 1.127720 1184 1.124768 1185 1.128624 1186 1.124093 1187 1.129529 1188 1.124997 1189 1.130435 1190 1.125901 1191 1.128544 1192 1.126807 1193 1.126657 1194 1.127713 1195 1.124773 1196 1.128619 1197 1.124077 1198 1.129527 1199 1.124983 1200 1.130435 1201 1.125890 1202 1.128546 1203 1.126798 1204 1.126661 1205 1.127706 1206 1.124778 1207 1.128615 1208 1.124061 1209 1.129524 1210 1.124970 1211 1.130435 1212 1.125879 1213 1.128548 1214 1.126789 1215 1.126664 1216 1.127699 1217 1.124783 1218 1.128610 1219 1.124046 1220 1.129522 1221 1.124956 1222 1.130435 1223 1.125868 1224 1.128549 1225 1.126780 1226 1.126667 1227 1.127692 1228 1.124788 1229 1.128606 1230 1.124031 1231 1.129520 1232 1.124943 1233 1.130435 1234 1.125857 1235 1.128551 1236 1.126771 1237 1.126670 1238 1.127686 1239 1.124792 1240 1.128602 1241 1.124016 1242 1.129518 1243 1.124931 1244 1.130435 1245 1.125846 1246 1.128552 1247 1.126763 1248 1.126673 1249 1.127680 1250 1.124797 1251 1.128597 1252 1.124001 1253 1.129516 1254 1.124918 1255 1.130435 1256 1.125836 1257 1.128554 1258 1.126754 1259 1.126676 1260 1.127673 1261 1.124801 1262 1.128593 1263 1.123987 1264 1.129514 1265 1.124906 1266 1.130435 1267 1.125826 1268 1.128555 1269 1.126746 1270 1.126679 1271 1.127667 1272 1.124806 1273 1.128589 1274 1.123973 1275 1.129512 1276 1.124894 1277 1.130435 1278 1.125816 1279 1.128557 1280 1.126738 1281 1.126682 1282 1.127661 1283 1.124810 1284 1.128585 1285 1.123959 1286 1.129510 1287 1.124882 1288 1.130435 1289 1.125806 1290 1.128558 1291 1.126730 1292 1.126685 1293 1.127655 1294 1.124814 1295 1.128581 1296 1.123945 1297 1.129508 1298 1.124870 1299 1.130435 1300 1.125796 1301 1.128560 1302 1.126722 1303 1.126688 1304 1.127649 1305 1.124819 1306 1.128577 1307 1.123932 1308 1.129506 1309 1.124859 1310 1.130435 1311 1.125786 1312 1.128561 1313 1.126715 1314 1.126690 1315 1.127644 1316 1.124823 1317 1.128573 1318 1.123919 1319 1.129504 1320 1.124848 1321 1.130435 1322 1.125777 1323 1.128562 1324 1.126707 1325 1.126693 1326 1.127638 1327 1.124827 1328 1.128570 1329 1.123906 1330 1.129502 1331 1.124837 1332 1.130435 1333 1.125768 1334 1.128564 1335 1.126700 1336 1.126696 1337 1.127632 1338 1.124831 1339 1.128566 1340 1.123893 1341 1.129500 1342 1.124826 1343 1.130435 1344 1.125759 1345 1.128565 1346 1.126692 1347 1.126698 1348 1.127627 1349 1.124835 1350 1.128562 1351 1.123881 1352 1.129498 1353 1.124815 1354 1.130435 1355 1.125750 1356 1.128566 1357 1.126685 1358 1.126701 1359 1.127622 1360 1.124838 1361 1.128559 1362 1.123868 1363 1.129496 1364 1.124804 1365 1.130435 1366 1.125741 1367 1.128568 1368 1.126678 1369 1.126703 1370 1.127616 1371 1.124842 1372 1.128555 1373 1.123856 1374 1.129495 1375 1.124794 1376 1.130435 1377 1.125732 1378 1.128569 1379 1.126671 1380 1.126706 1381 1.127611 1382 1.124846 1383 1.128552 1384 1.123844 1385 1.129493 1386 1.124784 1387 1.130435 1388 1.125724 1389 1.128570 1390 1.126664 1391 1.126708 1392 1.127606 1393 1.124850 1394 1.128548 1395 1.123833 1396 1.129491 1397 1.124774 1398 1.130435 1399 1.125715 1400 1.128571 1401 1.126658 1402 1.126711 1403 1.127601 1404 1.124853 1405 1.128545 1406 1.123821 1407 1.129489 1408 1.124764 1409 1.130435 1410 1.125707 1411 1.128572 1412 1.126651 1413 1.126713 1414 1.127596 1415 1.124857 1416 1.128541 1417 1.123810 1418 1.129488 1419 1.124754 1420 1.130435 1421 1.125699 1422 1.128574 1423 1.126645 1424 1.126715 1425 1.127591 1426 1.124860 1427 1.128538 1428 1.123799 1429 1.129486 1430 1.124744 1431 1.130435 1432 1.125691 1433 1.128575 1434 1.126638 1435 1.126718 1436 1.127586 1437 1.124864 1438 1.128535 1439 1.123788 1440 1.129484 1441 1.124735 1442 1.130435 1443 1.125683 1444 1.128576 1445 1.126632 1446 1.126720 1447 1.127581 1448 1.124867 1449 1.128532 1450 1.123777 1451 1.129483 1452 1.124726 1453 1.130435 1454 1.125675 1455 1.128577 1456 1.126626 1457 1.126722 1458 1.127577 1459 1.124870 1460 1.128529 1461 1.123766 1462 1.129481 1463 1.124716 1464 1.130435 1465 1.125667 1466 1.128578 1467 1.126619 1468 1.126724 1469 1.127572 1470 1.124874 1471 1.128526 1472 1.123755 1473 1.129480 1474 1.124707 1475 1.130435 1476 1.125660 1477 1.128579 1478 1.126613 1479 1.126727 1480 1.127568 1481 1.124877 1482 1.128523 1483 1.123745 1484 1.129478 1485 1.124698 1486 1.130435 1487 1.125653 1488 1.128580 1489 1.126607 1490 1.126729 1491 1.127563 1492 1.124880 1493 1.128520 1494 1.123735 1495 1.129477 1496 1.124690 1497 1.130435 1498 1.125645 1499 1.128581 1500 1.126602 \end{filecontents*} \begin{filecontents*}[overwrite]{ratio_table.dat} n r 4 1.345186 5 1.312938 6 1.290363 7 1.302858 8 1.265738 9 1.292855 10 1.265757 11 1.282929 12 1.260870 13 1.273079 14 1.261975 15 1.263305 16 1.258708 17 1.253606 18 1.257541 19 1.243981 20 1.253507 21 1.234430 22 1.250391 23 1.233459 24 1.245404 25 1.233556 26 1.240886 27 1.233616 28 1.235113 29 1.232167 30 1.229614 31 1.229661 32 1.223249 33 1.227150 34 1.217063 35 1.224647 36 1.216199 37 1.220585 38 1.215877 39 1.216705 40 1.213830 41 1.212835 42 1.211839 43 1.208152 44 1.210173 45 1.203087 46 1.208503 47 1.202955 48 1.205632 49 1.201263 50 1.201979 51 1.199753 52 1.198333 53 1.198369 54 1.194696 55 1.196980 56 1.192391 57 1.195587 58 1.190984 59 1.193399 60 1.189660 61 1.190017 62 1.188506 63 1.186704 64 1.187348 65 1.183541 66 1.186186 67 1.182367 68 1.185020 69 1.181189 70 1.183204 71 1.180099 72 1.180234 73 1.179133 74 1.177052 75 1.178163 76 1.174998 77 1.177190 78 1.174014 79 1.176214 80 1.173027 81 1.174578 82 1.172037 83 1.171849 84 1.171202 85 1.168779 86 1.170392 87 1.167769 88 1.169579 89 1.166947 90 1.168763 91 1.166121 92 1.167184 93 1.165292 94 1.164582 95 1.164461 96 1.162255 97 1.163731 98 1.161573 99 1.163055 100 1.160888 101 1.162377 102 1.160201 103 1.160776 104 1.159511 105 1.158223 106 1.158818 107 1.156766 108 1.158123 109 1.156203 110 1.157425 111 1.155638 112 1.156842 113 1.155071 114 1.155169 115 1.154501 116 1.152694 117 1.153928 118 1.152113 119 1.153354 120 1.151530 121 1.152777 122 1.151044 123 1.151998 124 1.150581 125 1.150221 126 1.150117 127 1.148667 128 1.149650 129 1.148193 130 1.149181 131 1.147716 132 1.148710 133 1.147238 134 1.147725 135 1.146757 136 1.145824 137 1.146274 138 1.145114 139 1.145875 140 1.144734 141 1.145499 142 1.144351 143 1.145121 144 1.143966 145 1.143926 146 1.143580 147 1.142395 148 1.143191 149 1.142000 150 1.142800 151 1.141659 152 1.142408 153 1.141360 154 1.141931 155 1.141059 156 1.140527 157 1.140756 158 1.139856 159 1.140451 160 1.139545 161 1.140144 162 1.139232 163 1.139836 164 1.138918 165 1.139077 166 1.138601 167 1.137818 168 1.138283 169 1.137584 170 1.137999 171 1.137349 172 1.137768 173 1.137112 174 1.137535 175 1.136873 176 1.136508 177 1.136633 178 1.135945 179 1.136391 180 1.135697 181 1.136147 182 1.135448 183 1.135901 184 1.135203 185 1.135464 186 1.135033 187 1.134584 188 1.134861 189 1.134407 190 1.134688 191 1.134228 192 1.134513 193 1.134048 194 1.134336 195 1.133866 196 1.133590 197 1.133682 198 1.133189 199 1.133497 200 1.133015 201 1.133311 202 1.132899 203 1.133123 204 1.132781 205 1.132920 206 1.132662 207 1.132387 208 1.132541 209 1.132262 210 1.132420 211 1.132135 212 1.132296 213 1.132007 214 1.132171 215 1.131877 216 1.131633 217 1.131746 218 1.131487 219 1.131613 220 1.131419 221 1.131479 222 1.131350 223 1.131374 224 1.131280 225 1.131306 226 1.131208 227 1.131094 228 1.131135 229 1.131016 230 1.131060 231 1.130937 232 1.130985 233 1.130857 234 1.130908 235 1.130775 236 1.130687 237 1.130692 238 1.130664 239 1.130608 240 1.130639 241 1.130556 242 1.130614 243 1.130533 244 1.130587 245 1.130510 246 1.130559 247 1.130243 248 1.130530 249 1.130269 250 1.130499 251 1.130294 252 1.130468 253 1.130317 254 1.130435 255 1.130340 256 1.130145 257 1.130361 258 1.129835 259 1.130381 260 1.129906 261 1.130400 262 1.129975 263 1.130418 264 1.130044 265 1.130435 266 1.130112 267 1.129809 268 1.130179 269 1.129458 270 1.130244 271 1.129570 272 1.130309 273 1.129682 274 1.130372 275 1.129792 276 1.130435 277 1.129902 278 1.129500 279 1.130010 280 1.129109 281 1.130118 282 1.129260 283 1.130225 284 1.129410 285 1.130330 286 1.129559 287 1.130435 288 1.129707 289 1.129213 290 1.129855 291 1.128785 292 1.130001 293 1.128972 294 1.130146 295 1.129158 296 1.130291 297 1.129342 298 1.130435 299 1.129527 300 1.128946 301 1.129710 302 1.128484 303 1.129892 304 1.128704 305 1.130074 306 1.128923 307 1.130255 308 1.129141 309 1.130435 310 1.129358 311 1.128699 312 1.129575 313 1.128202 314 1.129791 315 1.128453 316 1.130006 317 1.128703 318 1.130221 319 1.128953 320 1.130435 321 1.129201 322 1.128467 323 1.129449 324 1.127939 325 1.129697 326 1.128219 327 1.129943 328 1.128498 329 1.130189 330 1.128777 331 1.130435 332 1.129054 333 1.128251 334 1.129332 335 1.127692 336 1.129608 337 1.127999 338 1.129885 339 1.128306 340 1.130160 341 1.128611 342 1.130435 343 1.128917 344 1.128101 345 1.129222 346 1.127460 347 1.129526 348 1.127793 349 1.129829 350 1.128125 351 1.130132 352 1.128456 353 1.130435 354 1.128787 355 1.128120 356 1.129118 357 1.127242 358 1.129448 359 1.127599 360 1.129777 361 1.127955 362 1.130106 363 1.128310 364 1.130435 365 1.128666 366 1.128138 367 1.129020 368 1.127036 369 1.129375 370 1.127416 371 1.129729 372 1.127794 373 1.130082 374 1.128173 375 1.130435 376 1.128551 377 1.128156 378 1.128928 379 1.126842 380 1.129306 381 1.127243 382 1.129682 383 1.127643 384 1.130059 385 1.128043 386 1.130435 387 1.128442 388 1.128172 389 1.128842 390 1.126658 391 1.129241 392 1.127079 393 1.129639 394 1.127500 395 1.130037 396 1.127920 397 1.130435 398 1.128340 399 1.128187 400 1.128760 401 1.126484 402 1.129179 403 1.126924 404 1.129598 405 1.127364 406 1.130016 407 1.127804 408 1.130435 409 1.128243 410 1.128202 411 1.128682 412 1.126319 413 1.129120 414 1.126777 415 1.129559 416 1.127235 417 1.129997 418 1.127693 419 1.130435 420 1.128151 421 1.128215 422 1.128608 423 1.126162 424 1.129065 425 1.126637 426 1.129522 427 1.127113 428 1.129978 429 1.127588 430 1.130435 431 1.128063 432 1.128228 433 1.128538 434 1.126026 435 1.129012 436 1.126505 437 1.129487 438 1.126996 439 1.129961 440 1.127488 441 1.130435 442 1.127980 443 1.128241 444 1.128471 445 1.126051 446 1.128962 447 1.126378 448 1.129453 449 1.126886 450 1.129944 451 1.127393 452 1.130435 453 1.127900 454 1.128253 455 1.128408 456 1.126074 457 1.128915 458 1.126257 459 1.129421 460 1.126780 461 1.129928 462 1.127302 463 1.130435 464 1.127825 465 1.128264 466 1.128347 467 1.126097 468 1.128869 469 1.126142 470 1.129391 471 1.126679 472 1.129913 473 1.127216 474 1.130435 475 1.127753 476 1.128274 477 1.128289 478 1.126118 479 1.128826 480 1.126032 481 1.129362 482 1.126583 483 1.129899 484 1.127133 485 1.130435 486 1.127684 487 1.128285 488 1.128234 489 1.126138 490 1.128784 491 1.125927 \end{filecontents*} \documentclass[11pt]{article} \usepackage{amsmath,amssymb,amsthm,mathtools} \usepackage[margin=1in]{geometry} \usepackage{graphicx} \usepackage{booktabs} \usepackage{longtable} \usepackage{microtype} \usepackage{enumitem} \usepackage[font=small,labelfont=bf]{caption} \usepackage{subcaption} \usepackage{xcolor} \usepackage{tikz} \usetikzlibrary{calc,positioning,arrows.meta,shapes.geometric,fit,backgrounds,decorations.pathreplacing} \usepackage{pgfplots} \usepgfplotslibrary{groupplots} \pgfplotsset{compat=1.17} \setlength{\emergencystretch}{2.5em} \usepackage{hyperref} \hypersetup{colorlinks=true, linkcolor=black, citecolor=black, urlcolor=blue} \usepackage[capitalise,noabbrev]{cleveref} \newtheorem{theorem}{Theorem} \newtheorem{proposition}[theorem]{Proposition} \newtheorem{lemma}[theorem]{Lemma} \newtheorem{corollary}[theorem]{Corollary} \theoremstyle{definition} \newtheorem{definition}[theorem]{Definition} \newtheorem{remark}[theorem]{Remark} % cleveref names shared-counter environments after the counter ("Theorem"); alias them per environment. \usepackage{etoolbox} \AtBeginEnvironment{lemma}{\crefalias{theorem}{lemma}} \AtBeginEnvironment{proposition}{\crefalias{theorem}{proposition}} \AtBeginEnvironment{corollary}{\crefalias{theorem}{corollary}} \AtBeginEnvironment{definition}{\crefalias{theorem}{definition}} \AtBeginEnvironment{remark}{\crefalias{theorem}{remark}} \newcommand{\per}{\operatorname{per}} \renewcommand{\deg}{\operatorname{deg}} \newcommand{\bell}{\ell} \newcommand{\Fs}{F^{\ast}} \newcommand{\lean}[1]{\texttt{#1}} \definecolor{afive}{HTML}{8A2F45} \definecolor{afour}{HTML}{0F6F7F} \definecolor{asix}{HTML}{B86E00} \definecolor{soft}{HTML}{F1DFE4} \definecolor{coolsoft}{HTML}{D9ECEF} \definecolor{leanbg}{HTML}{F4F2EC} % The formal side of each step, set off from the mathematics. \newenvironment{inlean}{\par\medskip\noindent\begin{tikzpicture}\node[fill=leanbg,rounded corners=2pt, inner sep=6pt,text width=\dimexpr\linewidth-12pt\relax,font=\small]\bgroup\textbf{In Lean.}\ }% {\egroup;\end{tikzpicture}\par\medskip} \tikzset{ v/.style={circle,fill=black,inner sep=1.3pt}, cen/.style={circle,draw=black,fill=white,inner sep=2.2pt}, box/.style={draw,rounded corners=2pt,align=center,font=\small,inner sep=4pt}, } \title{The maximum Laplacian ratio of a tree:\\ a complete answer to a question of Brualdi and Goldwasser,\\ kernel-checked in Lean} \author{Peter W.\ Murphy, MD} \date{9 October 2026 \quad (preprint, not yet refereed)} \begin{document} \maketitle \begin{abstract} For a tree $T$ with Laplacian $L(T)$, Brualdi and Goldwasser (1984) introduced the \emph{Laplacian ratio} $\pi(T)=\per L(T)/\prod_v\deg v$ and asked which tree on $n$ vertices maximizes it. We answer the question for every $n$. For every $n\ge 4$ the maximum is attained by a \emph{spider of cherry arms}: a centre carrying pendant paths of length two (cherries) and \emph{arms}, an arm being a vertex that carries cherries. For $n\ge 492$ the centre carries only arms, almost all with five cherries, and the exceptional arms are fixed by $6(n-1)\bmod 11$ through an explicit rule; for $4\le n\le 491$ the maximizer is given by an explicit table. Along the way we determine the exact exponential growth rate of the maximum, $\tfrac{64}{621}\rho^{n}\le\max_{|T|=n}\pi(T)\le 2\rho^{n-1}$ with $\rho=(621/64)^{1/11}$, and prove the sharp inequality behind it: every pendant subtree $b$ has matching weight at most $\rho^{|b|}$, with equality exactly for the five-cherry arm. The whole argument is formalized in Lean~4 with Mathlib and checked by the Lean kernel, depending only on Lean's three standard axioms. Large parts of it are certificates: exact data produced by untrusted generators and checked by the kernel. We explain the mathematics, show where each piece lives in the formal development and why it is organized that way, and discuss what the answer and the method suggest. \end{abstract} \tableofcontents \bigskip %===================================================================================================== \section{Introduction} %===================================================================================================== \subsection{The question} Let $T$ be a tree on $n\ge2$ vertices, $D$ its diagonal degree matrix, $A$ its adjacency matrix and $L(T)=D-A$ its Laplacian. Determinants and spectra of Laplacians are classical (see Merris's survey~\cite{Merris1994}): by the matrix-tree theorem the principal minors count spanning trees. Permanents are a different matter. The permanent $\per M=\sum_{\sigma}\prod_iM_{i,\sigma(i)}$ looks like the determinant without the signs, but it is \#P-hard to compute in general~\cite{Valiant1979}, and there is no comparable structure theory. Brualdi and Goldwasser~\cite{BG1984} studied $\per L(T)$ for trees and bipartite graphs. Since the permanent of a Laplacian grows with the degrees, they normalized it and introduced the \emph{Laplacian ratio} \[ \pi(T)=\frac{\per L(T)}{\prod_{v\in V(T)}\deg v}. \] They showed that $\pi(T)\ge 2$ for every tree on at least two vertices, with equality exactly for the star, and they asked the natural companion question: \emph{which tree on $n$ vertices maximizes $\pi$?} \subsection{A short history} \paragraph{1984: the question.} Merris, Rebman and Watkins~\cite{MRW1981} had introduced the permanental polynomial of the Laplacian a few years earlier; Brualdi and Goldwasser~\cite{BG1984} then studied $\per L$ of trees and bipartite graphs systematically, giving bounds in terms of the number of vertices, the degree sequence, the diameter and the matching number. Among much else, they showed that over trees on $n$ vertices the permanent $\per L(T)$ itself is smallest for the star and largest for the path, so the permanent alone is not interesting to optimize: it mostly rewards long paths with many vertices of degree two. Dividing by $\prod_v\deg v$ removes that trivial effect, and they introduced the ratio $\pi(T)$ for exactly this purpose. They proved the lower bound $\pi\ge2$ and posed extremal problems for the ratio, including bounds for trees with a given bipartition and the maximum over all trees on $n$ vertices. Later work sharpened the permanental bounds themselves; for instance, Geng, Hu and Li~\cite{GHL2010} determined the minimal permanents of Laplacians of trees, also under a maximum-degree constraint. \paragraph{2024--2025: the minimum side, and a conjecture for the maximum.} The minimum-type questions were resolved first. Wu, Dong, Lai and Zeng~\cite{Wu2024} determined the minimum of $\pi$ over trees on $n$ vertices with diameter at least $k$, and Wu, Dong and Lai~\cite{WDL2025} the minimum over trees with a given bipartition. For the maximum, Wu, Dong and Lai made a precise conjecture. For odd $n$ the maximizer should be the subdivided star with $(n-1)/2$ legs of length two, that is, a centre carrying only cherries, $C^{(n-1)/2}$ in the notation below, with value \[ \pi\big(C^{(n-1)/2}\big)=2\Big(\frac32\Big)^{(n-3)/2}; \] for even $n$ they conjectured explicit subdivided stars with closed-form values in the two classes $n\equiv0$ and $n\equiv2\pmod4$. The conjecture is natural: cherries are the best small building block (a cherry has matching weight $\tfrac32$ on two vertices), and for small $n$ it is correct. \paragraph{2026: counterexamples.} Pant~\cite{Pant2026} refuted the conjecture. His trees are caterpillars $T(a_1,\dots,a_m)$: a path $x_1x_2\cdots x_m$ in which $x_i$ carries $a_i$ cherries. He gave three infinite families, $A_t=T(3,t,3)$ on $2t+15$ vertices, $B_t=T(t,t,t,t)$ on $8t+4$ vertices and $C_t=T(t,t,t+1,t)$ on $8t+6$ vertices, whose ratios exceed the conjectured values from $t=4$ on, that is from $n=23$, $36$ and $38$ respectively, one family for each residue class of the conjecture. He also observed that the equality statement already fails at $n=21$, where $T(3,3,3)$ attains the conjectured value with a different degree sequence. He concluded that determining the maximum remains open, and he proposed no replacement. \paragraph{How the pieces fit.} With the complete answer in hand (\cref{thm:main}), the earlier work lines up exactly, which we find a pleasing check on everything involved: \begin{itemize} \item The Wu--Dong--Lai formulas give the true maximum for every $n\le22$, and for every even $n\le34$. They first fail at $n=23$, $36$ and $38$, precisely the sizes of Pant's first counterexamples $A_4$, $B_4$ and $C_4$. \item At $n=21$ exactly two trees are maximal: the conjectured $C^{10}$ and Pant's $T(3,3,3)$. Rooted at its middle vertex, $T(3,3,3)$ is the spider $C^3A_3^2$ (three cherries and two arms with three cherries each), and the two values agree: both equal $19683/256$. \item At $n=23$ Pant's $A_4=T(3,4,3)$ is \emph{the} maximizer: rooted at its middle vertex it is the spider $C^4A_3^2$. His other two families are caterpillars with four hubs, which are never spiders, so by \cref{thm:reduction} they are never maximal; at $n=36$ and $38$ the maximizers are $C^4A_4^3$ and $C^5A_4^3$. \end{itemize} So the answer grows out of both earlier proposals. Wu, Dong and Lai were right that pendant paths of length two are the basic unit; Pant was right that grouping them on several hubs beats a single hub of cherries. What neither family captures is the eventual structure: one hub carrying \emph{arms}, each a second-level hub with exactly five cherries. \subsection{The answer} This paper answers the question for every $n$. The answer is built from two small pieces (\cref{fig:spider}). \begin{definition}[cherries, arms, spiders] A \emph{cherry} is a pendant path of length two. For $j\ge1$ an \emph{arm} $A_j$ is a vertex, adjacent to the centre, that carries $j$ cherries and nothing else; it has $2j+1$ vertices. We write $A_0$ for a leaf adjacent to the centre. A \emph{spider of cherry arms} (in this paper, simply a \emph{spider}) is a tree with a vertex, the \emph{centre}, all of whose branches are leaves, cherries or arms. We write $C^{c}A_{j_1}A_{j_2}\cdots$ for the spider whose centre carries $c$ cherries and arms $A_{j_1},A_{j_2},\dots$, and use exponents for repeated arms. \end{definition} \begin{figure}[htbp]\centering \begin{tikzpicture}[scale=0.8] \node[cen] (o) at (0,0) {}; \foreach \a/\ang in {1/90,2/210,3/330} { \node[v,afive] (a\a) at (\ang:1.6) {}; \draw (o)--(a\a); \foreach \k in {0,...,4} { \pgfmathsetmacro{\t}{\ang-48+24*\k} \node[v] (m\a\k) at ($(a\a)+(\t:0.9)$) {}; \node[v] (l\a\k) at ($(a\a)+(\t:1.65)$) {}; \draw (a\a)--(m\a\k)--(l\a\k); } } \end{tikzpicture} \qquad \begin{tikzpicture}[scale=0.8] \node[v,afive] (a) at (0,0) {}; \node[cen] (p) at (0,-1.3) {}; \draw[dashed] (a)--(p); \foreach \k in {0,...,4} { \pgfmathsetmacro{\t}{30+30*\k} \node[v] (m\k) at (\t:0.9) {}; \node[v] (l\k) at (\t:1.7) {}; \draw (a)--(m\k)--(l\k); } \node at (0,-2.0) {\small $T=\tfrac{621}{64}=\rho^{11}$}; \end{tikzpicture} \caption{Left: the spider $A_5^{3}$ on 34 vertices (centre drawn open). For large $n$ the maximizer looks like this, a centre carrying many five-cherry arms; small sizes are more varied, and at $n=34$ itself the maximizer is $C^8A_8$. Right: the five-cherry arm $A_5$, an 11-vertex pendant subtree whose matching weight is exactly $\rho^{11}$. It is the unique pendant subtree attaining the sharp bound of \cref{thm:sharp}.} \label{fig:spider} \end{figure} \begin{theorem}[main theorem]\label{thm:main} For every $n\ge4$ the tree $\mathrm{bgMax}(n)$ below has $n$ vertices and maximizes $\pi$ over all trees on $n$ vertices. \begin{enumerate} \item For $n\ge 492$, put $s=6(n-1)\bmod 11$. The centre of $\mathrm{bgMax}(n)$ carries only arms, and all of them are $A_5$ except: \begin{itemize} \item $s\in\{1,2,3,4\}$: $s$ arms are $A_6$; except that for $s=3$ with $n\le722$ and for $s=4$ with $n\le 2319$, instead $11-s$ arms are $A_4$; \item $s\in\{5,\dots,10\}$: $11-s$ arms are $A_4$. \end{itemize} \item For $4\le n\le 491$, $\mathrm{bgMax}(n)$ is the spider listed in \cref{app:table}. \end{enumerate} For $n\le3$ there is only one tree on $n$ vertices. \end{theorem} The recipe is easier to remember than it looks. An $A_5$ has 11 vertices, an $A_4$ has 9 and an $A_6$ has 13. After the centre there are $n-1$ vertices to distribute, and $n-1\equiv2s\pmod{11}$. Each $A_6$ used in place of an $A_5$ adds $2$ modulo 11 and each $A_4$ subtracts $2$, so $s$ copies of $A_6$, or $11-s$ copies of $A_4$, exactly absorb the remainder (\cref{tab:rule}). The theorem says which of the two ways wins. The two late switches at $n=722$ and $n=2319$ are genuine: they are where two very close competitors trade places (\cref{fig:race}). \begin{table}[h]\centering\small \begin{tabular}{@{}l|ccccccccccc@{}} \toprule $s=6(n-1)\bmod 11$ & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10\\ \midrule non-$A_5$ arms & none & $A_6$ & $A_6^2$ & $A_6^3$ & $A_6^4$ & $A_4^6$ & $A_4^5$ & $A_4^4$ & $A_4^3$ & $A_4^2$ & $A_4$\\ until the switch & & & & $A_4^8$ & $A_4^7$ & & & & & & \\ & & & & \scriptsize($n\le722$) & \scriptsize($n\le2319$) & & & & & & \\ \bottomrule \end{tabular} \caption{The rule of \cref{thm:main} for $n\ge492$, class by class. All other arms are $A_5$, and the centre carries no cherries or leaves.} \label{tab:rule} \end{table} \paragraph{Why five cherries.} The number $\rho=(621/64)^{1/11}\approx1.22948$ is the exact exponential growth rate of the maximum. \begin{theorem}[growth rate]\label{thm:growth} For every $n\ge1$, $\displaystyle \frac{64}{621}\,\rho^{n}\ \le\ \max_{|T|=n}\pi(T)\ \le\ 2\,\rho^{\,n-1}.$ \end{theorem} The upper bound comes from a sharp inequality for pendant subtrees (\cref{thm:sharp}): every pendant subtree $b$ contributes a factor at most $\rho^{|b|}$, with equality only for the five-cherry arm. So each vertex of a tree can contribute at most a factor $\rho$ to $\pi$, and only vertices inside five-cherry arms achieve it. A maximizer therefore uses as many five-cherry arms as the arithmetic of $n$ allows, and all the difficulty is in the lower-order terms. For comparison, Pant's families grow like $(3/2)^{n/2}\approx1.2247^{n}$, just below $\rho$. \subsection{How the proof goes} The proof has three layers. \begin{enumerate}[label=(\alph*)] \item \emph{Algebra.} For a tree, the permanent of the Laplacian is a weighted count of matchings, and a cavity recursion computes it from the leaves up (\cref{sec:matching,sec:cavity}). \item \emph{Reduction to spiders.} Rooting a tree at a vertex of maximum degree, we show that any tree which is not a spider is strictly beaten by some spider with the same number of vertices (\cref{sec:reduction}). The engine is the sharp inequality of \cref{sec:ceiling}, refined into per-vertex inequalities that measure how much each non-spider feature costs. \item \emph{Optimization over spiders.} Spiders form an explicit family with a closed-form value. We solve the optimization over it exactly (\cref{sec:spiders}). \end{enumerate} Each layer is split by size, because different arguments are efficient in different ranges (\cref{fig:map}): \begin{center}\small \begin{tabular}{@{}lp{0.42\textwidth}p{0.33\textwidth}@{}} \toprule $n$ & reduction to spiders & best spider \\ \midrule $4$--$6$ & \multicolumn{2}{p{0.78\textwidth}}{exact rational evaluation of every tree} \\ $7$--$149$ & envelope certificate (degree $\le 23$) + high-degree theorem & table sweep \\ $150$--$491$ & credited rate cells + high-degree theorem & table sweep \\ $\ge 492$ & rate cells + high-degree theorem & exchange lemmas + 223 polynomial certificates \\ \bottomrule \end{tabular} \end{center} \subsection{How to read this paper} The mathematics is presented in the usual way, with proofs or proof outlines. Alongside it, shaded paragraphs marked \textbf{In Lean} say where each step lives in the formal development, what the formal statement is, and why it is organized the way it is. A reader interested only in the mathematics can skip them. A reader who wants to audit the formal proof should read them together with \cref{sec:lean}, which spells out exactly what the Lean theorem says, and with the reading guide \texttt{formalization/READING\_GUIDE.md} in the repository. \paragraph{Status.} Every step is formalized in Lean~4~\cite{Lean4} with Mathlib~\cite{Mathlib} and checked by the Lean kernel. The headline theorems depend only on \lean{propext}, \lean{Classical.choice} and \lean{Quot.sound}, with no \lean{sorry}, no \lean{native\_decide} and no added axioms. The result has not yet been refereed. The kernel certifies the deductions. What a reader must still check is that the formal statement says what we claim it says, and \cref{sec:lean} is written to make that check easy. The work was carried out with extensive help from an AI system (see the acknowledgements). Partly for that reason we have tried to make every claim checkable by machine and every certificate reproducible from scratch. \begin{figure}[tbp]\centering \begin{tikzpicture}[font=\small, stage/.style={box,fill=coolsoft,text width=27mm}, lean/.style={font=\scriptsize\ttfamily,text=black!60,align=center}, arr/.style={-{Stealth[length=2mm]}}] \node[box,fill=soft,text width=70mm] (all) at (0,0) {every tree $T$ on $n$ vertices}; \node[box,text width=70mm] (root) at (0,-1.1) {reroot at a vertex of maximum degree $k$}; \node[stage] (hi) at (-5.4,-2.9) {$k\ge24$\\ tangent envelope:\\ non-atoms lose $\ge\frac1{75}$}; \node[stage] (e) at (-1.8,-2.9) {$k\le23$\\ $7\le n\le149$\\ envelope certificate}; \node[stage] (m) at ( 1.8,-2.9) {$k\le23$\\ $150\le n\le491$\\ credited rate cells}; \node[stage] (r) at ( 5.4,-2.9) {$k\le23$\\ $n\ge492$\\ linear deficit}; \node[lean,anchor=north] (lhi) at (hi.south) {BGSpiderReduction\\BGSpiderCells\\BGHighDegreeSmall}; \node[lean,anchor=north] (le) at (e.south) {BGEnvCert/*\\(57 G149 shards)}; \node[lean,anchor=north] (lm) at (m.south) {BGSpiderMid*}; \node[lean,anchor=north] (lr) at (r.south) {BGSpiderLowDegree}; \node[box,fill=soft,text width=70mm] (sp) at (0,-5.7) {every maximizer is a spider (\cref{thm:reduction})}; \node[stage,text width=40mm] (tab) at (-2.6,-7.2) {$n\le491$: kernel sweep of\\ every balanced spider}; \node[stage,text width=46mm] (rule) at (2.9,-7.2) {$n\ge492$: structure +\\ 223 polynomial certificates}; \node[lean,anchor=north] at (tab.south) {BGSpiderTable*}; \node[lean,anchor=north] at (rule.south) {BGSpiderStruct, BGSpiderCand*}; \node[stage,text width=20mm] (tiny) at (-6.2,-7.2) {$4\le n\le6$\\ every tree\\ evaluated}; \node[lean,anchor=north] at (tiny.south) {BGMaximizerTiny}; \node[box,fill=soft,text width=70mm] (ans) at (0,-9.4) {$\mathrm{bgMax}(n)$ maximizes $\pi$ for every $n\ge4$}; \node[lean,anchor=north] at (ans.south) {BGMaximizerAll.bg\_maximizer\_all}; \draw[arr] (all)--(root); \foreach \x in {hi,e,m,r} {\draw[arr] (root.south) -- (\x.north);} \foreach \x in {lhi,le,lm,lr} {\draw[arr] (\x.south) -- (sp.north);} \draw[arr] (sp)--(tab); \draw[arr] (sp)--(rule); \draw[arr] ($(tab.south)+(0,-0.4)$) -- (ans.north); \draw[arr] ($(rule.south)+(0,-0.4)$) -- (ans.north); \draw[arr] ($(tiny.south)+(0,-0.4)$) |- (ans.west); \end{tikzpicture} \caption{The proof at a glance, with the Lean modules that carry each step. The top half shows that every maximizer is a spider, the bottom half finds the best spider, and \lean{BGMaximizerAll} joins the ranges.} \label{fig:map} \end{figure} %===================================================================================================== \section{From permanents to matchings}\label{sec:matching} %===================================================================================================== The first step is classical, and it is what makes the problem tractable at all: for a tree, the permanent of the Laplacian collapses to a sum over matchings. \begin{theorem}[\cite{BG1984,Pant2026}]\label{thm:matchsum} For a tree $T$, \[ \per L(T)=\sum_{M}\ \prod_{v\notin V(M)}\deg v, \qquad\text{hence}\qquad \pi(T)=\sum_{M}\ \prod_{uv\in M}\frac{1}{\deg u\,\deg v}, \] the sums running over all matchings $M$ of $T$, including the empty one, and $V(M)$ denoting the set of matched vertices. \end{theorem} \begin{proof} A term $\prod_i L_{i,\sigma(i)}$ of the permanent is nonzero only if every $i$ is fixed by $\sigma$ or sent to a neighbour. The non-trivial cycles of $\sigma$ then run along edges of $T$. Since $T$ has no cycles, they are transpositions along edges, that is, a matching $M$. A fixed point contributes $L_{ii}=\deg i$ and a matched edge contributes $L_{ij}L_{ji}=(-1)(-1)=1$. Dividing by $\prod_v\deg v$ gives the second formula. \end{proof} So $\pi(T)$ is a \emph{weighted matching count}: every matching contributes the product, over its edges, of $1/(\deg u\deg v)$. The empty matching contributes $1$; single edges contribute a little each; larger matchings contribute products of these small numbers (\cref{fig:matching}). In statistical-physics language, $\pi$ is the partition function of a monomer-dimer system in the sense of Heilmann and Lieb~\cite{HL1972}, with a dimer on edge $uv$ carrying activity $1/(\deg u\deg v)$. \begin{figure}[htbp]\centering \begin{tikzpicture}[scale=1.0] \node[cen,label=below:{\scriptsize 3}] (c) at (0,0) {}; \node[v,label=below:{\scriptsize 2}] (a1) at (-1.3,0) {}; \node[v,label=below:{\scriptsize 1}] (a2) at (-2.6,0) {}; \node[v,label=below:{\scriptsize 2}] (b1) at (1.3,0) {}; \node[v,label=below:{\scriptsize 1}] (b2) at (2.6,0) {}; \node[v,label=right:{\scriptsize 1}] (l) at (0,1.2) {}; \draw (a2)--(a1)--(c)--(b1)--(b2); \draw (c)--(l); \draw[line width=2.4pt,afive,opacity=0.75] (a2)--(a1); \draw[line width=2.4pt,afive,opacity=0.75] (c)--(l); \draw[line width=2.4pt,afive,opacity=0.75] (b1)--(b2); \node[align=left,font=\small,anchor=west] at (3.3,0.4) {weight of this matching\\ $=\dfrac{1}{1\cdot2}\cdot\dfrac{1}{3\cdot1}\cdot\dfrac{1}{2\cdot1}=\dfrac1{12}$}; \node[align=left,font=\small,anchor=west] at (3.3,-1.0) {$\pi(T)=\sum_M(\text{weight of }M)=\dfrac{7}{2}$}; \end{tikzpicture} \caption{The spider $C^2A_0$ on six vertices (centre open, degrees shown by each vertex) and one of its matchings. Each matched edge $uv$ contributes $1/(\deg u\deg v)$. Summing over all 12 matchings, including the empty one, gives $\pi(T)=\per L(T)/\prod\deg v=7/2$.} \label{fig:matching} \end{figure} Two consequences are worth drawing out. First, $\per L(T)$ is not hard to compute for trees: \cref{thm:matchsum} and the recursion of the next section compute it in linear time. Every value in this paper is an exact rational that anyone can recompute. Second, the maximization problem now has a clear tension. A matched edge is worth more when its endpoints have small degree, but small degrees mean few edges, and every edge incident to a vertex raises that vertex's degree and so lowers the weight of all its other edges. The maximizer resolves this tension in a surprisingly rigid way. \begin{inlean} This is \lean{pi\_eq\_msum} in \lean{Matching.lean}, proved for any finite acyclic simple graph with Mathlib's \lean{Matrix.permanent}. It is the only place where the permanent enters the formal proof. Everything afterwards works with the matching sum, called \lean{Aobj}, and the bridge theorem \lean{pi\_utree} in \lean{R47Tree.lean} says that for the trees of the formalization \lean{Aobj t} equals $\per L/\prod\deg$ of the realized graph. That is how the final theorem can be stated literally for the permanent (\cref{sec:lean}). \end{inlean} %===================================================================================================== \section{The cavity recursion}\label{sec:cavity} %===================================================================================================== Matching sums on trees can be computed from the leaves upward. This is the ``cavity method'' of statistical physics (see, e.g., Mézard and Montanari~\cite{MM2009}); on a tree it is exact, and it is the workhorse of the whole proof. \paragraph{Planted branches.} A \emph{planted branch} $b$ is a rooted tree whose root will be attached to one further vertex, its parent. Degrees are always measured in the final tree, so the root of $b$ has degree $d_b=(\text{number of children})+1$. Let $T_b$ be the matching sum of \cref{thm:matchsum} restricted to edges of $b$, and $T^{\circ}_b$ the same sum over matchings that leave the root of $b$ unmatched. The ratio \[ y_b=\frac{T^{\circ}_b}{d_b\,T_b} \] is the \emph{message} that $b$ sends to its parent: it measures how available the root of $b$ is to be matched upward, per unit of its degree. Splitting the matchings of $b$ according to whether, and to which child, the root is matched gives the recursion \begin{equation}\label{eq:cavity} T_b=\Big(\prod_{c}T_c\Big)\frac{d_b+R_b}{d_b},\qquad y_b=\frac{1}{d_b+R_b},\qquad R_b=\sum_c y_c, \end{equation} where the products and sums run over the children $c$ of the root (\cref{fig:cavity}). Indeed $T^{\circ}_b=\prod_cT_c$, and matching the root to child $c$ contributes $\frac{1}{d_bd_c}T^{\circ}_c\prod_{c'\neq c}T_{c'}=\frac{y_c}{d_b}\prod_{c'}T_{c'}$. A leaf has $T=1$ and $y=1$. For a tree rooted at a vertex with $k$ children, the same computation with $d=k$ (the root has no parent) gives \begin{equation}\label{eq:root} \pi(T)=\Big(\prod_{c}T_c\Big)\Big(1+\frac{R}{k}\Big),\qquad R=\sum_c y_c . \end{equation} Since \eqref{eq:cavity} multiplies in one factor per vertex, a useful rewriting is \begin{equation}\label{eq:logsum} \log T_b=\sum_{v\in b}\log\Big(1+\frac{R_v}{d_v}\Big). \end{equation} \begin{figure}[htbp]\centering \begin{tikzpicture}[scale=1] \node[v,label=left:{\small $v$}] (v) at (0,0) {}; \node[cen] (p) at (0,1.2) {}; \node[font=\small,anchor=west] at (0.2,1.2) {parent}; \draw[dashed] (v)--(p); \foreach \x/\lab in {-2.4/1,-0.8/2,2.4/k} { \coordinate (c\lab) at (\x,-1.3); \draw (v)--(c\lab); \draw[fill=coolsoft] (c\lab)--++(-0.6,-1.2)--++(1.2,0)--cycle; \node[v] at (c\lab) {}; \node[font=\scriptsize] at ($(c\lab)+(0,-1.5)$) {$(T_{c_\lab},\,y_{c_\lab})$}; } \node at (0.8,-1.9) {$\cdots$}; \draw[-{Stealth},afive,thick] (3.6,-1.8)--(3.6,0.2); \node[align=left,font=\small,anchor=west] at (3.8,-0.8) {$T_v=\prod_c T_c\cdot\dfrac{d_v+R_v}{d_v}$\\[4pt] $y_v=\dfrac{1}{d_v+R_v}$\\[4pt] $R_v=\sum_c y_c,\quad d_v=k+1$}; \end{tikzpicture} \caption{The cavity recursion. Each child subtree summarizes itself by a weight $T$ and a message $y$, and the vertex combines them. The whole tree's ratio is the same combination at the root, with $d=k$ because the root has no parent.} \label{fig:cavity} \end{figure} \paragraph{Atoms.} Iterating \eqref{eq:cavity} on the smallest pieces: \begin{center}\small \begin{tabular}{@{}lccc@{}} \toprule piece & vertices & weight $T$ & message $y$\\ \midrule leaf $A_0$ & 1 & $1$ & $1$\\ cherry & 2 & $3/2$ & $1/3$\\ arm $A_j$ & $2j+1$ & $(3/2)^j\,\frac{4j+3}{3(j+1)}$ & $\frac{3}{4j+3}$\\ \bottomrule \end{tabular} \end{center} For the arm, the arm vertex has degree $j+1$ and receives $R=j/3$ from its $j$ cherries. In particular \[ T(A_5)=\Big(\frac32\Big)^5\cdot\frac{23}{18}=\frac{243}{32}\cdot\frac{23}{18}=\frac{621}{64}, \] and the arithmetic identity $27\cdot23=621$ hidden in this line will reappear as the reason the extremal structure is exactly tight. Which piece gives the most weight per vertex? \Cref{fig:rates} plots $\log T(A_j)/(2j+1)$. A cherry gives $\tfrac12\log\tfrac32\approx0.2027$ per vertex. Arms do better, and the best is $A_5$, at $0.2065862$, with $A_4$ ($0.2064721$) and $A_6$ ($0.2064696$) just behind. As $j$ grows the arm approaches the cherry value, because the arm vertex itself becomes a negligible fraction of the arm. This small plot already contains the answer's shape: use $A_5$'s wherever possible, and fix the remainder with the nearly-as-good $A_4$ and $A_6$. What the plot does \emph{not} show, and what makes the problem hard, is that the root factor $1+R/k$ in \eqref{eq:root} also depends on the messages: arms with larger $y$ (smaller arms) help the root. The rule in \cref{thm:main} is the outcome of that competition. \begin{figure}[htbp]\centering \begin{tikzpicture} \begin{axis}[width=0.78\textwidth,height=5.4cm,xlabel={$j$ (cherries on the arm)}, ylabel={$\log T(A_j)/(2j+1)$},xmin=0.5,xmax=15.5,ymin=0.185,ymax=0.2095, xtick={1,...,15},yticklabel style={/pgf/number format/fixed,/pgf/number format/precision=3}, grid=major,grid style={black!10},tick label style={font=\scriptsize},label style={font=\small}] \addplot[mark=*,mark size=1.6pt,afour,thick] table[x=j,y=rate] {rates.dat}; \addplot[dashed,black!60,domain=0.5:15.5] {0.2027326}; \node[font=\scriptsize,anchor=north east] at (axis cs:15.3,0.2025) {cherry: $\tfrac12\log\tfrac32$}; \addplot[dotted,afive,thick,domain=0.5:15.5] {0.2065862}; \node[font=\scriptsize,afive,anchor=south] at (axis cs:5,0.2068) {$A_5$: $\log\rho$}; \end{axis} \end{tikzpicture} \caption{Weight per vertex of the arm $A_j$. The five-cherry arm is the unique maximum, and its value $\log\rho$ is the growth rate of the maximum of $\pi$ (\cref{thm:growth}). The arms $A_4$ and $A_6$ trail it by about $10^{-4}$, and long arms tend to the cherry value.} \label{fig:rates} \end{figure} \begin{inlean} The formalization has two models of trees and a bridge between them. \lean{UTree} (file \lean{R47Tree.lean}) is the ``real'' tree: a rooted tree that can be realized as a Mathlib \lean{SimpleGraph}, which is where the permanent lives. \lean{BGSCL.Branch} is a lightweight copy designed for recursion, and \lean{BGSCL.cav} computes the pair $(T^{\circ}_b,T_b)$ by \eqref{eq:cavity}; \lean{bY} is the message and \lean{piRoot} is \eqref{eq:root}. The translation \lean{fromU} from \lean{UTree} to \lean{Branch} and the theorem \lean{Aobj\_eq\_piRoot} (file \lean{BGMaximizer.lean}) say that computing with the lightweight model gives the true matching sum. Why two models? Proofs about permanents need a graph with a vertex type; proofs by recursion and by kernel computation need a plain inductive type with no graph attached. Keeping them separate, and proving once that they agree, keeps both kinds of proof simple. \end{inlean} %===================================================================================================== \section{The sharp ceiling and the growth rate}\label{sec:ceiling} %===================================================================================================== Write $\Fs=\tfrac1{11}\log\tfrac{621}{64}=\log\rho$ and, for a planted branch $b$ with $|b|$ vertices, \[ \bell(b)=\log T_b-|b|\,\Fs . \] Think of $\bell(b)$ as the \emph{profit} of the branch: its log-weight minus the best possible log-weight for its size. The central inequality says profit is never positive. \begin{theorem}[sharp ceiling]\label{thm:sharp} Every planted branch $b$ satisfies $T_b\le\rho^{|b|}$, that is $\bell(b)\le0$, with equality if and only if $b$ is the five-cherry arm $A_5$. \end{theorem} \subsection{Subactions: paying for a vertex with its children's credit} By \eqref{eq:logsum}, the profit is a sum of local terms, \[ \bell(b)=\sum_{v\in b}e_v,\qquad e_v=\log\Big(1+\frac{R_v}{d_v}\Big)-\Fs . \] Some vertices have $e_v>0$ (a vertex whose children send it large messages does well locally) and some have $e_v<0$ (a leaf has $e=-\Fs$). A term-by-term bound is hopeless. Instead we look for a \emph{potential} $\varrho\ge0$ on vertices, depending only on a vertex's local state, such that \begin{equation}\label{eq:sub} e_v+\varrho(v)\ \le\ \sum_{c\text{ child of }v}\varrho(c)\qquad\text{for every vertex }v. \end{equation} Read \eqref{eq:sub} as a budget: each vertex may run a local profit $e_v$, but must pay for it out of the credit $\varrho(c)$ banked by its children, and must also bank credit $\varrho(v)$ for its own parent. Summing \eqref{eq:sub} over all vertices of $b$, each $\varrho(v)$ appears once on the left and once on the right (at its parent), except the root's, so everything telescopes (\cref{fig:telescope}): \[ \bell(b)=\sum_ve_v\ \le\ -\varrho(\mathrm{root})\ \le\ 0 . \] In the language of ergodic optimization such a $\varrho$ is a \emph{subaction}~\cite{Bousch2001,Jenkinson2019}; its existence is the discrete analogue of finding a calibrating potential for an optimal orbit. \begin{figure}[htbp]\centering \begin{tikzpicture}[scale=1.0, lab/.style={font=\scriptsize,fill=white,inner sep=1pt}] \node[v] (r) at (0,0) {}; \node[v] (a) at (-2.8,-1.5) {}; \node[v] (b) at (0,-1.5) {}; \node[v] (c) at (2.8,-1.5) {}; \node[v] (a1) at (-3.8,-3.0) {}; \node[v] (a2) at (-1.8,-3.0) {}; \node[v] (c1) at (2.8,-3.0) {}; \draw (r)--(a) (r)--(b) (r)--(c) (a)--(a1) (a)--(a2) (c)--(c1); \node[lab,anchor=south] at (r.north) {$e_r+\varrho(r)\le\varrho(a)+\varrho(b)+\varrho(c)$}; \node[lab,anchor=south east] at (a.north west) {$e_a+\varrho(a)\le\varrho(a_1)+\varrho(a_2)$}; \node[lab,anchor=south west] at (c.north east) {$e_c+\varrho(c)\le\varrho(c_1)$}; \node[lab,anchor=north] at (a1.south) {$e_{a_1}+\varrho(a_1)\le0$}; \node[lab,anchor=north] at (a2.south) {$e_{a_2}+\varrho(a_2)\le0$}; \node[lab,anchor=north] at (b.south) {$e_{b}+\varrho(b)\le0$}; \node[lab,anchor=north] at (c1.south) {$e_{c_1}+\varrho(c_1)\le0$}; \node[font=\small,align=center] at (0,-4.2) {add them up: every $\varrho$ except the root's cancels, so $\sum_ve_v\le-\varrho(r)\le0$}; \end{tikzpicture} \caption{Why a subaction proves the ceiling. Each vertex's inequality pays its local profit $e_v$ out of its children's credit; summed over the tree, the credits cancel along every edge.} \label{fig:telescope} \end{figure} \paragraph{The witness.} Remarkably, a very simple potential works. Writing $y$ for a vertex's message and grouping vertices by their number of children, \[ \varrho_{\mathrm{wit}}= \begin{cases} \Fs & \text{leaf},\\[1pt] 2\Fs-\log\tfrac32+\tfrac14\big(y-\tfrac13\big) & \text{one child},\\[1pt] \tfrac1{32}\,y & \text{two children},\\[1pt] \tfrac1{384}\,y & \text{three children},\\[1pt] 0 & \text{four or more children}. \end{cases} \] Three instances of \eqref{eq:sub} are equalities, and they are exactly the three kinds of vertex in $A_5$: \begin{itemize} \item a leaf: $e=-\Fs$ and $\varrho=\Fs$, so $e+\varrho=0$; \item the middle vertex of a cherry (one leaf child, message $1/3$): $e+\varrho=(\log\tfrac32-\Fs)+(2\Fs-\log\tfrac32)=\Fs=\varrho(\text{leaf})$; \item the arm vertex with five cherries ($d=6$, $R=5/3$, $\varrho=0$): $e=\log\tfrac{23}{18}-\Fs$, and the children's credit is $5(2\Fs-\log\tfrac32)$. These agree exactly when $11\Fs=\log\big(\tfrac{23}{18}(\tfrac32)^5\big)=\log\tfrac{621}{64}$, which is the definition of $\Fs$. \end{itemize} Every other instance of \eqref{eq:sub} holds with room to spare. Checking that is a finite computation once one notices that \eqref{eq:sub} only involves a vertex and its children's local states. Large degrees need no case split: a vertex with four or more children carries no credit itself, and a single tangent-line bound on $\log(1+R/d)$ settles all of them at once. The verification splits into cells by degree and by ranges of the children's messages; in each cell the inequality compares a rational envelope against a rational enclosure of a logarithm. \paragraph{Equality.} If $\bell(b)=0$ then every inequality along $b$ is tight. Tightness at the root forces degree six, and at degree six it forces all five children to be cherries: a single non-cherry child makes the cell strict. The strictness needs the numerical fact $2\Fs-\log\tfrac32<\tfrac1{96}$, which follows from $\log x\tfrac3{23}=y(A_5)$). \begin{figure}[htbp]\centering \begin{tikzpicture}[scale=0.75] \begin{scope} \node[cen] (o) at (0,0) {}; \foreach \ang in {90,160,230} { \node[v] (a) at (\ang:1.3) {}; \draw (o)--(a); \foreach \k in {-1,0,1} {\draw (a)--++(\ang+35*\k:0.6) node[v]{} --++(\ang+35*\k:0.5) node[v]{};} } \node[v,asix] (x) at (330:1.3) {}; \draw (o)--(x); \node[v,asix] (x1) at ($(x)+(330:0.8)$) {}; \draw[asix] (x)--(x1); \foreach \k in {-1,0,1} {\draw[asix] (x1)--++(330+40*\k:0.6) node[v,asix]{} --++(330+40*\k:0.5) node[v,asix]{};} \draw[asix] (x)--++(260:0.6) node[v,asix]{}; \node[font=\small,align=center] at (0,-2.9) {not a spider: one branch\\ is not an atom}; \end{scope} \draw[-{Stealth},thick] (3.0,0)--(4.4,0) node[midway,above,font=\small] {beaten by}; \begin{scope}[xshift=7.5cm] \node[cen] (o) at (0,0) {}; \foreach \ang in {90,162,234,306} { \node[v] (a) at (\ang:1.3) {}; \draw (o)--(a); \foreach \k in {-1,0,1} {\draw (a)--++(\ang+35*\k:0.6) node[v]{} --++(\ang+35*\k:0.5) node[v]{};} } \draw (o)--(18:1.2) node[v]{} --(18:1.9) node[v]{}; \node[font=\small,align=center] at (0,-2.9) {a spider on the\\ same number of vertices}; \end{scope} \end{tikzpicture} \caption{The reduction. Rooted at a vertex of maximum degree, a tree is a spider exactly when every branch at the root is an atom (leaf, cherry or arm). A non-atom branch (highlighted) always costs more profit than it can return through the root bonus, so some spider of the same size does strictly better.} \label{fig:reduction} \end{figure} The argument then splits by the root degree $k$ and by $n$. \subsection{High degree: $k\ge24$} When the root has many children, the root bonus $\log(1+S/k)$ is nearly linear in $S$ over the relevant range. Replace it by its tangent line at the spider value $S/k=3/23$ (\cref{fig:tangent}). The slope prices each unit of message at $\mu=\tfrac{23}{26k}\le\tfrac{23}{624}$, and the profit identity becomes a sum over branches of \[ V_\mu(b)=\bell(b)+\mu\,y_b, \] a branch's profit plus the market value of its message. On this range of prices we show that $A_5$ maximizes $V_\mu$ over all branches, and that every non-atom lies below it by at least $\tfrac1{75}$. (The closest non-atom competitor is a vertex carrying five cherries and one $A_4$: it falls $0.0145$ below at $\mu=0$ and $0.0152$ below at the largest price $\mu=\frac{23}{624}$.) So a tree with a non-atom branch has $\log\pi-(n-1)\Fs\le\log\tfrac{26}{23}-\tfrac1{75}$, which is below the benchmark \eqref{eq:floor} because $\tfrac1{75}>\tfrac{10}{960}$. \begin{figure}[htbp]\centering \begin{tikzpicture} \begin{axis}[width=0.62\textwidth,height=5cm,xlabel={$S/k$},ylabel={root bonus}, xmin=0,xmax=0.4,ymin=0,ymax=0.36,grid=major,grid style={black!10}, tick label style={font=\scriptsize},label style={font=\small}, xtick={0,0.1,0.130434,0.2,0.3,0.4},xticklabels={0,0.1,$\frac3{23}$,0.2,0.3,0.4}] \addplot[thick,afour,domain=0:0.4,samples=60] {ln(1+x)}; \addplot[dashed,afive,domain=0:0.4] {ln(26/23)+(23/26)*(x-3/23)}; \addplot[only marks,mark=*,mark size=1.8pt,afive] coordinates {(0.130434,0.122602)}; \node[font=\scriptsize,afour,anchor=north west] at (axis cs:0.27,0.22) {$\log(1+S/k)$}; \node[font=\scriptsize,afive,anchor=south east] at (axis cs:0.33,0.30) {tangent: price per unit of $S$}; \end{axis} \end{tikzpicture} \caption{The high-degree argument replaces the concave root bonus by its tangent at the spider value $S/k=3/23$, which can only overestimate it. The bonus then becomes linear, and each branch can be judged on its own: its profit plus the value of its message at a fixed price.} \label{fig:tangent} \end{figure} \begin{inlean} The envelope statement reduces, through the subaction of \cref{sec:ceiling}, to three per-vertex inequalities (\lean{surchargeCore\_proved}, \lean{atomCell0Core\_proved}, \lean{atomCellMuCore\_proved}) in \lean{BGSpiderCells.lean}, proved with 22 rational tangent certificates and degree-six Taylor enclosures of $\log$; the tightest margin is $7.3\cdot10^{-4}$. The result is \lean{spider\_dominates\_highDegree\_uncond} for $n\ge91$. For $25\le n\le90$ the benchmark \eqref{eq:floor} is too weak, so \lean{BGHighDegreeSmall.highDegree\_small} compares instead with the exact best spider from the table of \cref{sec:spiders}, one kernel-checked inequality per $n$. \end{inlean} \subsection{Low degree and large $n$: linear deficits} When $k\le23$ the tangent trick is too crude, and we use size instead. A tree with a non-atom branch should lose profit in proportion to its size, while the root bonus is bounded. We strengthen the subaction inequality \eqref{eq:sub} by a small fixed rate $\alpha$ per vertex. A \emph{rate cell} with degree cap $D$ and rate $\alpha$ is a per-vertex inequality which, telescoped exactly as in \cref{fig:telescope}, yields a \emph{linear deficit} \[ \bell(b)+\varrho_{\mathrm{wit}}(b)\ \le\ -\alpha|b|\qquad\text{for every non-atom branch }b \text{ with at most }D-1\text{ children per vertex.} \] Atoms are exempt, because $A_5$ has zero profit and cannot lose anything. Then \[ \log\pi-(n-1)\Fs\ \le\ R_k-\alpha(n-1), \] where $R_k$ bounds what the root can gain; it is computed separately for each root degree $k$, one root cell per degree. The bound falls under the benchmark floor $\log\frac{26}{23}-\frac1{96}$ once $n-1>(R_k-\log\frac{26}{23}+\frac1{96})/\alpha$. The largest root constant, $R_2\approx0.3194$, does not matter, because its rate $\frac1{135}$ is large. The binding case is root degree $6$, where $R_6\le0.2447$ with $\alpha=\frac1{3700}$ requires $n-1\ge491$ (at $n-1=490$ the inequality fails by $6.6\cdot10^{-5}$), while degrees $7$ to $23$ need at most $n-1\ge464$ and degrees $2$ to $5$ at most $n-1\ge298$. That is where the threshold $492$ comes from. \begin{center}\small \begin{tabular}{@{}lccccc@{}} \toprule root degree $k$ & $6$--$23$ & $5$ & $4$ & $3$ & $2$\\ cap $D$ & $23$ & $5$ & $4$ & $3$ & $2$\\ rate $\alpha$ & $1/3700$ & $1/2100$ & $1/660$ & $1/420$ & $1/135$\\ \bottomrule \end{tabular} \end{center} \begin{inlean} \lean{BGSpiderLowDegree.lean}: 32 rate cells and 22 root cells, each a tangent certificate with rational envelopes (tightest margin $2.8\cdot10^{-4}$), assembled into \lean{spider\_dominates\_lowDegree\_uncond}. \lean{BGMax.bg\_spider\_reduction} in \lean{BGMaximizer.lean} combines both degree ranges with the rerooting lemma \lean{exists\_maxRooted} for every $n\ge492$. \end{inlean} \subsection{Low degree, $150\le n\le491$: rate cells with credits} Below $492$ the linear deficit is not yet large enough, and we sharpen it in two ways. First, in a tree of maximum degree $\le D$ every message satisfies $y\ge 1/(2D-1)$, which narrows the range of messages each cell must handle. Second, non-atom branches carry a \emph{credit} $\kappa$ depending on their number of children, $\bell(b)+\varrho_{\mathrm{wit}}(b)\le-\alpha|b|-\kappa(b)$, which they pass up to the root. The root is then bounded by an explicit knapsack over atoms, certified separately for each pair $(k,n)$. The comparison spiders are the $A_5/A_4$ benchmark for $n\ge275$; for $150\le n\le274$ the benchmark is too weak, and the comparison uses spiders $C^cA_5^aA_4^q$ that also carry a few cherries at the centre. \begin{inlean} \lean{BGSpiderMid.lean} proves the generic credited telescoping. The generated files \lean{BGSpiderMidCellsD2}--\lean{D23} (cells, one file per cap) and \lean{BGSpiderMidRootK2}--\lean{K23} (root knapsacks, one file per root degree) are the certificates. \lean{BGSpiderMidFinal.lean} assembles \lean{spider\_dominates\_of\_maxDegreeRoot\_150}, and \lean{BGMax.maximizer\_is\_spider\_150} states the result for every $n\ge150$. \end{inlean} \subsection{Low degree, $7\le n\le149$: the envelope certificate} For small trees a uniform rate is far too weak, so we compute instead. The object computed is a \emph{Bellman envelope}: a table $w(m,g)$ that bounds, for every branch of size $m$, its profit plus the value of its message at price $\mu_g$, where the prices run over a grid (\cref{fig:envelope}). Fix a rational rate $f$ close to $\Fs$ (it cancels between a tree and a spider of the same size; the certificate uses $f=28392988613/2^{37}$ and the prices $\mu_g=(g+1)/200$ for $0\le g<100$), put $V_{\mu}(b)=\log T_b-|b|f+\mu y_b$, and consider a vertex with its children. The function $x\mapsto\log x+\mu/x$ is concave on the relevant range, so its tangent bounds $V_\mu$ at the vertex by a constant plus $\sum_cV_{\nu}(c)$ at a new price $\nu$. In words: a vertex's value at price $\mu$ is controlled by its children's values at a price that the vertex determines. The children's sizes add up to $m-1$, so the best total over children is a max-plus knapsack over sizes. A table that satisfies all these knapsack inequalities is a valid envelope by induction on size, and the proof needs only that finitely many table inequalities hold. \begin{figure}[htbp]\centering \begin{tikzpicture}[scale=0.9] \foreach \i in {0,...,6} \foreach \j in {0,...,4} { \pgfmathsetmacro{\sh}{15+8*\j} \fill[afour!\sh] (\i*0.5,\j*0.45) rectangle ++(0.5,0.45); } \draw[black!40,xstep=0.5,ystep=0.45] (0,0) grid (3.5,2.25); \draw (0,0) rectangle (3.5,2.25); \node[font=\small,below] at (1.75,0) {size $m$}; \node[font=\small,rotate=90,above] at (0,1.12) {price $\mu_g$}; \node[font=\small,above] at (1.75,2.3) {envelope table $w(m,g)$}; \fill[afive] (3.0,0.9) rectangle ++(0.5,0.45); \draw[-{Stealth},thick] (3.8,1.1)--(5.0,1.1); \begin{scope}[xshift=6.4cm,yshift=1.9cm] \node[v,afive,label=above:{\small entry $(m,g)$}] (p) at (0,0) {}; \foreach \x/\s in {-1.3/m_1,0/m_2,1.3/m_3} { \draw (p)--(\x,-1.1); \draw[fill=coolsoft] (\x,-1.1)--++(-0.4,-0.8)--++(0.8,0)--cycle; \node[font=\scriptsize] at (\x,-2.15) {$w(\s,\nu)$}; } \node[font=\small,align=left,anchor=west] at (1.9,-0.9) {tangent step + knapsack:\\[2pt] $w(m,g)\ \ge\ \text{const}+\!\!\max\limits_{m_1+m_2+\cdots=m-1}\sum_i w(m_i,\nu)$}; \end{scope} \end{tikzpicture} \caption{The envelope certificate. A table indexed by branch size and price is valid if every entry dominates the tangent-step bound computed from smaller entries; induction on size then bounds every branch. The table for $n\le149$ is stored in fixed point and checked entry by entry by the Lean kernel.} \label{fig:envelope} \end{figure} We cover root degrees $2\le k\le23$, using separate tables for caps $C\in\{1,\dots,8,12,16,22\}$ on the number of children of a vertex (so vertex degree at most $C+1$); roots of degree $\ge24$ are handled by the high-degree argument. The final root inequality, with at least one non-atom child, is compared against certified lower bounds for explicit spiders. \begin{inlean} This is the most computation-heavy part of the proof, and its organization is dictated by how the Lean kernel evaluates. The theory is in \lean{BGEnvCert/}: \lean{Tangent} (the tangent step), \lean{Envelope} (the induction on size), \lean{Sound} (a passing Boolean check implies the real inequalities), \lean{Spider} (certified spider values) and \lean{AssembleK} (combining the caps). The data is in \lean{BGEnvCert/G149/}: 57 generated files. Tables are fixed point with 34 fractional bits, packed as lanes of large natural numbers, and each check is a Boolean function evaluated by \lean{decide +kernel}. The file \lean{MainK} assembles them into \lean{envcertK}, and \lean{BGMaximizerSmall.maximizer\_is\_spider\_small} gives the result for $7\le n\le149$. \Cref{sec:telperion} explains why the data is split the way it is. \end{inlean} \subsection{The smallest trees, and the summary} For $4\le n\le6$ there are few enough trees to evaluate every one exactly over $\mathbb{Q}$. The maximizers are the paths $P_4,P_5,P_6$, which are spiders; the formal proof checks that the tabled spider is optimal at these sizes. \begin{theorem}\label{thm:reduction} For every $n\ge7$, every tree on $n$ vertices that maximizes $\pi$ is, after rerooting at a vertex of maximum degree, a spider. For $n\ge492$ every tree on $n$ vertices is weakly beaten by a spider on $n$ vertices. \end{theorem} \begin{inlean} \lean{BGMaximizerTiny.lean} enumerates trees for $n\le6$ by a fuel-bounded structural recursion (the kernel does not efficiently unfold well-founded recursion) and evaluates them with a $\mathbb{Q}$ copy of the cavity recursion, \lean{cavQ}, proved equal to the real one by \lean{cavQ\_cast}. The three range theorems of \cref{thm:reduction} are \lean{maximizer\_is\_spider\_small}, \lean{maximizer\_is\_spider\_150} and \lean{bg\_spider\_reduction}. Existence of a maximizer at each size, which the argument needs, is \lean{BGMaximizerMid.exists\_max\_tree}: there are finitely many trees on $n$ vertices. \end{inlean} %===================================================================================================== \section{The best spider}\label{sec:spiders} %===================================================================================================== We now optimize over spiders. By \eqref{eq:root} and the table of atoms, a spider's value has a closed form, and the problem becomes a question about integers. \subsection{The closed form and the balance identity} A spider is described up to isomorphism by the multiset of its centre's children, and \[ F=\Big(\frac32\Big)^{c+\sum j}\prod_{\text{arms}}\alpha_j\cdot\Big(1+\frac{c/3+\sum b_j}{D}\Big), \qquad \alpha_j=\frac{4j+3}{3(j+1)},\quad b_j=\frac{3}{4j+3}, \] where $c$ is the number of cherries at the centre, the product and sum run over the arms (leaves being $A_0$, with $\alpha_0=b_0=1$), and $D$ is the degree of the centre. The first factor is fixed by $n$ up to the number of arms, so the optimization is a balance between the arm factors $\alpha_j$ and the bracket. \begin{lemma}[balance]\label{lem:balance} Put $Q_\kappa(x,y)=\alpha_x\alpha_y(\kappa+b_x+b_y)$. For integers $k,t\ge0$, \[ Q_\kappa(k+t+1,k+1)-Q_\kappa(k+t+2,k)=\frac{(t+1)\big((\kappa-3)(8k+4t+15)+3\big)}{9(k+1)(k+2)(k+t+2)(k+t+3)}. \] Consequently, if $D\ge3$, moving a cherry from an arm to an arm at least two smaller strictly increases $F$, and in every maximizer with $D\ge3$ all arm sizes (leaves included) differ by at most one. \end{lemma} \begin{proof} The move (\cref{fig:balance}) keeps $n$, $D$ and the power of $\tfrac32$, and multiplies $F$ by $Q_\kappa(\text{new})/Q_\kappa(\text{old})$ with $\kappa=D+R_0\ge3$, where $R_0$ is the message sum of the other children. The right side of the identity is then positive. The identity itself is a polynomial identity in $k,t,\kappa$. \end{proof} \begin{figure}[htbp]\centering \begin{tikzpicture}[scale=0.8] \newcommand{\arm}[4]{% \node[v,#4] (A) at (#1,#2) {}; \foreach \k in {1,...,#3} { \pgfmathsetmacro{\t}{90+(\k-(#3+1)/2)*24} \draw (A)--++(\t:0.6) node[v]{} --++(\t:0.45) node[v]{}; } } \begin{scope} \node[cen] (o) at (0,-1.2) {}; \draw (o)--(-1.3,0); \draw (o)--(1.3,0); \arm{-1.3}{0}{6}{afive} \arm{1.3}{0}{2}{afour} \node[font=\small] at (0,-1.9) {$A_{6}$ and $A_{2}$}; \draw[-{Stealth},afive,thick] (-0.9,1.35) to[bend left=35] node[above,font=\scriptsize]{move one cherry} (1.0,1.35); \end{scope} \draw[-{Stealth},thick] (3.0,-0.3)--(4.3,-0.3) node[midway,above,font=\small] {$F$ increases}; \begin{scope}[xshift=7.3cm] \node[cen] (o) at (0,-1.2) {}; \draw (o)--(-1.3,0); \draw (o)--(1.3,0); \arm{-1.3}{0}{5}{afive} \arm{1.3}{0}{3}{afour} \node[font=\small] at (0,-1.9) {$A_{5}$ and $A_{3}$}; \end{scope} \end{tikzpicture} \caption{The balance move of \cref{lem:balance}, shown with $k=2$, $t=2$ (the centre's other children are not drawn). Whenever the centre has at least three children, evening out two arms whose sizes differ by two or more strictly increases the ratio. So a best spider has all its arms of two consecutive sizes.} \label{fig:balance} \end{figure} Two further exact exchanges are used: two leaves at the centre are never better than one cherry, and a general local-exchange criterion that is affine in $R_0$, and so reduces to checking two quadratics in the number $D_0$ of other children. \begin{inlean} \lean{BGSpiderOpt.lean} models a spider as a list of children with the closed-form value \lean{F} over $\mathbb{Q}$ and proves \lean{balance\_identity}, \lean{F\_balance\_lt}, \lean{balanced\_of\_isMax} and \lean{F\_leafpair\_lt}; the general exchange criterion \lean{F\_exchange\_lt} is in \lean{BGSpiderStruct.lean}. The link to real trees is \lean{BGSpiderRule.Aobj\_spiderU}: for the tree \lean{spiderU l} built from a child list \lean{l}, \lean{Aobj} equals \lean{F l}. \end{inlean} \subsection{Sizes up to 491: a kernel sweep} By \cref{lem:balance}, a maximizer with $D\ge3$ is determined by four numbers $(c,s,a,b)$: $c$ cherries, $a$ arms $A_s$ and $b$ arms $A_{s+1}$. For each $n$ there are at most about thirty thousand such configurations ($30{,}135$ at $n=491$), plus the configurations with $D\le2$. Each value has an explicit integer numerator and denominator. For each $n\le491$ the kernel compares every candidate against the table entry by a cross-multiplied inequality of natural numbers. At $n=21$ two non-isomorphic spiders tie ($C^{10}$ and $C^3A_3^2$); the table records $C^3A_3^2$. The table also shows how varied small maximizers are. Below $n=46$ arms of every size from one to eight appear, with up to nine cherries at the centre (at $n=19$). From $n=46$ on every arm is an $A_4$, $A_5$ or $A_6$, but a few cherries remain at the centre until $n=333$, and the $A_4$/$A_6$ choice keeps shifting until $n=2319$. \begin{inlean} \lean{BGSpiderTable.lean} proves the soundness of the check (\lean{spider\_opt\_of\_check}); the table itself is \lean{BGSpiderTableData.tabData}, and the 46 generated files \lean{BGSpiderTableChunk\_*} run the check for between three and $130$ sizes each (the first covers $4\le n\le133$), as small kernel declarations for each $n$ (the table value, blocks of rows, and the remaining cases) glued into the check for that $n$; \lean{BGSpiderTableAll.spider\_opt\_table} assembles them. The table rows are printed in \cref{app:table}, generated from the Lean file itself. \end{inlean} \subsection{Sizes from 492: structure, then 223 certificates} For large $n$ a sweep is impossible, so we argue. Let $l$ be a spider maximizing $F$ with $n\ge492$. A sequence of exchanges pins down its shape: \begin{enumerate} \item the centre has at least three children (otherwise a global bound shows it is far from optimal); \item no arm $A_j$ has $j\ge13$: split it into $A_{j-11}$ and two $A_5$'s; \item no arm has $7\le j\le12$: trade eleven $A_j$'s for $2j+1$ copies of $A_5$, and compare globally with the rule spider; \item at most eight cherries: nine cherries lose to two $A_4$'s; \item no arm has $j\le3$; \item hence every arm is $A_4$, $A_5$ or $A_6$; by balance $A_4$ and $A_6$ never occur together; and there are at most ten of each. \end{enumerate} The global comparison uses the identity $(\prod T)^2=(3/2)^{n-1}\prod h$ with $h(\text{cherry})=1$ and $h(A_j)=\tfrac23\alpha_j^2$; its tightest instance is $24.45<28.43$. What remains is a finite list of shapes whose sizes grow with $n$. A candidate is determined by its counts $(c,k_4,k_5,k_6)$, and \[ F=\Phi(c,k_4,k_5,k_6)=\Big(\frac32\Big)^{c}G_4^{k_4}G_5^{k_5}G_6^{k_6} \Big(1+\frac{c/3+k_4B_4+k_5B_5+k_6B_6}{c+k_4+k_5+k_6}\Big) \] with $G_4=\tfrac{513}{80}$, $G_5=\tfrac{621}{64}$, $G_6=\tfrac{6561}{448}$, $B_4=\tfrac3{19}$, $B_5=\tfrac3{23}$, $B_6=\tfrac19$. The triple $(c,k_4,k_6)$ fixes the residue class $s$, hence the rule winner's counts. After dividing out a common power of $G_5$, the comparison $\Phi(\text{candidate})\le\Phi(\text{winner})$ becomes $P(m)\ge0$ for an explicit quadratic $P$ in the common number $m$ of five-cherry arms. There are 189 triples and 223 certificates. 221 of them write $P(L+t)$ with nonnegative coefficients in $t$, which is visibly positive for every $t\ge0$. The other two, the competitions that decide the thresholds $722$ and $2319$, write it in the Bernstein basis on a bounded interval, because there the rival really does win outside the interval (\cref{fig:race}). \begin{figure}[htbp]\centering \begin{tikzpicture} \begin{groupplot}[group style={group size=2 by 1,horizontal sep=16mm}, width=0.48\textwidth,height=5cm,xlabel={$n$},grid=major,grid style={black!10}, tick label style={font=\scriptsize},label style={font=\small},title style={font=\small}, scaled x ticks=false] \nextgroupplot[title={$s=3$: $A_4^8$ against $A_6^3$},ylabel={$10^6\,(F_{A_4}/F_{A_6}-1)$}, xmin=550,xmax=1000,ymin=-1000,ymax=1150] \addplot[only marks,mark=*,mark size=1pt,afour] table[x=n,y=d] {race_s3.dat}; \draw[black!60] (axis cs:550,0)--(axis cs:1000,0); \draw[dashed,afive] (axis cs:727.5,-1000)--(axis cs:727.5,1150); \node[font=\scriptsize,afive,anchor=west] at (axis cs:740,800) {switch: $722\mid733$}; \nextgroupplot[title={$s=4$: $A_4^7$ against $A_6^4$}, xmin=1600,xmax=3000,ymin=-250,ymax=520] \addplot[only marks,mark=*,mark size=0.8pt,afour] table[x=n,y=d] {race_s4.dat}; \draw[black!60] (axis cs:1600,0)--(axis cs:3000,0); \draw[dashed,afive] (axis cs:2324.5,-250)--(axis cs:2324.5,520); \node[font=\scriptsize,afive,anchor=west] at (axis cs:2350,380) {switch: $2319\mid2330$}; \end{groupplot} \end{tikzpicture} \caption{The two late switches in the rule. In residue classes $s=3$ and $s=4$ the maximizer uses $A_4$'s until the relative advantage of $A_6$'s, which grows slowly with $n$, overtakes it. The margins are tiny: at the last size before each switch the $A_4$ spider wins by $2.0\cdot10^{-5}$ and $3.6\cdot10^{-6}$ in relative terms. The two Bernstein-basis certificates prove these signs exactly on each side.} \label{fig:race} \end{figure} \begin{inlean} \lean{BGSpiderStruct.structProp\_492} proves the shape constraints (the local exchanges close by \lean{nlinarith} once certain quadratics are shown positive). \lean{BGSpiderCandBase.lean} defines $\Phi$ and $P$. The generated files \lean{BGSpiderCandCells0}--\lean{8} hold the certificates, one file per cherry count, each checked by \lean{ring} (the identity) and \lean{norm\_num} (the signs), and \lean{BGSpiderCand.candProp\_492} assembles the 189 cases. \lean{BGSpiderRule.bg\_maximizer\_of} combines these with the reduction, and \lean{BGMaximizerFinal.bg\_maximizer} is the theorem for $n\ge492$. \end{inlean} Together, \cref{thm:reduction} and this section prove \cref{thm:main}. %===================================================================================================== \section{What exactly the Lean theorem says}\label{sec:lean} %===================================================================================================== The main theorem in Lean is \begin{verbatim} theorem R3Cert.BGMaximizerAll.bg_maximizer_all (n : Nat) (h4 : 4 <= n) : usize (bgMax n) = n /\ forall t : UTree, usize t = n -> Aobj t <= Aobj (bgMax n) \end{verbatim} and its companion \lean{bg\_maximizer\_all\_perm} states the same inequality for the permanent of the Laplacian divided by the product of degrees, computed on the realized graphs. The proof of \lean{bg\_maximizer\_all} is a ten-line case split on $n$ that calls the four range theorems. What a reader must trust is not that proof (the kernel checked it) but the definitions it is about: \begin{itemize} \item \lean{UTree} is the type of finite rooted trees, built by \lean{node} from a list of subtrees, and \lean{usize} counts vertices. Every finite tree, rooted anywhere, is a \lean{UTree}; rerooting is handled inside the proof, so the quantifier really ranges over all trees. \item \lean{Step3.realize (dtRealize t)} turns $t$ into an explicit edge list, and \lean{aGraph} turns that into a Mathlib \lean{SimpleGraph} on its vertex type. \item \lean{lapl G} is the matrix with $\deg i$ on the diagonal, $-1$ on edges and $0$ elsewhere, and \lean{Matrix.permanent} is Mathlib's permanent. \item \lean{Aobj t} is the weighted matching sum of the realized tree, and \lean{pi\_utree} proves that it equals \lean{(lapl (aGraph ...)).permanent} divided by the product of the degrees. \item \lean{bgMax n} is \lean{spiderU (tab n)} for $n\le491$ and \lean{spiderU (W n)} otherwise, where \lean{tab} reads the table \lean{BGSpiderTableData.tabData} and \lean{W} implements the rule of \cref{thm:main}. \end{itemize} So \lean{bg\_maximizer\_all\_perm} states: for every $n\ge4$ and every tree $t$ on $n$ vertices, $\per L/\prod\deg$ of $t$ is at most that of $\mathrm{bgMax}(n)$, with the permanent and the degrees read off the actual graph. The file \lean{AxiomGuard.lean} prints the axioms of the 20 headline theorems. A \lean{sorry} anywhere in their dependencies would appear there as \lean{sorryAx}, and a \lean{native\_decide} as \lean{Lean.ofReduceBool}. \paragraph{The same theorem in Mathlib's vocabulary.} Because \lean{UTree} and \lean{Aobj} are ours, the repository also states the result using only Mathlib's definitions on the graph side, in the file \texttt{formalization/Statement.lean}: \begin{verbatim} theorem brualdi_goldwasser_upper (n : Nat) (h4 : 4 <= n) {V : Type} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] (hG : G.IsTree) (hV : Fintype.card V = n) : (G.lapMatrix R).permanent / (prod v, (G.degree v : R)) <= (F (bgChildren n) : R) \end{verbatim} together with \lean{brualdi\_goldwasser\_attained}: some tree on \lean{Fin n} has ratio exactly \lean{F (bgChildren n)}. Here \lean{IsTree}, \lean{lapMatrix} (degree matrix minus adjacency matrix), \lean{Matrix.permanent} and \lean{degree} are Mathlib's, and the only definitions of ours a reader must check are the closed form \lean{F} of \cref{sec:spiders} and the list of the centre's children \lean{bgChildren n} (the table for $n\le491$, the rule for $n\ge492$). The bridge is three short modules: \lean{TreePaths} proves that every Mathlib tree is isomorphic to the path graph of a \lean{UTree} of the same size (by removing a leaf, using Mathlib's \lean{IsTree.exists\_vert\_degree\_one\_of\_nontrivial}, and re-attaching it as a new last child); \lean{TreeBridge} proves that this path graph is the realized graph; and \lean{BGStatement} proves that the Laplacian ratio is invariant under graph isomorphism and assembles the two theorems. \paragraph{Uniqueness.} The theorem above gives \emph{a} maximizer. That it is unique up to isomorphism (except at $n=21$, where exactly two non-isomorphic trees attain the maximum) was first established by exact computation for $n\le491$ (\cref{sec:indep}) and for $n\ge2320$ by an exact rational certificate. It is now also formalized, in the separate library \texttt{formalization/BGUnique}, and checked by Lean's kernel (\lean{bg\_maximizer\_unique\_mathlib} for $n\ne21$ and \lean{bg\_maximizers\_21\_mathlib} for $n=21$, stated with Mathlib's \lean{IsTree}, \lean{lapMatrix} and graph isomorphism). A Comparator challenge for it is in the repository: Comparator confirms that the solution proves exactly the challenge's statements with the standard axioms, but its kernel replays were not completed, so no second-kernel verdict is claimed for uniqueness. %===================================================================================================== \section{Certificates and Telperion}\label{sec:telperion} %===================================================================================================== Most of the proof's bulk is data: envelope tables, rate-cell constants, table rows, polynomial coefficients. We produce it with generators written in Python using exact integer and rational arithmetic, and we never trust the generators. Each certificate is a Lean file whose checks the kernel evaluates, so a wrong certificate is simply a failed build. \begin{figure}[htbp]\centering \begin{tikzpicture}[node distance=6mm,font=\small,arr/.style={-{Stealth[length=2mm]},thick}] \node[box,fill=black!5] (gen) {generator\\ \scriptsize Python, exact arithmetic}; \node[box,fill=black!5,right=of gen] (cert) {certificate\\ \scriptsize tables, constants,\\ \scriptsize polynomials}; \node[box,fill=black!5,right=of cert] (file) {Lean file\\ \scriptsize data + checks}; \node[box,fill=soft,right=14mm of file] (ker) {Lean kernel\\ \scriptsize evaluates, type-checks}; \node[box,fill=coolsoft,below=9mm of cert] (frz) {frozen record\\ \scriptsize hashes, byte-for-byte diff}; \draw[arr] (gen)--(cert); \draw[arr] (cert)--(file); \draw[arr] (file)--(ker); \draw[arr,dashed] (cert)--(frz); \begin{scope}[on background layer] \node[draw=black!40,dashed,rounded corners,fit=(gen)(cert)(file)(frz),inner sep=6pt, label={[font=\scriptsize,text=black!60]above:untrusted: a bug here can only cause a failed build}] {}; \node[draw=afive,thick,rounded corners,fit=(ker),inner sep=6pt, label={[font=\scriptsize,text=afive]above:trusted}] {}; \end{scope} \end{tikzpicture} \caption{The certificate pipeline. Only the kernel is trusted. The frozen record lets anyone regenerate a family from scratch and confirm that the Lean files in the repository are exactly what the generator produces.} \label{fig:pipeline} \end{figure} The certificates are packaged with Telperion, a pipeline built on exactly that division of labour: an untrusted \emph{emitter} produces a certificate, a small adapter renders it as Lean, and the Lean kernel is the only trusted component (\cref{fig:pipeline}). For each certificate family the repository contains the generator, a \emph{frozen} copy of its output with hashes, and a driver that regenerates the family from scratch and compares it byte for byte, both with the frozen copy and with the files in the formalization: \begin{center}\small \begin{tabular}{@{}lrl@{}} \toprule family & Lean files & content \\ \midrule \texttt{spider\_table} & 48 & table rows and the per-$n$ sweep, $n\le491$ \\ \texttt{envcert\_g149} & 57 & envelope tables, tangents, spider bounds, $7\le n\le149$ \\ \texttt{mid\_cells} & 45 & credited rate cells and root knapsacks, $150\le n\le491$ \\ \texttt{cand\_certs} & 10 & the 223 polynomial certificates, $n\ge492$ \\ \bottomrule \end{tabular} \end{center} The byte-for-byte check matters for review. A reader does not have to read 57 files of packed integers; it is enough to read the generator, run it, and see that it reproduces the files the kernel checked. And even that is only needed to understand the proof, not to trust it: the kernel's verdict does not depend on how the data was produced. \paragraph{Making the kernel do it.} Three facts about the Lean kernel shaped the certificates. \begin{enumerate}[label=(\roman*)] \item The kernel unfolds definitions by well-founded recursion very slowly, so every recursive check is structural, with an explicit fuel parameter. \item It does not share the evaluation of repeated argument subterms: a loop state used twice is evaluated twice, and a chain of such loops blows up. We emit literal constants, and force evaluation of natural numbers before passing them on (\lean{BGEnvCert.Force}). \item Arithmetic in $\mathbb{Q}$ is slow in the kernel, so large checks use natural numbers and fixed point, and only small ones use $\mathbb{Q}$. \end{enumerate} We use \lean{decide +kernel} and never \lean{native\_decide}, so the compiler is not trusted. Because the kernel keeps every intermediate term of a declaration in memory, large checks are split into many small theorems and many files, and a unifying file assembles them. Even so, the heaviest files need up to about $63$\,GB each. The sharding is what makes the proof checkable on a single large workstation. %===================================================================================================== \section{Independent computations}\label{sec:indep} %===================================================================================================== None of the following is needed for the Lean proof. They are independent checks of the answer by entirely different methods. \begin{itemize} \item \emph{Certified search, $n\le491$.} A bottom-up search over all rooted trees, with no degree cap, storing every quantity as an outward-rounded interval and discarding a partial state only when it is provably strictly beaten in every completion. Surviving candidates are re-evaluated in exact rational arithmetic. For every $n\le491$ the exact maximum equals the table value, and \emph{every} maximizing tree is a spider. (952\,s on one core.) \item \emph{Brute force.} Exact enumeration of all non-isomorphic trees agrees for $n\le18$. \item \emph{A second kernel.} The repository contains a challenge/solution pair for the Lean FRO's Comparator~\cite{Comparator}: the challenge states \lean{brualdi\_goldwasser\_upper} and \lean{brualdi\_goldwasser\_attained} with \lean{sorry} and imports only the definitions of the answer. Comparator checks that the solution proves exactly those statements, using only the three standard axioms, and replays the exported proof both in Lean's kernel and in nanoda~\cite{nanoda}, an independent implementation of the Lean kernel in Rust. This check has passed twice. On 27 September 2026, at commit \texttt{295d0ac}, both kernels accepted the solution (5.1 hours, 63\,GB peak memory). On 8 October 2026 it was re-run at commit \texttt{a77678d}, after the spider-table checks were split into small per-$n$ kernel declarations, and both kernels again accepted the solution (2.7 hours, 56\,GB peak memory). Both runs were on macOS, where Comparator's Linux sandbox was replaced by a pass-through shim, and Comparator has not yet been run in CI. These results refer to the proof terms of the two commits named; every later commit is checked by Lean's kernel in the ordinary build. \item \emph{Spider optimization.} An exhaustive exact optimization over the spider family for $n\le2400$, together with an exact rational certificate for $n\ge2320$, agrees with the table and the rule; an exact Pareto dynamic programme over the family with no balance assumption agrees for $n\le600$. \end{itemize} %===================================================================================================== \section{Discussion}\label{sec:discussion} %===================================================================================================== \Cref{thm:main} answers the question Brualdi and Goldwasser asked. In this section we look at what the answer says: about the shape of extremal trees, about the size of the maximum, about where the problem sits among extremal problems on trees, and about permanents and methods more generally. We end with what remains open. Unless stated otherwise, everything below is a consequence of \cref{thm:main} and the closed form of \cref{sec:spiders}; the few statements that go beyond it are labelled as questions or heuristics. \subsection{The shape of the maximizer} \paragraph{One hub, bounded depth.} Every maximizer is a spider, so every vertex is within distance three of the centre and the diameter is at most $6$. (Among the maximizers in \cref{app:table} and those given by the rule, the diameter is exactly $6$ once the centre carries two arms with cherries.) This is a sharp contrast with the permanent itself: Brualdi and Goldwasser showed that $\per L(T)$ is largest for the path, whose diameter is $n-1$. Dividing by $\prod_v\deg v$ does not merely rescale the problem; it moves the extremal trees from maximal diameter to bounded diameter. At the other end, the minimum of $\pi$ is attained by the star~\cite{BG1984}. So both extremes of the Laplacian ratio have a single hub: the star, whose hub carries leaves, and the spider of five-cherry arms, whose hub carries second-level hubs. \paragraph{The degree profile.} For large $n$ the maximizer is made of $\lfloor(n-1)/11\rfloor-O(1)$ copies of the eleven-vertex block $A_5$, plus at most ten defect arms $A_4$ or $A_6$. Its degree sequence is therefore, up to $O(1)$ vertices: about $5n/11$ leaves, about $5n/11$ vertices of degree $2$, about $n/11$ vertices of degree $6$, and a single vertex, the centre, of degree about $n/11$. Exactly one vertex has unbounded degree. The degree-$6$ vertices are where the optimization happens: an arm vertex with $j$ cherries balances the number of cherries it collects against the degree it pays for them, and $j=5$ is the unique best balance (\cref{fig:rates}). \paragraph{Rigidity.} For large $n$ the maximizer is a star of identical blocks with a bounded number of defects, and the defects are dictated by $n\bmod11$. This is the typical shape of answers in ergodic optimization, where an optimal orbit is periodic and a subaction certifies it~\cite{Bousch2001,Jenkinson2019}, and indeed that is how the growth-rate proof works: the potential $\varrho_{\mathrm{wit}}$ is tight exactly on the three vertex types of the optimal block (\cref{sec:ceiling}). \paragraph{Why the problem resisted guesses.} The earlier conjectures were natural extrapolations from small trees, and \cref{app:table} shows why that is treacherous. For small $n$ the maximizer wanders through arms of many sizes, with many cherries at the centre. It settles into $A_4$'s, $A_5$'s and $A_6$'s only at $n=46$, keeps a few centre cherries until $n=333$, and the choice between $A_4$'s and $A_6$'s keeps changing until $n=2319$. The Wu--Dong--Lai formulas are exactly right up to $n=22$ (and for even $n$ up to $34$), so the conjecture was well supported by the data one could reasonably compute by hand; it simply described a regime that ends early. \subsection{The size of the maximum} \Cref{thm:growth} pins the growth rate but leaves a factor of about $16$ between its lower and upper constants. \Cref{thm:main} removes it: the maximum is known exactly for every $n$, and its normalized value converges along each residue class. \begin{corollary}\label{cor:constant} Let $\rho=(621/64)^{1/11}$, and put \[ \delta_4=\frac{T(A_4)}{\rho^{9}}=\frac{513/80}{\rho^{9}}\approx0.9989741,\qquad \delta_6=\frac{T(A_6)}{\rho^{13}}=\frac{6561/448}{\rho^{13}}\approx0.9984859 . \] \begin{enumerate} \item For every $n\equiv1\pmod{11}$ with $n\ge254$, \[ \max_{|T|=n}\pi(T)=\frac{26}{23}\Big(\frac{621}{64}\Big)^{(n-1)/11}. \] \item For each residue $s=6(n-1)\bmod11$, as $n\to\infty$ within the class, \[ \frac{\max_{|T|=n}\pi(T)}{\rho^{\,n-1}}\ \longrightarrow\ c_s=\frac{26}{23}\,\delta_4^{\,k_4(s)}\,\delta_6^{\,k_6(s)}, \] where $k_6(s)=s$, $k_4(s)=0$ for $1\le s\le4$; $k_4(s)=11-s$, $k_6(s)=0$ for $5\le s\le10$; and $k_4(0)=k_6(0)=0$. In particular \[ \limsup_{n\to\infty}\frac{\max\pi}{\rho^{n-1}}=\frac{26}{23}\approx1.130435,\qquad \liminf_{n\to\infty}\frac{\max\pi}{\rho^{n-1}}=c_5=\frac{26}{23}\delta_4^{\,6}\approx1.123494 . \] \end{enumerate} \end{corollary} \begin{proof} For $n\equiv1\pmod{11}$ we have $s=0$, and for $254\le n\le491$ the table, and for $n\ge492$ the rule, gives the spider $A_5^{k}$ with $k=(n-1)/11$. Its value is $T(A_5)^k(1+y(A_5))=(621/64)^k\cdot\tfrac{26}{23}$, since every arm sends the message $\tfrac3{23}$. For general $s$ and $n\ge2320$ the rule gives $k_4$ arms $A_4$, $k_6$ arms $A_6$ and $k_5$ arms $A_5$ with $n-1=9k_4+11k_5+13k_6$, so \[ \frac{F}{\rho^{\,n-1}}=\delta_4^{k_4}\,\delta_6^{k_6}\Big(1+\frac{k_4\cdot\frac3{19}+k_5\cdot\frac3{23}+k_6\cdot\frac19}{k_4+k_5+k_6}\Big), \] and the bracket tends to $1+\tfrac3{23}=\tfrac{26}{23}$ because $k_4,k_6$ are bounded while $k_5\to\infty$. \end{proof} \begin{table}[h]\centering\footnotesize\setlength{\tabcolsep}{3.2pt} \begin{tabular}{@{}l*{11}{c}@{}} \toprule $s$ & 0 & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10\\ \midrule $c_s$ & 1.13043 & 1.12872 & 1.12701 & 1.12531 & 1.12360 & 1.12349 & 1.12465 & 1.12580 & 1.12696 & 1.12812 & 1.12928\\ \bottomrule \end{tabular} \caption{The limit of $\max\pi/\rho^{n-1}$ in each residue class $s=6(n-1)\bmod11$ (\cref{cor:constant}). These are the eleven levels visible at the right of \cref{fig:ratio}.} \label{tab:cs} \end{table} So the maximum is $c_{s(n)}\rho^{\,n-1}(1+O(1/n))$, with eleven explicit constants, all within $0.7\%$ of each other. The period-$11$ oscillation in \cref{fig:ratio} is exactly this: each class carries a fixed number of defect arms, and each defect costs a factor $\delta_4$ or $\delta_6$, about one part in a thousand. The first part of the corollary is also a pleasant closed form: for $n\equiv1\pmod{11}$ the answer to Brualdi and Goldwasser's question is a single power of a rational number, times $\tfrac{26}{23}$. (The corollary is not stated separately in Lean, but it is a finite computation from the formal theorem and the closed form $F$.) \paragraph{Where the late switches come from.} The two switches in the rule, at $n=722$ and $n=2319$ (\cref{fig:race}), have a simple explanation. In a class $s\in\{1,2,3,4\}$ the remainder can be absorbed either by $s$ arms $A_6$ or by $11-s$ arms $A_4$. In the bulk, the sixes are cheaper: the fours cost $(11-s)\log(1/\delta_4)$ and the sixes cost $s\log(1/\delta_6)$, and for $s\le4$ the former is larger. But fours send larger messages to the centre ($\tfrac3{19}>\tfrac3{23}>\tfrac19$), and the root bonus $\log(1+R/D)$ rewards that by an amount proportional to $1/D$, where $D\approx n/11$ is the centre degree. So the fours win while $D$ is small and lose once the bonus has decayed below the bulk difference. Equating the two to first order predicts switches near $n\approx738$ for $s=3$ and $n\approx2335$ for $s=4$, against the true switches at $722\mid733$ and $2319\mid2330$; for $s=2$ it predicts about $449$, against the true switch at $423\mid434$ (below $492$, where the table takes over). The heuristic explains the thresholds; the certificates of \cref{sec:spiders} are what prove them. \subsection{Where the problem sits among extremal problems on trees} Many classical tree invariants have the path and the star as their extremal trees. The number of matchings (the Hosoya index), for example, is largest for the path and smallest for the star~\cite{WagnerGutman2010}. Csikvári's generalized tree shift~\cite{Csikvari2010} explains a great deal of this: it is a partial order on trees with the path at the bottom and the star at the top, and many invariants (the number of closed walks, the spectral radius, the Estrada index and others) are monotone along it, so their extremes are forced to be the path and the star. The Laplacian ratio is a weighted count of matchings, but it is not of this kind. Its minimum is the star, the top of the poset; if it were monotone along the poset its maximum would be the path, and it is not. The weight $1/(\deg u\deg v)$ on each matched edge is what breaks monotonicity: it rewards matchings near low-degree vertices, but low degree limits how many edges a vertex can contribute. The result is an extremal tree that is neither a path nor a star, and whose shape depends on $n$ modulo $11$. This suggests a natural family of problems in between. \begin{itemize} \item For $\alpha\ge0$ let $\pi_\alpha(T)=\sum_M\prod_{uv\in M}(\deg u\deg v)^{-\alpha}$. Then $\pi_0$ is the Hosoya index, maximized by the path, and $\pi_1=\pi$ is maximized by spiders of five-cherry arms. How does the maximizer move as $\alpha$ increases from $0$ to $1$ and beyond: through which shapes, and at which values of $\alpha$ does it change? The cavity recursion and the subaction method apply verbatim, with $\log\rho$ replaced by an $\alpha$-dependent rate. \end{itemize} \subsection{A statistical-physics reading} By \cref{thm:matchsum}, $\pi(T)$ is the partition function of a monomer-dimer system on $T$ in which a dimer on the edge $uv$ has activity $1/(\deg u\deg v)$~\cite{HL1972}. In that language, $\log\rho$ is the largest free energy per vertex that any tree can achieve, and \cref{thm:sharp} says the five-cherry arm is its unique ``ground state'': the only pendant structure that achieves it exactly. The maximizer is then a ground-state configuration with the fewest defects that the vertex count allows, and $\log(1/\delta_4)$ and $\log(1/\delta_6)$ are the energies of the two cheapest defects. The subaction $\varrho_{\mathrm{wit}}$ of \cref{sec:ceiling} plays the role that calibrated sub-actions play in Aubry--Mather theory and ergodic optimization~\cite{Bousch2001,Jenkinson2019}: a local certificate that no configuration can beat the ground state. It would be interesting to know how general this is. For which other weighted matching problems on trees, or other tree functionals computed by a cavity recursion, is the extremal tree a periodic arrangement of a single block, certified by a finite piecewise-affine subaction? \subsection{Permanents} The permanent is \#P-hard~\cite{Valiant1979}, and its extremal theory is thin: questions of the form ``which matrix in a natural class maximizes the permanent?'' are often hard even when the class is simple. For Laplacians of trees, the matching-sum formula turns the permanent into a partition function that factorizes over the tree, and that is what made this problem solvable. The same structure applies to other matrix functions of trees built from $D$ and $A$. For example, the signless Laplacian $D+A$ of a tree has the same permanent, since a matched edge contributes $A_{ij}A_{ji}=1$ either way, so \cref{thm:main} answers the analogous question for it too. Immanants of $L$ interpolate between the determinant and the permanent, and orderings of trees by such quantities have been studied~\cite{Csikvari2010}. For graphs with cycles the matching-sum formula no longer holds: a permutation can follow a cycle of the graph, and such terms contribute alongside the matchings. Brualdi and Goldwasser also studied bipartite graphs~\cite{BG1984}, and the maximum of $\per L/\prod\deg$ over connected graphs, or over connected bipartite graphs, on $n$ vertices is a natural next question. Whether cycles help or hurt, and whether an analogue of the sharp ceiling holds, we do not know. \subsection{Method} Most of the proof is a small number of ideas (the cavity recursion, the subaction, tangent envelopes, exchange arguments) applied through a large number of verified inequalities. This is a common shape for extremal results, and such proofs are often hard to check: the ideas are in the paper, but the inequalities are in a computer program that a referee cannot easily audit. Here every inequality is checked by the Lean kernel, and every certificate can be regenerated and compared byte for byte. We think this division, conceptual proof for people and certificate checking for the kernel, is a good model for computer-assisted extremal combinatorics, and the practical lessons of \cref{sec:telperion} (sharding, fixed point, structural recursion) apply well beyond this problem. The method also degrades gracefully: where a uniform argument was too weak (small $n$), it was replaced by a larger certificate rather than by an unchecked computation. A related point concerns how the work was done. Much of the exploration, formalization and certificate engineering was carried out with an AI system. In a project of that kind the natural worry is an error that no one notices. Formal verification changes that: an error in a certificate or a proof step is a failed build, not a hidden mistake. The remaining human responsibility, checking that the definitions and the statement mean what the paper says, is exactly the part that \cref{sec:lean} isolates. \subsection{What remains} \begin{itemize} \item \emph{A conceptual proof of the reduction.} The thresholds $150$, $491$ and $492$ are artefacts of the method. A direct argument that every maximizer is a spider, for all $n$, would be more illuminating than the certificates, and would probably say something about when cavity-recursion optimizers are ``star-shaped''. \item \emph{The interpolating family $\pi_\alpha$.} Which trees maximize $\pi_\alpha$, and where does the maximizer change shape? \item \emph{Constrained versions.} Trees of maximum degree at most $\Delta$ (the rate cells of \cref{sec:reduction} already work under degree caps), trees with a prescribed degree sequence, and trees with a given diameter, the constraint under which the minimum was studied~\cite{Wu2024}. \item \emph{Graphs with cycles.} Bipartite and general connected graphs, as above. \item \emph{Independent review.} The kernel checks the deductions; human review of the statement and the definitions is still needed, and welcome. \end{itemize} \section{Limitations} \begin{itemize} \item The result has not been refereed. The Lean kernel checks the deductions; the correspondence between the formal definitions and the mathematical statement (\cref{sec:lean}) is what a human reviewer should check. \item The proof is long and mostly computational. We do not have a short conceptual proof that the maximizer is a spider, only per-vertex inequalities verified by certificate. \item Uniqueness is checked by Lean's kernel only; the second-kernel check covers the maximum and the maximizer, not uniqueness. \item The trusted base is the Lean kernel, Mathlib's definitions of the permanent and of simple graphs, and our definitions listed in \cref{sec:lean}. \item The full build needs a machine with about $96$\,GB of memory (the heaviest certificate file alone peaks at $63$\,GB) and takes one to two hours on a recent workstation. \end{itemize} \section{Reproducing the results} The repository \url{https://github.com/DrMurphyIsIn/brualdi-goldwasser} contains the Lean project (Lean \texttt{v4.32.0}, Mathlib), the certificate generators with their frozen outputs, the Telperion engine, the source of this paper and a project page with an interactive version of \cref{thm:main} (\url{https://drmurphyisin.github.io/brualdi-goldwasser/}). Releases are archived at Zenodo under the concept DOI \href{https://doi.org/10.5281/zenodo.22983412}{10.5281/zenodo.22983412}, which always resolves to the latest release. The repository also contains a separate small Lean project, \texttt{formalization/cherry}, on a weighted family $\pi_\lambda$ (an extra weight $\lambda$ on every matched edge, $\lambda=1$ being $\pi$); it is not needed for, and does not change, the theorem of this paper. \begin{verbatim} cd formalization && lake exe cache get && ./build.sh lake env lean AxiomGuard.lean lake build BGUnique # uniqueness (a separate library) cd .. # back to the repository root certificates/verify.sh # regenerate all certificates, compare certificates/verify.sh --full # also the certified search, n <= 491 \end{verbatim} The plots in this paper are generated from the same data by \texttt{paper/figdata.py}, and the appendix table by \texttt{paper/gen\_table.py}. \section*{Acknowledgements} The formalization, the certificate generators and much of the exploration were developed with extensive assistance from Claude, an AI system made by Anthropic, working under the author's direction. The author takes responsibility for the content. The correctness of the formal proof rests on the Lean kernel, not on either. \section*{Licensing} Mathematics and Lean code: Apache-2.0. This paper: CC-BY-4.0. The vendored Telperion engine: Business Source License~1.1, free for research, teaching and peer review. \begin{thebibliography}{99} \bibitem{Bousch2001} T.~Bousch, \emph{La condition de Walters}, Ann.\ Sci.\ \'Ec.\ Norm.\ Sup\'er.\ (4) \textbf{34} (2001), 287--311. \href{https://doi.org/10.1016/S0012-9593(00)01062-4}{doi:10.1016/S0012-9593(00)01062-4}. \bibitem{BG1984} R.~A.~Brualdi and J.~L.~Goldwasser, \emph{Permanent of the Laplacian matrix of trees and bipartite graphs}, Discrete Math.\ \textbf{48} (1984), 1--21. \href{https://doi.org/10.1016/0012-365X(84)90127-4}{doi:10.1016/0012-365X(84)90127-4}. \bibitem{Csikvari2010} P.~Csikv\'ari, \emph{On a poset of trees}, Combinatorica \textbf{30} (2010), 125--137. \href{https://doi.org/10.1007/s00493-010-2516-0}{doi:10.1007/s00493-010-2516-0}. \bibitem{Lean4} L.~de~Moura and S.~Ullrich, \emph{The Lean~4 theorem prover and programming language}, in: Automated Deduction -- CADE~28, Lecture Notes in Comput.\ Sci.\ \textbf{12699}, Springer, 2021, 625--635. \bibitem{GHL2010} X.~Geng, X.~Hu and S.~Li, \emph{Further results on permanental bounds for the Laplacian matrix of trees}, Linear Multilinear Algebra \textbf{58} (2010), 571--587. \href{https://doi.org/10.1080/03081080902765583}{doi:10.1080/03081080902765583}. \bibitem{HL1972} O.~J.~Heilmann and E.~H.~Lieb, \emph{Theory of monomer-dimer systems}, Comm.\ Math.\ Phys.\ \textbf{25} (1972), 190--232. \href{https://doi.org/10.1007/BF01877590}{doi:10.1007/BF01877590}. \bibitem{Jenkinson2019} O.~Jenkinson, \emph{Ergodic optimization in dynamical systems}, Ergodic Theory Dynam.\ Systems \textbf{39} (2019), 2593--2618. \href{https://doi.org/10.1017/etds.2017.142}{doi:10.1017/etds.2017.142}. \bibitem{Comparator} Lean FRO, \emph{Comparator}: checking a Lean proof against a separately written statement, \url{https://github.com/leanprover/comparator} (version \texttt{v4.32.0}). \bibitem{Mathlib} The mathlib Community, \emph{The Lean mathematical library}, in: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2020), ACM, 2020, 367--381. \href{https://doi.org/10.1145/3372885.3373824}{doi:10.1145/3372885.3373824}. \bibitem{Merris1994} R.~Merris, \emph{Laplacian matrices of graphs: a survey}, Linear Algebra Appl.\ \textbf{197--198} (1994), 143--176. \href{https://doi.org/10.1016/0024-3795(94)90486-3}{doi:10.1016/0024-3795(94)90486-3}. \bibitem{MRW1981} R.~Merris, K.~R.~Rebman and W.~Watkins, \emph{Permanental polynomials of graphs}, Linear Algebra Appl.\ \textbf{38} (1981), 273--288. \href{https://doi.org/10.1016/0024-3795(81)90026-4}{doi:10.1016/0024-3795(81)90026-4}. \bibitem{MM2009} M.~M\'ezard and A.~Montanari, \emph{Information, Physics, and Computation}, Oxford Graduate Texts, Oxford University Press, 2009. \bibitem{nanoda} C.~Bailey, \emph{nanoda\_lib}: a type checker for the Lean~4 kernel language, \url{https://github.com/ammkrn/nanoda_lib}. \bibitem{Pant2026} P.~Pant, \emph{Counterexamples to a conjecture on Laplacian ratios of trees}, arXiv:2605.14176 (2026). \bibitem{Valiant1979} L.~G.~Valiant, \emph{The complexity of computing the permanent}, Theoret.\ Comput.\ Sci.\ \textbf{8} (1979), 189--201. \href{https://doi.org/10.1016/0304-3975(79)90044-6}{doi:10.1016/0304-3975(79)90044-6}. \bibitem{WagnerGutman2010} S.~Wagner and I.~Gutman, \emph{Maxima and minima of the Hosoya index and the Merrifield--Simmons index: a survey of results and techniques}, Acta Appl.\ Math.\ \textbf{112} (2010), 323--346. \href{https://doi.org/10.1007/s10440-010-9575-5}{doi:10.1007/s10440-010-9575-5}. \bibitem{WDL2025} T.~Wu, X.~Dong and H.-J.~Lai, \emph{Two problems on Laplacian ratios of trees}, Discrete Appl.\ Math.\ \textbf{372} (2025), 224--236. \href{https://doi.org/10.1016/j.dam.2025.04.047}{doi:10.1016/j.dam.2025.04.047}. \bibitem{Wu2024} T.~Wu, X.~Dong, H.-J.~Lai and X.~Zeng, \emph{Solution to an open problem on Laplacian ratio}, Front.\ Math.\ \textbf{21} (2026), no.~4, 815--837. \href{https://doi.org/10.1007/s11464-024-0191-5}{doi:10.1007/s11464-024-0191-5}; arXiv:2402.15669 (2024). \end{thebibliography} \appendix \clearpage \section{The maximizers for $4\le n\le491$}\label{app:table} Notation: $C^{c}$ is $c$ cherries at the centre, $A_j^{m}$ is $m$ arms with $j$ cherries, $L$ a leaf at the centre. The third column is $\pi/\rho^{\,n-1}$, which by \cref{thm:growth} lies in $[\tfrac{64}{621}\rho,\,2]$. At $n=21$, $C^{10}$ ties with the listed tree. Generated from \texttt{BGSpiderTableData.lean} by \texttt{paper/gen\_table.py}. {\small \setlength{\tabcolsep}{4pt} \input{table_maximizers.tex} } \end{document}