/reports/forensics/tables2.md · raw
U1. Dec 2025+ proof kills per commit month: halt/nonhalt and file style
| month | nonhalt | halt | single-machine file | multi-machine file | param/cert | assistant-style header | refs to files not in repo | plain | n/a (certificate/other) |
|---|---|---|---|---|---|---|---|---|---|
| 2025-12 | 79 | 4 | 1 | 50 | 32 | 0 | 0 | 51 | 32 |
| 2026-01 | 10 | 2 | 0 | 9 | 3 | 0 | 0 | 9 | 3 |
| 2026-02 | 77 | 23 | 0 | 58 | 42 | 0 | 0 | 58 | 42 |
| 2026-03 | 52 | 0 | 3 | 42 | 7 | 0 | 0 | 45 | 7 |
| 2026-04 | 0 | 2 | 1 | 1 | 0 | 0 | 0 | 2 | 0 |
| 2026-06 | 9 | 0 | 1 | 0 | 8 | 0 | 0 | 1 | 8 |
| 2026-07 | 25 | 6 | 9 | 15 | 7 | 0 | 0 | 24 | 7 |
| 2026-08 | 34 | 18 | 10 | 33 | 9 | 0 | 3 | 40 | 9 |
| 2026-09 | 175 | 28 | 15 | 172 | 16 | 101 | 17 | 85 | 0 |
| 2026-10 | 12 | 7 | 4 | 15 | 0 | 11 | 7 | 1 | 0 |
U2. Commits since 2025-12-01: what each one added and which list removals it explains
| commit | date | author | message | .v A/M | holdout-universe strings added | list removals explained | nonhalt/halt/eqv | families |
|---|---|---|---|---|---|---|---|---|
| bdf5ff5 | 2025-12-16 | ccz181078 | add TranslatedBellv2,v3,v4, Bouncer_v1, BMO7, Sk17 eqv, upd FARv1,SOC | 13/15 | 73 | 66 | 62/4/0 | CTL/FAR certificates 25; TranslatedBell 10; SOC (shift-overflow counter) 9 |
| d7ae6ec | 2025-12-30 | ccz181078 | add LongLoop | 2/5 | 17 | 17 | 17/0/0 | Longitudinal (LongAcc/LongLoop/LongN) 8; CTL/FAR certificates 6; SOBC 2 |
| 7fd9993 | 2026-01-29 | ccz181078 | 6x2 1326 => 1314, 2x5 75 => 74 | 2/5 | 12 | 12 | 10/2/0 | BLEC 4; misc named mechanism 4; RWLAcc/RRBA (inductive decider certs) 2 |
| 457869d | 2026-02-15 | ccz181078 | add LongAcc, upd LongLoop | 8/9 | 93 | 81 | 58/23/0 | Longitudinal (LongAcc/LongLoop/LongN) 48; SOCSS 17; CTL/FAR certificates 7 |
| 54863c1 | 2026-02-19 | ccz181078 | upd LongLoop | 0/3 | 7 | 7 | 7/0/0 | Longitudinal (LongAcc/LongLoop/LongN) 6; CTL/FAR certificates 1 |
| 83531ba | 2026-02-28 | ccz181078 | upd FARv1 | 0/1 | 12 | 12 | 12/0/0 | CTL/FAR certificates 12 |
| 760fc21 | 2026-03-11 | ccz181078 | add SBCv6a,SOBCv9,SOCSSv2,3,SOMDCv5,Sk1like_TC | 7/4 | 25 | 25 | 25/0/0 | SOCSS 8; CTL/FAR certificates 4; Skelet-like (Sk1/Sk17/SqrtSk17) 4 |
| eb3ecb7 | 2026-03-15 | ccz181078 | add LongLoop3x3v1, upd LongLoop for bbxy | 1/7 | 7 | 7 | 7/0/0 | CTL/FAR certificates 3; Longitudinal (LongAcc/LongLoop/LongN) 3; other: TC 1 |
| 1a7a35f | 2026-03-16 | ccz181078 | add Bouncer2x5v1,SOMDC2x5v2 | 2/1 | 0 | 0 | 0/0/0 | |
| 6f61914 | 2026-03-25 | ccz181078 | add SOCSSv4,5, SOMDCv6, LongLoopv3, optimize bigint ops in LongLoop | 4/1 | 21 | 20 | 20/0/0 | Longitudinal (LongAcc/LongLoop/LongN) 12; SOMDC 6; SOCSS 2 |
| 1f7ce92 | 2026-04-01 | ccz181078 | add BMO3 | 1/0 | 0 | 0 | 0/0/0 | |
| 85ed3a9 | 2026-04-02 | ccz181078 | add BMO3 variant | 0/1 | 0 | 0 | 0/0/0 | |
| 897a653 | 2026-04-07 | ccz181078 | add BigInt | 49/0 | 1 | 1 | 0/1/0 | Bell 1 |
| 64c53c7 | 2026-04-26 | ccz181078 | upd Eqv_Misc | 0/1 | 76 | 40 | 0/0/40 | eqv merge 33; eqv mention 7 |
| a95776a | 2026-04-29 | ccz181078 | upd Eqv_Misc | 0/2 | 25 | 14 | 0/1/13 | eqv merge 10; eqv mention 3; SOBC 1 |
| ecd92a9 | 2026-05-06 | ccz181078 | add extraction of inductive decider | 1/0 | 0 | 0 | 0/0/0 | |
| 6ba3eba | 2026-06-01 | ccz181078 | add some CTL,FAR certs | 1/3 | 14 | 0 | 0/0/0 | |
| 10e149a | 2026-06-15 | ccz181078 | add some FAR certs | 0/2 | 6 | 6 | 6/0/0 | CTL/FAR certificates 6 |
| 4a7ecfa | 2026-06-16 | ccz181078 | add LongN: long. analysis that works when width and height of the defined part --> inf | 1/0 | 1 | 0 | 0/0/0 | |
| e52b811 | 2026-06-30 | ccz181078 | add FIBv4, upd FARv1 (+2 certs) | 1/1 | 3 | 3 | 3/0/0 | CTL/FAR certificates 2; misc named mechanism 1 |
| eb20dbd | 2026-07-02 | ccz181078 | upd SMODCv6 | 0/1 | 2 | 2 | 2/0/0 | SOMDC 2 |
| 895b0f3 | 2026-07-03 | ccz181078 | add InfiniteRect, upd LongNv1 | 3/1 | 3 | 3 | 3/0/0 | Longitudinal (LongAcc/LongLoop/LongN) 2; misc named mechanism 1 |
| ac98a31 | 2026-07-29 | ccz181078 | add CounterClass2,Bouncer_v3,v4,BCv2,BLv2,FIBv5,LMv1,v2,SOBLv1,TranslatedBellv5, add some FAR,UBRRBAHalt certs | 13/3 | 26 | 26 | 20/6/0 | misc named mechanism 11; CTL/FAR certificates 6; CounterClass 4 |
| 7583181 | 2026-08-15 | ccz181078 | add BECv7,v8,BLECv3x,y,CounterClass3v1,InfiniteRect_v2,LMv3,SBCv10,v11,v6a2,SOMDCv7,Sk17Ex_1,8, upd Eqv_Misc,F | 13/12 | 54 | 45 | 27/12/6 | SBC (sync bouncer counter) 12; Longitudinal (LongAcc/LongLoop/LongN) 9; eqv merge 6 |
| 5a56ed7 | 2026-08-30 | ccz181078 | upd readme,CTL,CTLv2,UBRRBAHaltv2 add BLECv3z,BLv3,CCAv1,CubicCapLoop_v2,SOBCv10,SOBLv2,v3,TranslatedBellv6,Lo | 9/5 | 25 | 13 | 7/6/0 | SOBL 4; BLEC 2; misc named mechanism 2 |
| b801373 | 2026-09-05 | ccz181078 | add CounterClass1,Loop4Mono_v2,3,4,5,6 | 70/2 | 41 | 25 | 23/2/0 | CounterClass 16; Loop3/Loop4 9 |
| a7183bb | 2026-09-08 | ccz181078 | add SqrtSk17Like_v2,3,4,5, Sk17, Sk17_2x5, TranslatedBellv7,RGRv3, LA2x5Halts | 10/0 | 24 | 23 | 22/1/0 | Skelet-like (Sk1/Sk17/SqrtSk17) 21; misc named mechanism 1; TranslatedBell 1 |
| 51fa271 | 2026-09-16 | ccz181078 | add 78 SOC, 18 FractalType7, 11 Eqv, 2 FractalMisc | 12/3 | 119 | 105 | 86/12/7 | SOC (shift-overflow counter) 78; Fractal (FractalType*/Inv/Misc) 20; eqv merge 7 |
| dba975e | 2026-09-23 | univerz | add CounterRegular nonhalting proofs | 1/0 | 3 | 1 | 1/0/0 | SOBC 1 |
| 0e26ebd | 2026-09-23 | ccz181078 | Merge pull request #5 from univerz/counter-regular-proof | 0/0 | 0 | 0 | 0/0/0 | |
| 3127e48 | 2026-09-23 | ccz181078 | add 31 SOMDC_Class1, 2 SOMDCv8, 2 LongAccv1 | 2/1 | 35 | 35 | 35/0/0 | SOMDC 33; Longitudinal (LongAcc/LongLoop/LongN) 2 |
| 03de0b8 | 2026-09-23 | ccz181078 | Merge branch 'BB6' of github.com:ccz181078/busycoq into BB6 | 0/0 | 0 | 0 | 0/0/0 | |
| 605d26d | 2026-09-24 | ccz181078 | add BMO9, S18, SOBCv11,v12 | 3/1 | 4 | 3 | 3/0/0 | SOBC 2; misc named mechanism 1 |
| 27b8b41 | 2026-09-30 | ccz181078 | add BTCv4,SOTCv2,Sk1Machines,SOC23_Halt165,Nonhalt51,PeriodicHalt,SOC_4_3_Halt,Halt13,Halt14 | 9/0 | 18 | 18 | 5/13/0 | SOC (shift-overflow counter) 10; Skelet-like (Sk1/Sk17/SqrtSk17) 5; misc named mechanism 2 |
| 0940bb9 | 2026-10-07 | ccz181078 | add CubicMachines,SOCMisc,Bell60,QuadraticMess30,CounterClass3v2,Queue_v1,SBCv12 | 7/0 | 19 | 19 | 12/7/0 | SOC (shift-overflow counter) 7; Cubic (Cap/Cup/Mess/Machines) 6; Queue 2 |
U3. Coarse history per quarter (BB6 branch since 2024-05)
| quarter | commits | .v added | .v modified | lines added | holdout-universe 6x2 strings added | list removals attributed (4408→778 windows) | commit authors |
|---|---|---|---|---|---|---|---|
| 2024Q2 | 5 | 0 | 5 | 3,197 | 0 | 0 | ccz181078 5 |
| 2024Q3 | 24 | 53 | 25 | 49,198 | 1868 | 0 | ccz181078 24 |
| 2024Q4 | 27 | 40 | 61 | 599,198 | 166815 | 366 | ccz181078 27 |
| 2025Q1 | 15 | 94 | 54 | 242,466 | 65555 | 543 | ccz181078 15 |
| 2025Q2 | 6 | 13 | 8 | 41,451 | 179 | 104 | ccz181078 6 |
| 2025Q3 | 11 | 47 | 65 | 173,504 | 7832 | 1538 | ccz181078 11 |
| 2025Q4 | 12 | 53 | 72 | 127,444 | 868 | 542 | ccz181078 11, Shawn Ligocki 1 |
| 2026Q1 | 8 | 24 | 31 | 23,773 | 177 | 165 | ccz181078 8 |
| 2026Q2 | 10 | 54 | 10 | 35,268 | 126 | 66 | ccz181078 10 |
| 2026Q3 | 14 | 145 | 29 | 210,397 | 354 | 313 | ccz181078 13, univerz 1 |
| 2026Q4 | 1 | 7 | 0 | 13,699 | 19 | 19 | ccz181078 1 |
U4. The 778: sheet tabs and simulation backlog
| property | machines |
|---|---|
| in Classifications tab | 778 |
| Results status = (blank) | 759 |
| mentioned anywhere in verify/ | 299 |
| eqv group size > 1 | 291 |
| only as Eqv tm' (representative) | 286 |
| not simulated to 1e15 (open) | 168 |
| not simulated to 1e14 (open) | 133 |
| tab level-0 | 115 |
| has >=1 Discord link in sheet | 66 |
| tab level-1 | 41 |
| tab category-2 | 21 |
| Results status = CRYPTID | 18 |
| tab category-1 | 16 |
| tab category-3 | 15 |
| Cert_WF mention | 6 |
| Unverified-probably-incorrect tab | 4 |
| Results status = NONHALT | 1 |
| Discord link dated 2026-07-01 or later | 0 |
U5. Per sheet class (778): kill velocity and activity signals
| class | remaining | removed Dec+ | of which eqv | proof kills 06-29+ | proof kills 08-30+ | 3-mo velocity | last proof kill | state | sheet status set | in level tabs | in category tabs | with Discord link | latest link | not sim 1e14 | in verify/ |
|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|---|
| Shift-overflow counter | 128 | 299 | 40 | 141 | 130 | 0.52 | 2026-10-07 | hot (proof kill since 08-30) | 1 | 18 | 7 | 6 | 2026-03-29 | 6 | 50 |
| Skelet 1-like Class 1 | 101 | 11 | 0 | 5 | 5 | 0.05 | 2026-09-30 | hot (proof kill since 08-30) | 0 | 7 | 2 | 3 | 2025-03-29 | 0 | 34 |
| Unknown | 93 | 33 | 8 | 8 | 4 | 0.08 | 2026-10-07 | hot (proof kill since 08-30) | 0 | 12 | 2 | 18 | 2026-02-08 | 40 | 36 |
| Bell-like | 80 | 4 | 0 | 1 | 1 | 0.01 | 2026-10-07 | hot (proof kill since 08-30) | 15 | 23 | 9 | 10 | 2025-12-18 | 2 | 30 |
| Quadratic Mess | 51 | 10 | 0 | 5 | 2 | 0.09 | 2026-10-07 | hot (proof kill since 08-30) | 2 | 17 | 9 | 3 | 2026-04-08 | 0 | 21 |
| Cubic Mess | 50 | 13 | 4 | 7 | 6 | 0.12 | 2026-10-07 | hot (proof kill since 08-30) | 0 | 15 | 5 | 9 | 2025-12-03 | 1 | 26 |
| Bell eats counter | 40 | 7 | 3 | 4 | 0 | 0.09 | 2026-08-15 | cooling (proof kills Jul-Aug only) | 0 | 2 | 0 | 1 | 2024-11-03 | 0 | 16 |
| Shift-overflow bouncer counter | 33 | 13 | 0 | 8 | 3 | 0.20 | 2026-09-24 | hot (proof kill since 08-30) | 1 | 5 | 0 | 3 | 2025-06-18 | 0 | 13 |
| Chaotic Bell Class 3 | 22 | 0 | 0 | 0 | 0 | 0.00 | untouched (no proof kill since Dec) | 0 | 15 | 15 | 0 | 11 | 5 | ||
| Bouncer + Chaotic Edge | 20 | 13 | 2 | 4 | 0 | 0.17 | 2026-07-29 | cooling (proof kills Jul-Aug only) | 0 | 6 | 1 | 0 | 3 | 4 | |
| Chaotic Bell Class 1 | 19 | 4 | 4 | 0 | 0 | 0.00 | untouched (no proof kill since Dec) | 0 | 0 | 0 | 0 | 19 | 9 | ||
| Spaghetti | 18 | 5 | 3 | 0 | 0 | 0.00 | 2026-02-28 | stalled (proof kills Dec-Jun only) | 0 | 2 | 0 | 0 | 16 | 9 | |
| Chaotic 1dCA-like in bouncer | 14 | 5 | 3 | 0 | 0 | 0.00 | 2026-02-28 | stalled (proof kills Dec-Jun only) | 0 | 2 | 0 | 2 | 2025-02-06 | 14 | 8 |
| Skelet 1-like Class 2 | 14 | 1 | 0 | 1 | 0 | 0.07 | 2026-08-15 | cooling (proof kills Jul-Aug only) | 0 | 5 | 0 | 1 | 2025-10-28 | 0 | 4 |
| Shift-overflow structural counter | 11 | 11 | 0 | 8 | 0 | 0.42 | 2026-08-30 | cooling (proof kills Jul-Aug only) | 0 | 3 | 0 | 2 | 2025-06-18 | 0 | 7 |
| Structural counter + chaotic edge | 11 | 13 | 7 | 6 | 0 | 0.35 | 2026-08-30 | cooling (proof kills Jul-Aug only) | 0 | 0 | 0 | 0 | 0 | 8 | |
| Chaotic Ack-like Bell | 11 | 1 | 0 | 0 | 0 | 0.00 | 2026-02-15 | stalled (proof kills Dec-Jun only) | 0 | 4 | 0 | 0 | 0 | 2 | |
| Chaotic 1dCA-like in bell | 9 | 0 | 0 | 0 | 0 | 0.00 | untouched (no proof kill since Dec) | 0 | 4 | 0 | 1 | 2025-11-15 | 9 | 0 | |
| Monotone list | 8 | 12 | 0 | 9 | 9 | 0.53 | 2026-09-05 | hot (proof kill since 08-30) | 0 | 0 | 0 | 0 | 0 | 1 | |
| Chaotic Bell Class 2 | 7 | 8 | 0 | 4 | 1 | 0.36 | 2026-09-08 | hot (proof kill since 08-30) | 0 | 3 | 0 | 1 | 2025-02-09 | 0 | 1 |
| Translated Counter | 5 | 1 | 0 | 1 | 1 | 0.17 | 2026-09-30 | hot (proof kill since 08-30) | 0 | 3 | 0 | 5 | 2025-12-31 | 5 | 2 |
| Structural counter + counter | 5 | 0 | 0 | 0 | 0 | 0.00 | untouched (no proof kill since Dec) | 0 | 0 | 0 | 0 | 0 | 0 | ||
| Chaotic Bell Class 4 | 5 | 1 | 1 | 0 | 0 | 0.00 | untouched (no proof kill since Dec) | 0 | 1 | 0 | 0 | 0 | 4 | ||
| Chaotic Fractral Type 1 | 4 | 18 | 0 | 18 | 18 | 0.82 | 2026-09-16 | hot (proof kill since 08-30) | 0 | 2 | 1 | 0 | 0 | 1 | |
| Sync bouncer counter | 4 | 10 | 0 | 8 | 0 | 0.67 | 2026-08-15 | cooling (proof kills Jul-Aug only) | 0 | 0 | 0 | 0 | 0 | 1 | |
| Chaotic Fractral Others | 4 | 6 | 0 | 2 | 2 | 0.33 | 2026-09-16 | hot (proof kill since 08-30) | 0 | 1 | 0 | 0 | 0 | 0 | |
| Fractal in Bouncer | 3 | 6 | 0 | 2 | 0 | 0.40 | 2026-07-29 | cooling (proof kills Jul-Aug only) | 0 | 2 | 0 | 0 | 2 | 3 | |
| Counter Class 3 | 3 | 4 | 0 | 4 | 1 | 0.57 | 2026-10-07 | hot (proof kill since 08-30) | 0 | 2 | 0 | 1 | 2025-02-28 | 0 | 0 |
| Counter Class 2 | 3 | 4 | 0 | 4 | 0 | 0.57 | 2026-07-29 | cooling (proof kills Jul-Aug only) | 0 | 0 | 0 | 0 | 3 | 3 | |
| Counter Class 4 | 2 | 0 | 0 | 0 | 0 | 0.00 | untouched (no proof kill since Dec) | 0 | 2 | 0 | 0 | 2 | 1 |
U6. 'Done By' (Results tab) for Dec 2025+ list removals
| Done By | removals |
|---|---|
| mxdys | 302 |
| (blank) | 299 |
| -d | 55 |
| Andrew Ducharme | 19 |
| Alistaire | 9 |
| Pomme | 4 |
| Peacemaker | 4 |
| prurq | 4 |
| Racheline | 3 |
| Shawn Ligocki | 2 |
| racheline | 2 |
| Dyuan | 2 |
| dyuan | 2 |
| Peacemaker II | 2 |
| star | 1 |
| hipparcos | 1 |
| nerdyjoe | 1 |
| hi529 | 1 |
| 12AbBa | 1 |
| Autumn Pan | 1 |
| vyx | 1 |
| DrDisentangle | 1 |
| mammillaria | 1 |
Results-tab status of those removals: (blank) 324, NONHALT 227, EQUIVALENCE 56, HALT 30, NONHALT (?) 1
U7. Family mix: Dec 2025–Jun 2026 windows vs Jun 29–Oct 7 windows (proof kills)
| family | Dec–Jun | Jun 29–Oct 7 |
|---|---|---|
| SOC (shift-overflow counter) | 9 | 96 |
| Longitudinal (LongAcc/LongLoop/LongN) | 79 | 12 |
| CTL/FAR certificates | 67 | 6 |
| SOMDC | 11 | 36 |
| Skelet-like (Sk1/Sk17/SqrtSk17) | 11 | 19 |
| misc named mechanism | 9 | 21 |
| SOCSS | 28 | 0 |
| CounterClass | 0 | 24 |
| Fractal (FractalType*/Inv/Misc) | 3 | 21 |
| SBC (sync bouncer counter) | 6 | 13 |
| Loop3/Loop4 | 3 | 11 |
| SOBC | 9 | 5 |
| TranslatedBell | 10 | 3 |
| BLEC | 6 | 4 |
| RWLAcc/RRBA (inductive decider certs) | 5 | 5 |
| Cubic (Cap/Cup/Mess/Machines) | 0 | 7 |
| Bouncer | 4 | 2 |
| SOBL | 0 | 5 |
| other: TC | 3 | 0 |
| BEC (bell eats counter) | 0 | 2 |
| Bell | 1 | 1 |
| Inductive decider | 2 | 0 |
| Queue | 0 | 2 |
| QuadraticMess | 0 | 1 |
| SOTC | 0 | 1 |
| total | 266 | 297 |
U8. Bytes per machine of the attributed proof file (median), by family and period
| family | Dec–Jun median | n | Jun 29–Oct median | n |
|---|---|---|---|---|
| SOC (shift-overflow counter) | 5,683 | 9 | 10,189 | 96 |
| Longitudinal (LongAcc/LongLoop/LongN) | 2,691 | 79 | 231 | 12 |
| CTL/FAR certificates | 162 | 67 | 162 | 6 |
| SOMDC | 6,061 | 11 | 13,835 | 36 |
| Skelet-like (Sk1/Sk17/SqrtSk17) | 33,682 | 11 | 33,682 | 19 |
| misc named mechanism | 8,963 | 9 | 17,742 | 21 |
| SOCSS | 2,866 | 28 | 0 | |
| CounterClass | 0 | 2,847 | 24 | |
| Fractal (FractalType*/Inv/Misc) | 3,374 | 3 | 29,925 | 21 |
| SBC (sync bouncer counter) | 6,228 | 6 | 5,239 | 13 |
| Loop3/Loop4 | 4,620 | 3 | 25,922 | 11 |
| SOBC | 5,666 | 9 | 18,732 | 5 |
| TranslatedBell | 7,286 | 10 | 117,285 | 3 |
| BLEC | 6,177 | 6 | 313,600 | 4 |
| RWLAcc/RRBA (inductive decider certs) | 132 | 5 | 131 | 5 |
| Cubic (Cap/Cup/Mess/Machines) | 0 | 11,855 | 7 | |
| Bouncer | 3,438 | 4 | 6,828 | 2 |
| SOBL | 0 | 7,421 | 5 | |
| other: TC | 1,605 | 3 | 0 | |
| BEC (bell eats counter) | 0 | 11,960 | 2 | |
| Bell | 4,768 | 1 | 11,334 | 1 |
| Inductive decider | 151 | 2 | 0 | |
| Queue | 0 | 29,864 | 2 | |
| QuadraticMess | 0 | 38,975 | 1 | |
| SOTC | 0 | 27,109 | 1 | |
| all | 2,866 | 266 | 11,334 | 297 |
U9. Proof files behind Dec 2025+ kills, per family (template candidates)
| family | file | kills | commit date(s) | commit(s) | author | kind | bytes | style flag |
|---|---|---|---|---|---|---|---|---|
| SOC (shift-overflow counter) | verify/SOC_2_3_v4.v |
40 | 2026-09-16 | 51fa271 | ccz181078 | multi-machine file | 407,568 | assistant-style header |
| SOC (shift-overflow counter) | verify/SOC_2_5_v2.v |
12 | 2026-09-16 | 51fa271 | ccz181078 | multi-machine file | 106,563 | assistant-style header |
| SOC (shift-overflow counter) | verify/SOC_3_3_v5.v |
7 | 2026-09-16 | 51fa271 | ccz181078 | multi-machine file | 142,447 | assistant-style header |
| SOC (shift-overflow counter) | verify/SOC_2_3_v5.v |
7 | 2026-09-16 | 51fa271 | ccz181078 | multi-machine file | 53,865 | plain |
| Longitudinal (LongAcc/LongLoop/LongN) | verify/LongLoopv2.v |
24 | 2026-02-15..2026-03-15 | 457869d,54863c1,eb3ecb7 | ccz181078 | multi-machine file | 83,216 | plain |
| Longitudinal (LongAcc/LongLoop/LongN) | verify/LongAccHaltv1.v |
23 | 2026-02-15..2026-08-15 | 457869d,7583181 | ccz181078 | decider certificate | 4,646 | n/a (certificate/other) |
| Longitudinal (LongAcc/LongLoop/LongN) | verify/LongAccv1.v |
17 | 2026-02-15..2026-09-23 | 3127e48,457869d | ccz181078 | multi-machine file | 6,694 | plain |
| Longitudinal (LongAcc/LongLoop/LongN) | verify/LongLoopv3.v |
16 | 2026-03-25..2026-08-15 | 6f61914,7583181 | ccz181078 | multi-machine file | 45,744 | plain |
| CTL/FAR certificates | verify/FARv1.v |
73 | 2025-12-16..2026-07-29 | 10e149a,457869d,54863c1,760fc21,7fd9993,83531ba,ac98a31,bdf5ff5,d7ae6ec,e52b811,eb3ecb7 | ccz181078 | decider certificate | 26,156 | n/a (certificate/other) |
| SOMDC | verify/SOMDC_Class1.v |
31 | 2026-09-23 | 3127e48 | ccz181078 | multi-machine file | 428,875 | plain |
| SOMDC | verify/SOMDCv6.v |
8 | 2026-03-25..2026-07-02 | 6f61914,eb20dbd | ccz181078 | multi-machine file | 48,490 | plain |
| SOMDC | verify/SOMDCv4.v |
3 | 2026-02-15 | 457869d | ccz181078 | multi-machine file | 21,444 | plain |
| SOMDC | verify/SOMDCv5.v |
2 | 2026-03-11 | 760fc21 | ccz181078 | multi-machine file | 24,127 | plain |
| misc named mechanism | verify/FIBv3.v |
3 | 2026-01-29 | 7fd9993 | ccz181078 | multi-machine file | 28,008 | plain |
| misc named mechanism | verify/LMv2.v |
3 | 2026-07-29 | ac98a31 | ccz181078 | multi-machine file | 54,633 | plain |
| misc named mechanism | verify/BLv2.v |
3 | 2026-07-29 | ac98a31 | ccz181078 | multi-machine file | 12,728 | plain |
| misc named mechanism | verify/BCv2.v |
2 | 2026-07-29 | ac98a31 | ccz181078 | multi-machine file | 11,685 | plain |
| Skelet-like (Sk1/Sk17/SqrtSk17) | verify/Sk17.v |
15 | 2026-09-08 | a7183bb | ccz181078 | multi-machine file | 538,907 | assistant-style header |
| Skelet-like (Sk1/Sk17/SqrtSk17) | verify/Sk1Machines.v |
5 | 2026-09-30 | 27b8b41 | ccz181078 | multi-machine file | 83,110 | assistant-style header |
| Skelet-like (Sk1/Sk17/SqrtSk17) | verify/Sk1like_TC_v1.v |
3 | 2026-03-11 | 760fc21 | ccz181078 | multi-machine file | 14,642 | plain |
| Skelet-like (Sk1/Sk17/SqrtSk17) | verify/SqrtSk17Like_v2.v |
3 | 2026-09-08 | a7183bb | ccz181078 | multi-machine file | 18,326 | plain |
| SOCSS | verify/SOCSSv2.v |
18 | 2026-02-15..2026-03-11 | 457869d,760fc21 | ccz181078 | multi-machine file | 51,580 | plain |
| SOCSS | verify/SOCSSv3.v |
7 | 2026-03-11 | 760fc21 | ccz181078 | multi-machine file | 55,394 | plain |
| SOCSS | verify/SOCSS.v |
1 | 2025-12-30 | d7ae6ec | ccz181078 | multi-machine file | 37,286 | plain |
| SOCSS | verify/SOCSSv4.v |
1 | 2026-03-25 | 6f61914 | ccz181078 | single-machine file | 16,841 | plain |
| Fractal (FractalType*/Inv/Misc) | verify/FractalType7v2.v |
13 | 2026-09-16 | 51fa271 | ccz181078 | multi-machine file | 389,031 | refs to files not in repo |
| Fractal (FractalType*/Inv/Misc) | verify/FractalMisc.v |
5 | 2025-12-16..2026-09-16 | 51fa271,bdf5ff5 | ccz181078 | multi-machine file | 64,106 | plain |
| Fractal (FractalType*/Inv/Misc) | verify/FractalType7v3.v |
4 | 2026-09-16 | 51fa271 | ccz181078 | multi-machine file | 74,080 | refs to files not in repo |
| Fractal (FractalType*/Inv/Misc) | verify/FractalType1v5.v |
1 | 2026-08-15 | 7583181 | ccz181078 | multi-machine file | 30,815 | plain |
| CounterClass | verify/CounterClass1/CounterClass1.v |
16 | 2026-09-05 | b801373 | ccz181078 | parameterized family | 45,551 | plain |
| CounterClass | verify/CounterClass3v1.v |
3 | 2026-08-15 | 7583181 | ccz181078 | multi-machine file | 7,714 | plain |
| CounterClass | verify/CounterClass2v4.v |
1 | 2026-07-29 | ac98a31 | ccz181078 | single-machine file | 110,508 | plain |
| CounterClass | verify/CounterClass2v1.v |
1 | 2026-07-29 | ac98a31 | ccz181078 | single-machine file | 99,143 | plain |
| SBC (sync bouncer counter) | verify/SBCv11.v |
6 | 2026-08-15 | 7583181 | ccz181078 | multi-machine file | 31,434 | plain |
| SBC (sync bouncer counter) | verify/SBCv6a.v |
3 | 2026-03-11 | 760fc21 | ccz181078 | multi-machine file | 18,624 | plain |
| SBC (sync bouncer counter) | verify/SBCv9.v |
2 | 2026-02-15 | 457869d | ccz181078 | multi-machine file | 26,578 | plain |
| SBC (sync bouncer counter) | verify/SBCv10.v |
2 | 2026-08-15 | 7583181 | ccz181078 | multi-machine file | 50,090 | plain |
| Loop3/Loop4 | verify/Loop4Mono.v |
2 | 2025-12-16 | bdf5ff5 | ccz181078 | multi-machine file | 240,253 | plain |
| Loop3/Loop4 | verify/Loop4v4.v |
2 | 2026-08-15 | 7583181 | ccz181078 | multi-machine file | 69,535 | plain |
| Loop3/Loop4 | verify/Loop4Mono_v4.v |
2 | 2026-09-05 | b801373 | ccz181078 | multi-machine file | 21,295 | plain |
| Loop3/Loop4 | verify/Loop4Mono_v6.v |
2 | 2026-09-05 | b801373 | ccz181078 | multi-machine file | 51,843 | plain |
| SOBC | verify/SOBCv8.v |
7 | 2025-12-16..2026-04-29 | a95776a,bdf5ff5,d7ae6ec | ccz181078 | multi-machine file | 135,989 | plain |
| SOBC | verify/SOBCv9.v |
3 | 2026-03-11..2026-08-15 | 7583181,760fc21 | ccz181078 | multi-machine file | 21,373 | plain |
| SOBC | verify/SOBCv12.v |
2 | 2026-09-24 | 605d26d | ccz181078 | multi-machine file | 37,465 | plain |
| SOBC | verify/SOBCv10.v |
1 | 2026-08-30 | 5a56ed7 | ccz181078 | single-machine file | 151,813 | plain |
| TranslatedBell | verify/TranslatedBellv3.v |
6 | 2025-12-16 | bdf5ff5 | ccz181078 | multi-machine file | 43,718 | plain |
| TranslatedBell | verify/TranslatedBellv2.v |
2 | 2025-12-16 | bdf5ff5 | ccz181078 | multi-machine file | 27,625 | plain |
| TranslatedBell | verify/TranslatedBellv4.v |
2 | 2025-12-16 | bdf5ff5 | ccz181078 | multi-machine file | 9,157 | plain |
| TranslatedBell | verify/TranslatedBellv5.v |
1 | 2026-07-29 | ac98a31 | ccz181078 | single-machine file | 23,196 | plain |
| BLEC | verify/BLECv3.v |
6 | 2025-12-16..2026-01-29 | 7fd9993,bdf5ff5 | ccz181078 | multi-machine file | 37,064 | plain |
| BLEC | verify/BLECv3z.v |
2 | 2026-08-30 | 5a56ed7 | ccz181078 | multi-machine file | 772,348 | plain |
| BLEC | verify/BLECv3y.v |
1 | 2026-08-15 | 7583181 | ccz181078 | single-machine file | 241,027 | refs to files not in repo |
| BLEC | verify/BLECv3x.v |
1 | 2026-08-15 | 7583181 | ccz181078 | single-machine file | 88,113 | refs to files not in repo |
| RWLAcc/RRBA (inductive decider certs) | verify/RWLAccHaltv8.v |
5 | 2026-01-29..2026-02-15 | 457869d,7fd9993 | ccz181078 | decider certificate | 3,420 | n/a (certificate/other) |
| RWLAcc/RRBA (inductive decider certs) | verify/UBRRBAHaltv2.v |
4 | 2026-07-29..2026-08-30 | 5a56ed7,7583181,ac98a31 | ccz181078 | decider certificate | 14,040 | n/a (certificate/other) |
| RWLAcc/RRBA (inductive decider certs) | verify/RWLAccHaltv6.v |
1 | 2026-08-15 | 7583181 | ccz181078 | decider certificate | 16,858 | n/a (certificate/other) |
| Cubic (Cap/Cup/Mess/Machines) | verify/CubicMachines.v |
6 | 2026-10-07 | 0940bb9 | ccz181078 | multi-machine file | 71,130 | assistant-style header |
| Cubic (Cap/Cup/Mess/Machines) | verify/CubicCapLoop_v2.v |
1 | 2026-08-30 | 5a56ed7 | ccz181078 | single-machine file | 86,760 | plain |
| Bouncer | verify/Bouncer_v1.v |
4 | 2025-12-16 | bdf5ff5 | ccz181078 | multi-machine file | 13,754 | plain |
| Bouncer | verify/Bouncer_v3.v |
1 | 2026-07-29 | ac98a31 | ccz181078 | single-machine file | 3,471 | plain |
| Bouncer | verify/Bouncer_v4.v |
1 | 2026-07-29 | ac98a31 | ccz181078 | single-machine file | 10,184 | plain |
| SOBL | verify/SOBLv1.v |
3 | 2026-07-29..2026-08-30 | 5a56ed7,ac98a31 | ccz181078 | multi-machine file | 22,263 | plain |
| SOBL | verify/SOBLv2.v |
1 | 2026-08-30 | 5a56ed7 | ccz181078 | single-machine file | 22,943 | plain |
| SOBL | verify/SOBLv3.v |
1 | 2026-08-30 | 5a56ed7 | ccz181078 | single-machine file | 28,537 | plain |
| other: TC | verify/TCv3.v |
3 | 2026-03-11..2026-03-15 | 760fc21,eb3ecb7 | ccz181078 | multi-machine file | 4,816 | plain |
| Inductive decider | verify/Indv5.v |
1 | 2025-12-16 | bdf5ff5 | ccz181078 | decider certificate | 6,335 | n/a (certificate/other) |
| Inductive decider | verify/IndBGAS.v |
1 | 2026-02-15 | 457869d | ccz181078 | decider certificate | 22,147 | n/a (certificate/other) |
| Bell | verify/Bellv1.v |
1 | 2026-04-07 | 897a653 | ccz181078 | single-machine file | 4,768 | plain |
| Bell | verify/Bell60.v |
1 | 2026-10-07 | 0940bb9 | ccz181078 | single-machine file | 11,334 | assistant-style header |
| BEC (bell eats counter) | verify/BECv7.v |
2 | 2026-08-15 | 7583181 | ccz181078 | multi-machine file | 23,919 | plain |
| Queue | verify/Queue_v1.v |
2 | 2026-10-07 | 0940bb9 | ccz181078 | multi-machine file | 59,729 | assistant-style header |
| QuadraticMess | verify/QuadraticMess30.v |
1 | 2026-10-07 | 0940bb9 | ccz181078 | single-machine file | 38,975 | assistant-style header |
| SOTC | verify/SOTCv2.v |
1 | 2026-09-30 | 27b8b41 | ccz181078 | single-machine file | 27,109 | assistant-style header |
U10. Style tier of the file behind each Dec 2025+ proof kill, by commit month
Tiers (first match wins): explicit = a comment addresses 'the user' (assistant voice); assistant header = header claims standalone/self-contained/only-BusyCoq, consolidation, or cites an audit/attribution .md; absent refs = comments cite files not in the repo; prose-heavy = >=1 full-sentence comment per 1000 lines; classic = none of these (mostly mxdys's terse style); cert = decider certificate (no style).
| month | explicit | assistant header | absent refs | prose-heavy | classic | cert | total |
|---|---|---|---|---|---|---|---|
| 2025-12 | 0 | 0 | 0 | 0 | 51 | 32 | 83 |
| 2026-01 | 0 | 0 | 0 | 0 | 9 | 3 | 12 |
| 2026-02 | 0 | 0 | 0 | 0 | 58 | 42 | 100 |
| 2026-03 | 0 | 0 | 0 | 0 | 45 | 7 | 52 |
| 2026-04 | 0 | 0 | 0 | 0 | 2 | 0 | 2 |
| 2026-06 | 0 | 0 | 0 | 0 | 1 | 8 | 9 |
| 2026-07 | 0 | 0 | 0 | 0 | 24 | 7 | 31 |
| 2026-08 | 0 | 0 | 3 | 5 | 35 | 9 | 52 |
| 2026-09 | 0 | 101 | 17 | 51 | 34 | 0 | 203 |
| 2026-10 | 10 | 8 | 0 | 1 | 0 | 0 | 19 |
| total | 10 | 109 | 20 | 57 | 259 | 108 | 563 |
Jun 29–Oct 7 windows: explicit 10, assistant header 102, absent refs 20, prose-heavy 57, classic 92, cert 16 (of 297)
U11. Sheet class of Jun 29–Oct 7 proof kills by style tier of the proof file
| sheet class | explicit | assistant header | absent refs | prose-heavy | classic | cert | total |
|---|---|---|---|---|---|---|---|
| Shift-overflow counter | 7 | 78 | 0 | 43 | 8 | 5 | 141 |
| Chaotic Fractral Type 1 | 0 | 0 | 17 | 1 | 0 | 0 | 18 |
| Counter Class 1 | 0 | 0 | 0 | 0 | 16 | 0 | 16 |
| Monotone list | 0 | 0 | 0 | 2 | 7 | 0 | 9 |
| Bouncer + Complex Counter | 0 | 0 | 0 | 0 | 2 | 6 | 8 |
| Shift-overflow structural counter | 0 | 0 | 1 | 1 | 6 | 0 | 8 |
| Sync bouncer counter | 0 | 0 | 0 | 0 | 8 | 0 | 8 |
| Unknown | 2 | 0 | 2 | 2 | 2 | 0 | 8 |
| Shift-overflow bouncer counter | 0 | 0 | 0 | 4 | 1 | 3 | 8 |
| Skelet 17-like | 0 | 8 | 0 | 0 | 0 | 0 | 8 |
| Cubic Mess | 0 | 6 | 0 | 0 | 1 | 0 | 7 |
| List merging | 0 | 0 | 0 | 0 | 6 | 0 | 6 |
| Structural counter + chaotic edge | 0 | 0 | 0 | 0 | 6 | 0 | 6 |
| Quadratic Skelet 17-like | 0 | 0 | 0 | 1 | 5 | 0 | 6 |
| Quadratic Mess | 1 | 0 | 0 | 0 | 4 | 0 | 5 |
| Skelet 1-like Class 1 | 0 | 5 | 0 | 0 | 0 | 0 | 5 |
| Counter Class 2 | 0 | 0 | 0 | 0 | 4 | 0 | 4 |
| Bell eats counter | 0 | 0 | 0 | 2 | 2 | 0 | 4 |
| Bouncer + Chaotic Edge | 0 | 0 | 0 | 0 | 3 | 1 | 4 |
| Chaotic Bell Class 2 | 0 | 0 | 0 | 1 | 2 | 1 | 4 |
| Counter Class 3 | 0 | 1 | 0 | 0 | 3 | 0 | 4 |
| Fractal in Bouncer | 0 | 0 | 0 | 0 | 2 | 0 | 2 |
| Chaotic Fractral Others | 0 | 0 | 0 | 0 | 2 | 0 | 2 |
| Bouncer + Translated Counter | 0 | 2 | 0 | 0 | 0 | 0 | 2 |
| Structural counter + bouncer | 0 | 0 | 0 | 0 | 1 | 0 | 1 |
| Skelet 1-like Class 2 | 0 | 0 | 0 | 0 | 1 | 0 | 1 |
| Bell-like | 0 | 1 | 0 | 0 | 0 | 0 | 1 |
| Translated Counter | 0 | 1 | 0 | 0 | 0 | 0 | 1 |