docs(phase-31): cookbook §176a/b/c — the verification-layer laws, batch-gating mechanics, main clean-rebuild

Banking the PROCESS idioms this session produced, which were sitting only in commit messages,
tool docstrings and the wave prompt — none of which a future session reads.

- §176a VERIFICATION-LAYER LAWS: match_one verifies SHAPE not SYMBOL IDENTITY (masks
  jal/HI16/LO16 — a wrong callee or wrong global reports MATCH; func_8002A234 cost 5 gate
  attempts); a detector is ADVISORY and the gate is the ARBITER (3 wave-G drafts withheld on
  symfix flags all banked unchanged); a verifier that can pass WITHOUT BUILDING is worse than
  none (stale-binary false pass); an all-zeros gate result is a NULL not a finding; and the
  general rule — before believing a measurement, run the control that would make it FAIL.
- §176b BATCH-GATING MECHANICS: gate cost scales with (binary,TU) GROUPS not drafts; batched
  drafts must agree with EACH OTHER (type conflicts, duplicate typedefs); compatibility compares
  TYPE SIGNATURES ONLY but the declarator suffix matters (too-strict and too-coarse both bit me);
  conflict-dropped drafts are recoverable via cast-at-use; a COMPILE error names its own culprit
  so only a BYTE mismatch needs bisection.
- §176c MAIN CANNOT BE GATED INCREMENTALLY — psyq_integrate/ld_interleave rewrite the .ld;
  byte-proven both ways including with NO draft substituted. Use tools/gate_main.py.

Agent-discovered matching idioms are being mined from all 14 wave journals in parallel and land
next as §176.

docs/cookbook-index.md

@@ -2,7 +2,7 @@
 
 > **Generated by `tools/cookbook_index.py` — do not hand-edit** (R33). Regenerate after adding a cookbook section.
 >
-> `docs/matching-cookbook.md` is ~716 KB / 520 sections. Grepping it blind is how three P30 wave-1 agents each "discovered" an idiom that was already written down. **Start here, then read the section.** A section appears under every symptom it addresses.
+> `docs/matching-cookbook.md` is ~716 KB / 523 sections. Grepping it blind is how three P30 wave-1 agents each "discovered" an idiom that was already written down. **Start here, then read the section.** A section appears under every symptom it addresses.
 
 **How to use:** name what you SEE in the diff (a stolen delay slot, an extra `la`, a swapped register pair, a `conflicting types` error), find that symptom below, read those sections first. If nothing fits, THEN grind — and add a section when you win.
 
@@ -443,7 +443,7 @@
 - **§166** — THE DESTINATION-TU ORACLE (P30 S48): the seven-attempt bug that was never codegen  <sub>L14899</sub>
 - **§173** — THE STORED-PLUMBING RECOVERY RECIPE (P31 T6): symfix-first, per-group isolation, and where the verdicts have no drafts  <sub>L16603</sub>
 
-### build graph, splat & the harness  (109)
+### build graph, splat & the harness  (110)
 
 - **§4** — Flag/toolchain gotchas  <sub>L190</sub>
 - **Build** — mechanism — per-file opt override (splat resegmentation)  <sub>L288</sub>
@@ -554,6 +554,7 @@
 - **§165** — S48 WAVE-4 HARVEST (P30, 2026-08-12): banked the same day the wave landed  <sub>L13686</sub>
 - **§166** — THE DESTINATION-TU ORACLE (P30 S48): the seven-attempt bug that was never codegen  <sub>L14899</sub>
 - **§167** — S48 WAVE-5/6 HARVEST (P30, 2026-08-12): the saturation point  <sub>L14955</sub>
+- **§176c** — MAIN (SLUS_007.26) CANNOT BE GATED INCREMENTALLY  <sub>L16800</sub>
 
 ### process, measurement & doctrine  (73)
 
@@ -631,7 +632,7 @@
 - **§167z** — REFUTED IN WAVES 5/6: do NOT re-derive  <sub>L16151</sub>
 - **§168** — THE COUSIN TIER (P30 S49, 2026-08-12): h_seq's exact-hash brittleness, measured — and the similarity map above it  <sub>L16208</sub>
 
-### (unbucketed — title matched no symptom vocabulary)  (173)
+### (unbucketed — title matched no symptom vocabulary)  (175)
 
 - **§3-How** — to use this  <sub>L30</sub>
 - **§1** — Idiom catalog (asm pattern → C that produces it)  <sub>L39</sub>
@@ -806,6 +807,8 @@
 - **§172a** — TWO DECOMPILATION TELLS FROM THE SAME DIG (P30 S50-Max)  <sub>L16554</sub>
 - **§172b** — THREE MORE TELLS FROM THE GCC READ (P30 S50-Max, banked on Drew's ask)  <sub>L16570</sub>
 - **§174** — THE ADAPT-CARD WAVE RECIPE (P31 waves A/B, 2026-08-14): prevention beats recovery  <sub>L16639</sub>
+- **§176a** — THE VERIFICATION-LAYER LAWS (P31 overnight, 2026-08-15). What each check can and cannot prove.  <sub>L16734</sub>
+- **§176b** — BATCH-GATING MECHANICS (P31): what changes when N drafts land in ONE .c  <sub>L16774</sub>
 
 
 ## All sections, in order
@@ -1330,3 +1333,6 @@
 - **§173** — THE STORED-PLUMBING RECOVERY RECIPE (P31 T6): symfix-first, per-group isolation, and where the verdicts have no drafts  <sub>L16603</sub>
 - **§174** — THE ADAPT-CARD WAVE RECIPE (P31 waves A/B, 2026-08-14): prevention beats recovery  <sub>L16639</sub>
 - **§175** — A CALLER-SAVED REGISTER PIN CAN BE A CORRECTNESS BUG, NOT JUST A SCHEDULING CHOICE (P31 wave H, 2026-08-15)  <sub>L16709</sub>
+- **§176a** — THE VERIFICATION-LAYER LAWS (P31 overnight, 2026-08-15). What each check can and cannot prove.  <sub>L16734</sub>
+- **§176b** — BATCH-GATING MECHANICS (P31): what changes when N drafts land in ONE .c  <sub>L16774</sub>
+- **§176c** — MAIN (SLUS_007.26) CANNOT BE GATED INCREMENTALLY  <sub>L16800</sub>

docs/matching-cookbook.md

@@ -16730,3 +16730,80 @@ instruction, on a draft carrying a caller-saved pin, is this bug until proven ot
 
 **Why the gate doesn't save you cheaply:** the draft is *wrong code*, not merely unmatched, so it
 fails standalone too — you pay a full diagnosis cycle. This is prevention, like §174's laws.
+
+## §176a — THE VERIFICATION-LAYER LAWS (P31 overnight, 2026-08-15). What each check can and cannot prove.
+
+These are not matching idioms; they are the rules for *believing* a matching result. Every one was
+paid for in gate cycles this session.
+
+**1. `match_one` verifies INSTRUCTION SHAPE, not SYMBOL IDENTITY.** It masks jal/HI16/LO16
+relocations, so a draft that calls the WRONG FUNCTION or loads/stores the WRONG GLOBAL reports a
+clean MATCH. Byte-witnessed: `func_8002A234` (14 ins) stored `v1`→`D_80078EE8` and `0`→`D_80078EE4`
+where the target does the exact reverse; `match_one` said MATCH, the whole-binary build differed in
+2 bytes, and it cost five gate attempts. Same root cause as the invented PsyQ names in waves F/G
+(`S80131E00`→`Square0`, `Blk20_…`→`RotMatrixY`, `SRM_…`→`RotTransSV`).
+**Rule:** after MATCH, re-read the target `.s` relocation lines and check every symbol you wrote —
+each callee, each data symbol, and *which* symbol each load/store touches. Shape ≠ correctness.
+
+**2. A detector is ADVISORY; the whole-binary gate is the ARBITER.** `aprop_symfix` flags
+`STALE`/`AMBIGUOUS` on LOCAL identifiers (typedef names, inline-asm macro names) and its
+draft-symbol extraction misses some `extern` forms, so a name the draft *does* declare can still
+report `asm-only`. Three wave-G drafts were withheld on such flags; all three banked **unchanged**
+when finally gated. **Never withhold a standalone-MATCH draft on a flag alone** — gate it and let
+the bytes decide (R39: a refusal check that silently discards good work is worse than one that lets
+a few failures through).
+
+**3. A verifier that can pass WITHOUT BUILDING is worse than no verifier.** `gate_main` read the
+output binary's SHA after `make build`; when the build FAILED on a compile error the *previous*
+binary was still on disk, so it returned the good hash and reported BYTE-IDENTICAL for a build that
+never ran ("43 banked" on a TU that did not compile). The clean-fleet R22 caught it.
+**Rule:** delete the artifact before building, and treat a non-zero build exit as no-hash/never-pass.
+
+**4. An all-zeros result is a NULL, not a finding.** `gate_lane` swallows `gate_stage`'s stderr, so
+an unhandled `corpus.CorpusError` surfaced as `banked 0, near 0, failed 0` — indistinguishable from
+an honest "nothing banked", twice. A real gate always classifies its drafts. If every bucket is
+zero, the tool did not run; run `gate_stage` directly to see the exception.
+
+**5. Before believing a measurement, run the control that would make it FAIL.** The night's largest
+false conclusion — "main is blocked by a linker defect", complete with three hypotheses — died to
+one control: build with **NO draft substituted at all**. The "defect" reproduced with zero drafts,
+proving it was the build path, not the code. A null input, a known-answer population, or an
+independent oracle. R35 says fix the instrument first; this is the sharper form — *confirm the
+instrument can answer, and that it answers correctly on a case whose answer you already know.*
+
+## §176b — BATCH-GATING MECHANICS (P31): what changes when N drafts land in ONE .c
+
+**Gate cost scales with (binary, TU) GROUPS, not with drafts.** Each group is one whole-binary
+rebuild. Wave D was 42 drafts spread over 23 groups (~40 min of gate); waves F–N were 40–56 drafts
+in **1** group. `tools/build_wave_atlas.py` packs a wave into few TUs for exactly this reason — it
+is free throughput, purely a selection change.
+
+**Batched drafts must agree WITH EACH OTHER, not just with the file.** Each draft is written to
+compile standalone, so N drafts bring N independent `extern` sets into one TU:
+- **Type conflicts:** `D_800A4ED4` declared `s16` by one draft and `u16` by another; `func_8001C9D0`
+  as `void` / `void *` / `s32` across three. C rejects the TU.
+- **Duplicate typedefs:** every draft carries its own `typedef struct {…} SVECTOR;`. Once one banks,
+  that typedef lives in the `.c` forever and every later draft collides. Strip duplicates on
+  substitution (`harvest_verify` already did; `gate_main` now does).
+- **Compatibility compares TYPE SIGNATURES ONLY.** Parameter *names* are irrelevant to C — a checker
+  that compares them wrongly discards good drafts (my first version dropped 2 that way). But the
+  DECLARATOR SUFFIX absolutely matters: `u8 D_x` and `u8 D_x[]` are incompatible, and ignoring it let
+  a real conflict reach the build (my second version). Too-strict and too-coarse are both defects.
+- **Recovery, not rejection:** a conflict-dropped draft is usually CORRECT. Adopt the other
+  declaration **verbatim** and adapt at the USE site — `extern u8 D_80076251;` + `(&D_80076251)[i]`,
+  or `void f(s32 a0)` + `D_x[(s16)a0]` — which emits identical bytes (§174 Law 4).
+
+**A COMPILE error names its own culprit; only a BYTE mismatch needs a search.** Bisecting a batch
+costs a full clean rebuild per step (a 41-draft bisect ran 28 minutes producing nothing) while the
+compiler had already printed the symbol and line. Read the error first.
+
+## §176c — MAIN (SLUS_007.26) CANNOT BE GATED INCREMENTALLY
+
+main's `make extract` runs the EXE-only `psyq_integrate` + `ld_interleave` steps, which **rewrite the
+linker script**. `gate_lane`/`gate_stage` build incrementally, so they re-run that on an
+already-rewritten `.ld` and produce a **false diff** — precisely the trap R22's own rationale
+describes, and the reason main sat at 0.5% being treated as the project's hardest mass.
+**Byte-proven both ways:** `make extract BINARY=main && make build BINARY=main` → `143dbb89…`
+BYTE-IDENTICAL; `make build` alone → `c4546248…` and a 2-byte `jal` diff, deterministically, *even
+with no draft substituted*. Use `tools/gate_main.py` (substitute batch → extract → build → SHA);
+ONE clean rebuild verifies a whole batch. main then drafts like any overlay (98–100%).