/reports/forensics/style_summary.md · raw

S1. Proof-file style by era of first commit (median per file; proof files at the pin, certificates excluded)

era files bytes_per_machine comment_ratio median_proof_lines fw_tac_per_lemma gen_tac_per_lemma lia_per_lemma n_inductive n_fixpoint coqdoc_headings bullets snake_lemma_frac mean_lemma_name_len mean_line_len late_requires has_header prose_comments_per_kloc cbn_lists intro_patterns zify_or_selector
a: before 2025-12 107 3599 0 6 1.44 4.71 0.71 1 0 0 107 0.4 6.2 22.6 0 0 0 3 12 0
b: 2025-12..2026-06 27 7124 0 8 0.77 6.03 1.05 2 0 0 73 0.59 7.2 24.5 0 0 0 6 4 0
c: 2026-07..08 33 23196 0 6 0.31 9.6 0.85 3 2 0 141 0.9 10.8 31 0 0 0 27 24 0
d: 2026-09..10 62 13224 0.0085 5 0.23 7.975 1.06 3 4 0 86 0.715 9.25 41.1 1 0 1.965 27.5 38 0

S2. Same, split by assistant-style header / external-file references

group files bytes_per_machine comment_ratio median_proof_lines fw_tac_per_lemma gen_tac_per_lemma lia_per_lemma n_inductive n_fixpoint coqdoc_headings bullets snake_lemma_frac mean_lemma_name_len mean_line_len late_requires has_header prose_comments_per_kloc cbn_lists intro_patterns zify_or_selector
assistant-style header / c 3 88113 0.035 5 0.13 8.73 0.43 9 11 0 179 0.99 19.6 43.6 1 0 7.42 46 31 0
assistant-style header / d 24 23729.5 0.0155 4 0.605 6.35 0.885 4.5 12.5 0 118 0.72 8.3 43.15 2 1 6.025 70 70 0
plain / a 107 3599 0 6 1.44 4.71 0.71 1 0 0 107 0.4 6.2 22.6 0 0 0 3 12 0
plain / b 27 7124 0 8 0.77 6.03 1.05 2 0 0 73 0.59 7.2 24.5 0 0 0 6 4 0
plain / c 30 20577 0 6 0.47 9.665 0.865 3 2 0 122.5 0.895 10.75 29.85 0 0 0 22 24 0
plain / d 38 6605.5 0 6 0.08 9.385 1.515 1.5 1 0 35 0.71 9.5 38.2 0 0 0 2 14 0

S3. Files with an assistant-style header or references to files not in the repo

first seen commit file 6x2 proved bytes header / external refs
2026-08-15 7583181 BLECv3x.v 1 88,113 — refs: TM4x1.txt
2026-08-15 7583181 BLECv3y.v 1 241,027 — refs: TM4y1.txt
2026-08-15 7583181 SBCv6a2.v 1 45,581 — refs: TM11.txt
2026-09-08 a7183bb Sk17.v 16 538,907 Self-contained column-flow proofs for test_48/TM1--TM8 and Skelet17/v2--v8. Only BusyCoq and the Coq standard library are required.
2026-09-16 51fa271 FractalType7v2.v 13 389,031 — refs: FT7CallRules.v;FT7Compute.v;FT7ComputeSpec.v;FT7Cycle.v;FT7Entry.v;FT7Machines.v;FT7Proof.v;FT7Stages.v
2026-09-16 51fa271 FractalType7v3.v 4 74,080 — refs: FT7TM16Compute.v;FT7TM16ComputeSpec.v;FT7TM16Cycle.v;FT7TM16Nonhalt.v;FT7TM16Prefix.v;FT7TM17.v;FT7TM17Compute.v;FT7TM17ComputeSpec.v
2026-09-16 51fa271 SOC_2_3_v4.v 40 407,568 Consolidated checked proofs. See SOC_FT7_CONSOLIDATION.md for numbering. — refs: SOC23_R2carry.v;SOC23_R2carry01.v;SOC23_R2half.v;SOC23_R2parity.v;SOC23_R2split.v;SOC23_R2weighted.v;SOC23_ShortSplit.v;SOC23_TM102Halt.v
2026-09-16 51fa271 SOC_2_4_v8.v 4 45,933 Consolidated checked proofs. See SOC_FT7_CONSOLIDATION.md for numbering. — refs: SOC24_R3.v;SOC_FT7_CONSOLIDATION.md
2026-09-16 51fa271 SOC_2_5_v2.v 12 106,563 Consolidated checked proofs. See SOC_FT7_CONSOLIDATION.md for numbering. — refs: SOC25_R3.v;SOC25_R3zero.v;SOC25_TM85.v;SOC25_TM91.v;SOC_FT7_CONSOLIDATION.md
2026-09-16 51fa271 SOC_3_3_v5.v 7 142,447 Consolidated checked proofs. See SOC_FT7_CONSOLIDATION.md for numbering. — refs: SOC33_TM4.v;SOC_EX_WEIGHTED.md;SOC_ExWeighted.v;SOC_FT7_CONSOLIDATION.md
2026-09-16 51fa271 SOC_3_4_v1.v 1 16,383 Consolidated checked proofs. See SOC_FT7_CONSOLIDATION.md for numbering. — refs: SOC_FT7_CONSOLIDATION.md
2026-09-16 51fa271 SOC_3_6_v1.v 5 38,932 Consolidated checked proofs. See SOC_FT7_CONSOLIDATION.md for numbering. — refs: SOC_FT7_CONSOLIDATION.md
2026-09-16 51fa271 SOC_4_3_v1.v 2 25,226 Consolidated checked proofs. See SOC_FT7_CONSOLIDATION.md for numbering. — refs: SOC43_Extra.v;SOC_FT7_CONSOLIDATION.md
2026-09-30 27b8b41 BTCv4.v 2 31,585 M-Abozaid M23 and its sibling: event acceleration plus the existing CTL checker. Sources, certificate conversion and audit: EXTERNAL_BOUNCER_PROOFS.md. The DFA — refs: EXTERNAL_BOUNCER_PROOFS.md;m23_dfa_analyze.py
2026-09-30 27b8b41 SOC23_Halt165.v 1 91,057 SOC23.TM165: standalone periodic-tape checker and halting proof. This file needs only BusyCoq and the standard library.
2026-09-30 27b8b41 SOC23_Nonhalt51.v 1 130,826 SOC23.TM51: nonhalting by a generated-block queue invariant. Standalone; only BusyCoq and standard-library dependencies. The finite entry is checked using binar — refs: SOC51_BLOCK_PROOF.md
2026-09-30 27b8b41 SOC23_PeriodicHalt.v 3 92,160 SOC23.TM69/72/70: standalone periodic-tape checker, soundness and final checks. This file needs only BusyCoq and the standard library.
2026-09-30 27b8b41 SOC43_Halt13.v 1 56,273 SOC_ex 13 (test_SOC_4_3.TM10): finite halting proof with sparse powers. Standalone: only BusyCoq and standard-library dependencies. See SOC43_EX13_RUNS.md for t — refs: SOC43_EX13_RUNS.md
2026-09-30 27b8b41 SOC43_Halt14.v 1 87,337 SOC_ex row 14: standalone periodic-tape checker and its TM soundness.
2026-09-30 27b8b41 SOTCv2.v 1 27,109 M-Abozaid M7: BusyCoq translation of the translated-counter level cycle. Source and attribution: EXTERNAL_BOUNCER_PROOFS.md. All rules, initialization and nonha — refs: EXTERNAL_BOUNCER_PROOFS.md
2026-09-30 27b8b41 Sk1Machines.v 5 83,110 Sk1 Class1: TM17 nonhalts; TM91, TM94, TM104, TM105 halt. Self-contained except for BusyCoq and the Coq standard library.
2026-10-07 0940bb9 Bell60.v 1 11,334 Bell60: a complete RLE accelerator and its halting certificate. Only BusyCoq and standard-library dependencies; no stored long trace.
2026-10-07 0940bb9 CounterClass3v2.v 1 40,609 M1: macro-inductive nonhalting proof, ported to current BusyCoq. The two finite symbolic bridges are generated and checked inside Coq; no external trace table o — refs: Base.v;Tail.v;symsim.py
2026-10-07 0940bb9 CubicMachines.v 6 71,130 Completed machines from cubic.txt: TM1, TM17, TM18, TM39, TM41, TM49. Five halt proofs and one nonhalt proof. TM17 and TM18 share their one long computation. On — refs: cubic.txt
2026-10-07 0940bb9 QuadraticMess30.v 1 38,975 Parameter lemmas adapted from the halting-proof archive supplied by the user. The entire route is generated by a proved RLE parameter interpreter.
2026-10-07 0940bb9 Queue_v1.v 2 59,729 Adapted from the October 2026 nonhalting proof archive supplied by the user. The finite graph is constructed by a small generator, not a literal table.
2026-10-07 0940bb9 SOCMisc.v 7 316,038 SOC A1--A7: independent nonhalting proofs, with shared arithmetic. TM1, TM5 and TM6 use literal L/R mirrors; the others use the originals. Each machine and its — refs: SOCPair12Carry.v;SOCPair12Closure.v;SOCPair12Entry.v;SOCPair12EntryGuard.v;SOCPair12Exceptional.v;SOCPair12Guard.v;SOCPair12Ordinary.v;SOCPair12Overflow.v

S4. Signal hit counts

source strength pattern hits
sheet strong \bClaude\b 1
sheet strong \bOpus\b 1
sheet weak \barchive\b 1
v comment weak \b[A-Z][A-Z0-9_]+\.md\b 16
v comment weak \barchive\b 5
v comment weak \baudit\b 2
v comment weak \bconsolidat\w* 9
v comment weak \bgenerated (?:and checked )?(?:inside|by|in) (?:Coq|a)\b 2
v comment weak \bno (?:external|stored|literal)\b 2
v comment weak \bported to current BusyCoq\b 1
v comment weak \bself-contained\b 2
v comment weak \bstandalone\b 8
v comment weak \bthe user'?s?\b 3
v comment weak \buntrusted input\b 1
v comment weak only BusyCoq|requires only BusyCoq|BusyCoq and (?:the )?(?:Coq )?standard[- ]library 11
v comment weak supplied by the user 2