π
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| \version "2.24.0" | |
| \header { title = "The Irreducible Story" subtitle = "194 p-adic sections under dihedral interleaving" } | |
| \paper { #(set-paper-size "a3") } | |
| \score { \new Staff \with { midiInstrument = "tubular bells" } { | |
| \clef treble \tempo 4 = 160 | |
| \mark \markup { \box "1: A001379[192] Β· 56 strikes" } | |
| c'''16 c'''16 c'''16 c'''16 fis''16 c'''16 c'''16 c'''16 c'''16 ees'16 c'''16 c'''16 c'''16 c'''16 c'''16 fis16 c'''16 c'''16 c'''16 c'''16 f16 c'''16 c'''16 c'''16 c'''16 c'16 c'''16 c'''16 c'''16 c'''16 bes16 c'''16 c'''16 c'''16 c'''16 g16 c'''16 c'''16 c'''16 c'''16 fis16 c'''16 c'''16 c'''16 c'''16 c'''16 ees'16 c'''16 c'''16 c'''16 c'''16 fis''16 c'''16 c'''16 c'''16 c'''16 | |
| \bar "||" | |
| \mark \markup { \box "2: A001379[174] Β· 55 strikes" } | |
| c'''16 c'''16 c'''16 gis'16 c'''16 c'''16 c'''16 fis''16 c'''16 c'''16 c'''16 d'16 c'''16 c'''16 c'''16 g16 c'''16 c'''16 c'''16 gis'16 c'''16 c'''16 c'''16 fis16 c'''16 c'''16 c'''16 c''16 c'''16 c'''16 c'''16 bes16 c'''16 c'''16 c'''16 gis16 c'''16 c'''16 gis |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| # Fusion 6'Suz:2 (the complementary one) to 3^{1+12}:6'Suz:2 | |
| LibraryFusion( "6.Suz.2", record( name:="3^1+12:6.Suz:2", map:= | |
| [ 1, 76, 18, 5, 8, 89, 85, 11, 54, 240, 26, 81, 31, 80, 39, 95, 46, 93, 51, 117, | |
| 56, 248, 243, 58, 60, 251, 66, 255, 183, 410, 71, 462, 324, 225, 74, 465, 327, | |
| 227, 100, 108, 115, 103, 146, 140, 125, 132, 120, 136, 155, 162, 166, 152, | |
| 300, 178, 498, 394, 322, 190, 414, 191, 424, 419, 194, 205, 440, 217, 354, | |
| 222, 356, 209, 349, 228, 468, 469, 231, 391, 519, 236, 523, 482, 404, 263, | |
| 267, 270, 261, 277, 282, 287, 276, 293, 305, 442, 312, 309, 296, 318, 529, | |
| 487, 454, 490, 525, 458, 533, 335, 476, 333, 479, 343, 472, 376, 380, 371, | |
| 368, 359, 364, 384, 516, 511, 387, 396, 500, 401, 507, 398, 504, 427, 429, |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| mdupont@mdupont-G470:~/2026/07/06/index$ for x in `cat leech_lean.txt`; do echo $x; grep -h ":=" $x; done | sort |uniq -c | sort -rn | |
| 388 type0_count + type2_count + type3_count + type4_count = lambda_mod2_size := by native_decide | |
| 388 theorem type4_positive : type4_count > 0 := by native_decide | |
| 388 theorem short_vectors_double : 2 * type2_count = leech_vectors_norm4 := by native_decide | |
| 388 theorem N0_Nxyz_index : N0_order / Nxyz_order = 6 := by native_decide | |
| 388 theorem lambda_mod2_size_value : lambda_mod2_size = 16777216 := by native_decide | |
| 388 M24_order = 2^10 * 3^3 * 5 * 7 * 11 * 23 := by native_decide | |
| 388 Gx0_order / Nxyz_order = 16584750 := by native_decide | |
| 388 def type4_count : β := 8292375 | |
| 388 def type3_count : β := 8386560 |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "syntaxIdentical": false, | |
| "structurallyEqual": false, | |
| "size": 2, | |
| "proofTag": "independent", | |
| "members": [ | |
| { | |
| "statement": "β {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]\n [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}\n (adj1 : F β£ G) (adj2 : F' β£ G),\n CategoryTheory.CategoryStruct.comp (G.whiskerLeft (adj1.leftAdjointUniq adj2).hom) adj2.counit = adj1.counit", | |
| "namespace": "CategoryTheory.Adjunction", | |
| "name": "CategoryTheory.Adjunction.leftAdjointUniq_hom_counit", |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| { | |
| "syntaxIdentical": false, | |
| "structurallyEqual": true, | |
| "size": 3, | |
| "proofTag": "alias", | |
| "members": [ | |
| { | |
| "statement": "(motive : NameGenerator Γ NameGenerator β Sort u_1) β\n (x : NameGenerator Γ NameGenerator) β ((cngen ngen : NameGenerator) β motive (cngen, ngen)) β motive x", | |
| "namespace": "_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.getChildNgen", | |
| "name": "_private.Lean.Meta.LazyDiscrTree.0.Lean.Meta.LazyDiscrTree.getChildNgen.match_1", |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!DOCTYPE html> | |
| <html lang="en"> | |
| <head> | |
| <meta charset="utf-8"> | |
| <meta name="viewport" content="width=device-width, initial-scale=1"> | |
| <title>The Penteract in the Monster — a 5-cube shadow</title> | |
| <style> | |
| html,body{margin:0;height:100%;background:#05060e;color:#e9e9f3; | |
| font-family:"Segoe UI",system-ui,Helvetica,Arial,sans-serif;overflow:hidden} | |
| #wrap{position:fixed;inset:0} |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| <!DOCTYPE html> | |
| <html lang="en"> | |
| <head> | |
| <meta charset="utf-8"/> | |
| <meta name="viewport" content="width=device-width, initial-scale=1"/> | |
| <title>A Tour of the Monster</title> | |
| <style> | |
| :root { --gold:#ffd23f; --paper:#0c0c14; } | |
| * { box-sizing:border-box; } | |
| html,body { margin:0; height:100%; background:var(--paper); |
Loading
Sorry, something went wrong. Reload?
Sorry, we cannot display this file.
Sorry, this file is invalid so it cannot be displayed.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| " | |
| New Project | |
| History | |
| Aristotle CLI | |
| Docs | |
| Jim Dupont | |
| Settings | |
| Terms of Use |
NewerOlder