fix: case-material consistency sweep from 2026-07-03 review

- ten -> twelve structure counts in detective.md and
  manipulation-taxonomy.md (leftovers from the 10 -> 12 expansion;
  read literally they excluded circular_reasoning and
  hasty_generalization from detective case generation)
- "timed drill" -> commit-gate wording in structures.md (drill has
  no timer; the pressure is the commit gate)
- drop six dangling "see unverified_claims" pointers (no such
  section exists in any pack and the schema defines no such field;
  the disclosures already live inline)
- keller-dimension-7: unify certificate size on the first-party
  224 GB figure (was 200+/200 in two places)
- busy-beaver-5: reword S5's check to what pack material supports
  (only three of the 13 holdouts are named in-pack; full list
  recovery tracked in #10)

Closes #8, closes #9

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01FacH1bZvYjujVDWrZqiy7t

Author: Imbad0202

expeditions/alphageometry-imo.md

@@ -52,7 +52,7 @@ Lean proofs.
 ## audit_targets
 
 - **T1 — "Human-readable + symbolically checked" is a *different* verification standard from "machine-formal (Lean)."** *Objection:* an auditor might assume any AI math result is trustworthy only if Lean-checked, and dismiss AlphaGeometry as "not formally verified." *Resolution:* AlphaGeometry's checker is its own symbolic deduction engine plus human expert review of readable synthetic steps — a *sound by construction* engine emitting classical-geometry proofs, not a Lean kernel. Both are real verification; they certify different objects (a readable geometric argument vs. a kernel-checked formal term). Confirmed first-party: every solution "checked and verified by computer," plus Evan Chen's review. The audit lesson: name *which* checker certified *which* artifact before trusting or rejecting.
-- **T2 — The 25/30 score is first-party; the 25.9 gold-medallist average is NOT in the text I read.** *Objection:* "approaching the performance of an average IMO gold medallist" is qualitative in the abstract; the crisp "25.9" is easy to over-cite as if it were a headline paper number. *Resolution:* I confirmed 25/30 and the qualitative gold-medallist comparison from the abstract; the 25.9 figure comes from DeepMind's blog/secondary coverage, not the paper body I could access. Treat 25.9 as provenance-blog, not provenance-paper. See unverified_claims.
+- **T2 — The 25/30 score is first-party; the 25.9 gold-medallist average is NOT in the text I read.** *Objection:* "approaching the performance of an average IMO gold medallist" is qualitative in the abstract; the crisp "25.9" is easy to over-cite as if it were a headline paper number. *Resolution:* I confirmed 25/30 and the qualitative gold-medallist comparison from the abstract; the 25.9 figure comes from DeepMind's blog/secondary coverage, not the paper body I could access. Treat 25.9 as provenance-blog, not provenance-paper.
 - **T3 — The named engine "DDAR/DD+AR" is not confirmed from the paper body.** *Objection:* secondary sources call the symbolic engine "DDAR" (deductive database + algebraic/arithmetic reasoning); a careless auditor will attribute that acronym to the abstract. *Resolution:* the abstract I read says only "symbolic deduction engine." The DDAR / DD+AR naming is from blog and follow-up papers. The *mechanism* (symbolic deduction engine guided by the LM) is first-party; the *acronym* is secondary.
 - **T4 — "Solves 25" ≠ "geometry is solved."** *Objection:* approaching gold-medallist average reads as superhuman/general. *Resolution:* scope is *Euclidean plane geometry* on a 30-problem benchmark of one problem type; 5 of 30 were unsolved, and the result does not extend to combinatorics, number theory, or algebra olympiad problems. The milestone (S4) is narrow by design.
 - **T5 — "Without human demonstrations" ≠ "without human knowledge."** *Objection:* the title suggests the system bootstrapped from nothing. *Resolution:* it sidesteps human *proof* demonstrations via synthetic data, but the symbolic engine encodes human-curated geometry deduction rules and the construction vocabulary; "no demonstrations" is a claim about the training corpus, not about zero human priors.

expeditions/alphaproof-imo-2024.md

@@ -57,7 +57,7 @@ against a 4.5-hour human session, and the problems were hand-formalized first?
 
 - **T2 — "Silver medal" describes a SCORE, not contest-equivalent performance.** 28/42 lands in the IMO 2024 silver band (gold 29, silver 22). *Objection:* "Then it really did earn silver, full stop." *Resolution:* The 28 points are real and correctly placed, but humans earned their medals in two 4.5-hour sessions while AlphaProof took up to three days; the score is equivalent, the *conditions* are not. Audit the verb: "scored at silver level" holds; "performed like a silver medallist" overreaches.
 
-- **T3 — The natural-language→Lean step was done by humans, not the system.** The five non-geometry problem statements were manually formalized in Lean by experts before the prover ran. *Objection:* "Formalization is mechanical bookkeeping, irrelevant to the achievement." *Resolution:* It is not mechanical — faithful formalization can itself encode mathematical insight and is where mis-statements silently change the problem; an end-to-end claim must own this human input. (Note: I confirmed this via secondary summaries + insider blog, not the paper body — see unverified_claims.)
+- **T3 — The natural-language→Lean step was done by humans, not the system.** The five non-geometry problem statements were manually formalized in Lean by experts before the prover ran. *Objection:* "Formalization is mechanical bookkeeping, irrelevant to the achievement." *Resolution:* It is not mechanical — faithful formalization can itself encode mathematical insight and is where mis-statements silently change the problem; an end-to-end claim must own this human input. (Note: I confirmed this via secondary summaries + insider blog, not the paper body.)
 
 - **T4 — A whole problem-class (combinatorics) was missed.** Both P3 and P5 were unsolved. *Objection:* "4/6 is still excellent; the misses are noise." *Resolution:* The misses are not random — they cluster entirely in combinatorics, revealing a structural capability boundary that the aggregate "silver" headline hides. Auditing the *distribution* of failures, not just the count, is what distinguishes a real reasoner from a domain-specialist.
 

expeditions/busy-beaver-5.md

@@ -44,7 +44,7 @@ The difficulty was never the champion — it was certifying that nothing beats i
 - **S2 — Probe small cases to feel the explosion** `small_case_probe` Hand-check S(1)=1, S(2)=6, S(3)=21 (1960s), then S(4)=107 (Brady 1983). Watch the jump to 47,176,870 at n=5. Check: simulate the n=2/n=3 champions by hand and confirm the published step counts; confirm the growth is super-exponential, motivating why n=5 needed machines not pencils.
 - **S3 — Cut the search space before deciding anything** `representation_shift` Tree Normal Form (TNF) collapses ~16.7 trillion syntactic machines to 181,385,789 by removing unreachable transitions and symmetric relabelings. Check: confirm the enumeration is itself run *inside Coq* (so the "we considered all machines" claim is machine-checked, not asserted).
 - **S4 — Decompose "all non-halters" into sound partial deciders** `lemma_decomposition` Split the non-halting burden across five independently-proved deciders (Loops, NGramCPS, RepWL, FAR, WFAR), each a checkable lemma "if decider D accepts machine M, then M never halts." Check: each decider's soundness is a separate Coq theorem; a reader can audit one decider without the others.
-- **S5 — Write the abandonment condition for the automated sweep** `kill_criteria` The kill criterion is explicit: any machine no decider settles becomes a named holdout requiring an individual proof. This bounds the bespoke work to a finite enumerated residue (13 sporadic machines: Skelet #1, #10, #17, …) rather than an open-ended hunt. Check: the count of undecided machines is reported and finite; verify 13 individual proofs exist, one per holdout.
+- **S5 — Write the abandonment condition for the automated sweep** `kill_criteria` The kill criterion is explicit: any machine no decider settles becomes a named holdout requiring an individual proof. This bounds the bespoke work to a finite enumerated residue (13 sporadic machines: Skelet #1, #10, #17, …) rather than an open-ended hunt. Check: the count of undecided machines is reported and finite; the paper supplies one machine-checked non-halting proof per holdout — this pack names three (Skelet #1, #10, #17); the full 13-machine list lives in the paper and bbchallenge records, not in this pack.
 - **S6 — Recast the summit as a verifiable chain** `milestone_rewrite` The claim "S(5)=47,176,870" becomes: (a) the champion halts at exactly 47,176,870 steps; (b) TNF covers all machines; (c) every machine is either decided non-halting by some sound decider, halts at ≤ 47,176,870, or is one of the 13 hand-proved non-halters. All assembled and checked in Coq. Check: each conjunct is a distinct Coq statement; the top theorem is their composition, auditable clause by clause.
 - **S7 — Confirm the boundary: why S(6) is different** `kill_criteria` Apply the same kill criterion at n=6 and watch it fail: ~2,600 holdouts remain, some (Antihydra) equivalent to open Collatz-type conjectures; the paper predicts S(6) "will never be proved." Check: confirm at least one S(6) holdout is reduced to a recognized open problem, establishing that S(5) sat exactly at the edge of decidability-by-effort.
 

expeditions/chromatic-number-plane-5.md

@@ -31,7 +31,7 @@ You predict, before each reveal, what the result does and does NOT settle.
 
 **Where the verified result lives.** Aubrey D.N.J. de Grey, "The chromatic number of the plane is at least 5," arXiv:1804.02385 (submitted 8 Apr 2018; v2 11 Apr 2018; v3 30 May 2018). Later published in *Geombinatorics* (vol. 28, 2018). The abstract states verbatim that the construction gives "a family of finite unit-distance graphs in the plane that are not 4-colourable" and that "the smallest such graph that we have so far discovered has 1581 vertices."
 
-**How verified.** The core claim is a *finite, machine-checkable* assertion: that a specific ~1581-vertex graph has no proper 4-colouring. This is exactly a Boolean satisfiability (SAT) / graph-colouring instance, and was checked by computer — the Polymath16 first thread notes de Grey's argument "required checking for the nonexistence of particular types of 4-colourings of subgraphs ... that have almost 400 vertices, which requires a computer search," later reduced to ~278-vertex subgraphs. So the non-4-colourability is independently re-verifiable by anyone who re-runs a SAT solver on the published edge list — this is the strongest possible provenance for a finite combinatorial claim. (Marijn Heule and others produced independent/optimised verifications and smaller graphs; I did not confirm Heule's specific numbers first-party, see unverified_claims.)
+**How verified.** The core claim is a *finite, machine-checkable* assertion: that a specific ~1581-vertex graph has no proper 4-colouring. This is exactly a Boolean satisfiability (SAT) / graph-colouring instance, and was checked by computer — the Polymath16 first thread notes de Grey's argument "required checking for the nonexistence of particular types of 4-colourings of subgraphs ... that have almost 400 vertices, which requires a computer search," later reduced to ~278-vertex subgraphs. So the non-4-colourability is independently re-verifiable by anyone who re-runs a SAT solver on the published edge list — this is the strongest possible provenance for a finite combinatorial claim. (Marijn Heule and others produced independent/optimised verifications and smaller graphs; I did not confirm Heule's specific numbers first-party.)
 
 **First-party check.** Read directly from arXiv:1804.02385 abstract page: the title, author "Aubrey D.N.J. de Grey," submission date 8 Apr 2018, the three version dates, the phrase "not 4-colourable," and the vertex count **1581**. Read first-party from Gil Kalai's announcement post: the upper bound 7 is "found by Isbell, based on the hexagonal packing with 7 colors"; the Moser spindle is "a unit-distance graph with chromatic number 4"; and "Until recently it was known that the answer can be 4, 5, 6 or 7." Read first-party from the Polymath16 thread: the computer-search verification of non-4-colourability and the goal to reduce computer reliance. I could **not** confirm first-party: the *Geombinatorics* volume/page exactly, de Grey's profession, the 510-vertex Polymath record, or any Heule figure — all flagged below.
 

expeditions/funsearch-cap-set.md

@@ -60,7 +60,7 @@ The breakthrough step is **S4** — re-attributing the 2.2202 capacity figure. I
 
 - **T1 — "FunSearch solved / cracked the cap-set problem."** *Objection:* The Nature news framing ("outdoes human mathematicians on unsolved problem") implies closure. *Resolution:* It improved two *lower bounds* via explicit constructions; the maximum c_8 is undetermined, c_n is exact only for n ≤ 6, and the capacity upper bound γ ≤ 2.756 is untouched. Verified first-party in both the paper and Davis. The parent problem is OPEN — the pack must never imply otherwise.
 - **T2 — "The 2.2202 capacity bound is FunSearch's discovery."** *Objection:* Mis-attributes a human-AI feedback result to the AI. *Resolution:* FunSearch's standalone admissible set gave γ ≥ 2.2184; the jump to 2.2202 came from Ellenberg spotting a symmetry in the human-readable program. Davis: "99.99% of the credit for this interaction belongs to Ellenberg." Provenance must be split.
-- **T3 — Omitted/under-credited prior work and baseline.** *Objection:* The "new" record only means something against the prior state of the art. *Resolution:* The dim-8 baseline was 496 and the capacity baseline 2.2180; the binding upper bound is Ellenberg–Gijswijt 2017 (γ ≤ 2.756). I have these via the paper + Davis, but did NOT independently confirm 496 against OEIS A090245 or the original prior-construction source — flagged in unverified_claims.
+- **T3 — Omitted/under-credited prior work and baseline.** *Objection:* The "new" record only means something against the prior state of the art. *Resolution:* The dim-8 baseline was 496 and the capacity baseline 2.2180; the binding upper bound is Ellenberg–Gijswijt 2017 (γ ≤ 2.756). I have these via the paper + Davis, but did NOT independently confirm 496 against OEIS A090245 or the original prior-construction source.
 - **T4 — "The LLM understood the mathematics."** *Objection:* Suggests reasoning where there is search. *Resolution:* The model is never told the problem; it only mutates a `priority` subroutine. Davis's central charge is the "shallowness" of any implied understanding — the math-steering lives in the genetic wrapper, invisible to the LLM.
 - **T5 — "This is a broad new method for hard math."** *Objection:* Over-generalizes from a narrow construction-search win. *Resolution:* Requires an efficient evaluator, rich score signal, and small mutable skeleton (authors' own preconditions); corresponding author Fawzi confirmed a direct RL-over-constructions approach "didn't scale." Forecast transfer only where all three preconditions hold.
 

expeditions/keller-dimension-7.md

@@ -20,7 +20,7 @@ In 1930 Ott-Heinrich Keller conjectured that any tiling of n-dimensional space b
 
 The proof works through the Corrádi–Szabó (1990) reduction to cliques in the Keller graph Gₙ,ₛ, whose vertices are ⟨2s⟩ⁿ with two vertices adjacent iff they differ by exactly s in at least one coordinate and differ in at least two coordinates. A clique of size 2ⁿ in some Gₙ,ₛ witnesses that the conjecture is FALSE in dimension n. Kisielewicz (2017) had reduced dimension 7 to the single question of whether G₇,₃ contains a clique of size 2⁷ = 128. The authors prove (Theorem 1) that none of G₇,₃, G₇,₄, G₇,₆ contains a clique of size 128 — hence the conjecture holds.
 
-**Accessibility note.** The *claim* is visualizable to a layperson: can you ever tile space with cubes so that no two cubes share a full face? The two-dimensional picture (offset brick-laying still forces full-edge contacts) is intuitive. What is NOT human-auditable is the *proof*: it is the absence of a 128-clique in a graph on thousands of vertices, established by a SAT solver emitting a 200+ gigabyte unsatisfiability certificate across tens of thousands of subformulas. No human reads that certificate; the audit target is the *encoding* and the *checker*, not the search.
+**Accessibility note.** The *claim* is visualizable to a layperson: can you ever tile space with cubes so that no two cubes share a full face? The two-dimensional picture (offset brick-laying still forces full-edge contacts) is intuitive. What is NOT human-auditable is the *proof*: it is the absence of a 128-clique in a graph on thousands of vertices, established by a SAT solver emitting a 224-gigabyte unsatisfiability certificate across tens of thousands of subformulas. No human reads that certificate; the audit target is the *encoding* and the *checker*, not the search.
 
 ## history
 
@@ -63,7 +63,7 @@ After all this, dimension 7 was a single, sharply-posed finite question that sti
 
 ## breakthrough
 
-**S6 is the breakthrough** — not the SAT search itself but the certified-checker pipeline (DRAT proof → DRAT-trim → ACL2check, a checker formally verified in ACL2). It eluded the community because earlier dimension-7 work could pose the clique question but could not produce a *machine-auditable* answer; the move that closes the case is recognizing that the entire trust burden can be shifted onto a formally-verified proof checker, so a 200-gigabyte certificate no human can read still constitutes a rigorous proof. The hard mathematical narrowing (S1–S3, reducing to a single 128-clique question in G₇,₃) was already done by Corrádi-Szabó, Debroni et al., and Kisielewicz; what was missing was certified exhaustive search at scale.
+**S6 is the breakthrough** — not the SAT search itself but the certified-checker pipeline (DRAT proof → DRAT-trim → ACL2check, a checker formally verified in ACL2). It eluded the community because earlier dimension-7 work could pose the clique question but could not produce a *machine-auditable* answer; the move that closes the case is recognizing that the entire trust burden can be shifted onto a formally-verified proof checker, so a 224-gigabyte certificate no human can read still constitutes a rigorous proof. The hard mathematical narrowing (S1–S3, reducing to a single 128-clique question in G₇,₃) was already done by Corrádi-Szabó, Debroni et al., and Kisielewicz; what was missing was certified exhaustive search at scale.
 
 ## audit_targets
 

expeditions/lams-problem.md

@@ -34,7 +34,7 @@ you verify that something does not exist?
 
 **How verified.** I read the full text of arXiv:2012.04715 first-party (extracted from the PDF). Verification chain inside the paper: SAT instances solved by MapleSAT; resulting DRAT (Deletion Resolution Asymmetric Tautology) proofs checked by independent verifiers GRATgen and DRAT-trim. The "main" certificates (~4GB) are checked with DRAT-trim in forward-checking mode; the full GRATgen check of all proofs took about 33,000 core hours. Symmetry handling uses the Traces library, but the paper explains how the certificates are checkable without trusting Traces' output.
 
-**First-party check — numbers I read directly from arXiv:2012.04715:** order-10 nonexistence; 111×111 incidence matrix and the *n*²+*n*+1=111 count; the three codeword cases (weight 15, weight 16, primitive weight 19) and that this paper handles the hardest, the primitive weight-19 case (15/16 handled in companions); DRAT format; main certificates ~4GB; Traces A2 labellings ~7GB; ~33,000 core-hours for GRATgen checking; cubing produced over 312 million cubes in ~1,200 hours; 45 remaining cases with 639,075 nonisomorphic A2s; 24,882 partial solutions checked; 1989 LTS ~24 months at 2.1 GHz and Roy 2011 ~27 months at 2.4 GHz; the discovered A2-count discrepancies between the two prior searches. **Could NOT confirm first-party this session:** the ovals paper's "~1,850 core-hours / ~3 TB compressed" figures (these came from a search-result summary of arXiv:2001.11974, not the PDF body) — see unverified_claims.
+**First-party check — numbers I read directly from arXiv:2012.04715:** order-10 nonexistence; 111×111 incidence matrix and the *n*²+*n*+1=111 count; the three codeword cases (weight 15, weight 16, primitive weight 19) and that this paper handles the hardest, the primitive weight-19 case (15/16 handled in companions); DRAT format; main certificates ~4GB; Traces A2 labellings ~7GB; ~33,000 core-hours for GRATgen checking; cubing produced over 312 million cubes in ~1,200 hours; 45 remaining cases with 639,075 nonisomorphic A2s; 24,882 partial solutions checked; 1989 LTS ~24 months at 2.1 GHz and Roy 2011 ~27 months at 2.4 GHz; the discovered A2-count discrepancies between the two prior searches. **Could NOT confirm first-party this session:** the ovals paper's "~1,850 core-hours / ~3 TB compressed" figures (these came from a search-result summary of arXiv:2001.11974, not the PDF body).
 
 ## step_graph