[TomZahavy]

Summary

This PR updates the names, documentation, and module headers for the 6 BB(3, 3) holdout machines in BusyBeaver/BB33/ and BusyBeaver/README.md to use their canonical community holdout identifiers and wiki designations, eliminating the repo-invented "See-Saw" name.

Community Name & Designation Audit on BB(3, 3)

Across the bbchallenge wiki (notably BB(3, 3) and Holdouts lists) and Justin Blanchard's canonical list of 925 holdouts, the 6 remaining holdouts are identified as follows:

1. Bigfoot (1RB2RA1LC_2LC1RB2RB_---2LA1LA):
   • Community name: Bigfoot (Holdout #829; discovered & analyzed by Shawn Ligocki and @savask).
   • Wiki page: Bigfoot.
2. Wily Coyote (1RB2LA1LA_2LA0RA2RC_---0LC2RA and 1RB2LA1LA_2LA0RA2RC_---1RB2RA):
   • Community name: Wily Coyote (Holdout #531) and Wily Coyote twin (Holdout #532; analyzed by Racheline and @LegionMammal978).
   • Wiki page: Wily Coyote.
3. Holdout #758 / #153 Pair (1RB2LC1RC_2LC---2RB_2LA0LB0RA and 1RB0LB0RC_2LC2LA1RA_1RA1LC---):
   • In PR Add 6 BB(3,3) holdout reductions, HasStackedCollatzReduction, and BB6/BB33 split #9, this pair was dubbed the "See-Saw" pair ("See-Saw counter machine", "See-Saw conjugate"). This name was made up within this repository and does not exist on the wiki or in community discussion.
   • On the wiki and in community discussions, these machines do not have an animal/cryptid moniker; they are identified strictly by their holdout numbers (Holdout #758 and Holdout #153), described as the probvious champion / probvious halter and a potential Cryptid.
   • This PR removes "See-Saw" entirely and replaces it with Holdout #758 and Holdout #153 (the probvious champion / halter pair).
4. Holdout #397 (1RB1LB2LC_1LA2RB1RB_---0LA2LA):
   • On the wiki, this machine does not have an animal/cryptid moniker either; it is designated as Holdout #397 (noted on the wiki as "similar to Wily Coyote", analyzed by @LegionMammal978 as a 6-carry sweep transducer).
   • This PR adds the canonical Holdout #397 identifier to its headers and table rows.

Changes

• BusyBeaver/BB33/README.md:
  • Replaced "See-Saw Pair" with "Holdout #758 / #153 Pair (Probvious Champion / Halter)".
  • Added community holdout numbers (#829, #531, #532, #758, #153, #397) to table rows and section headers.
• BusyBeaver/README.md:
  • Updated the BB(3, 3) summary bullet with canonical names and holdout IDs.
• Module headers & docstrings (BusyBeaver/BB33/):
  • M_1RB0LB0RC_2LC2LA1RA_1RA1LCHHH.lean: Replaced (BB(3, 3) See-Saw Conjugate) with (Holdout #153) and documented its relation as the conjugate of Holdout #758.
  • M_1RB2LC1RC_2LCHHH2RB_2LA0LB0RA.lean: Replaced (BB(3, 3) See-Saw Counter Machine) with (Holdout #758) and documented it as the probvious champion / halter.
  • M_1RB2RA1LC_2LC1RB2RB_HHH2LA1LA.lean: Added Holdout #829.
  • M_1RB2LA1LA_2LA0RA2RC_HHH0LC2RA.lean: Added Holdout #531.
  • M_1RB2LA1LA_2LA0RA2RC_HHH1RB2RA.lean: Added Holdout #532.
  • M_1RB1LB2LC_1LA2RB1RB_HHH0LA2LA.lean: Added Holdout #397.
  • WilyCoyote.lean: Added holdout numbers #531 and #532.

Verification

• All 7 modified Lean files typecheck cleanly (lake env lean).
• All modified/added lines in Lean files are $\le 100$ characters.
• Theorem names, namespaces, and challenge files (BusyBeaverChallenge.lean, comparator/busy_beaver.json) are untouched.

[mo271]

Thanks @TomZahavy — good catch replacing the repo-invented "See-Saw" name and aligning all 6 BB(3, 3) machines with their canonical wiki holdout numbers (#829, #531, #532, #758, #153, #397). Verified all 6 IDs and links against wiki.bbchallenge.org. LGTM!
(Heads-up on merge order: this touches L6 of BusyBeaver/README.md right below L5 touched by #22, so whichever lands second will have a tiny 2-line adjacent-line conflict there. Optional nit if rebasing: mentioning once in BusyBeaver/BB33/README.md's intro that the # IDs index the canonical 925-holdout BB(3, 3) list would make the numbers self-contained in-repo too.)