Investment state: **result**. This describes research progress; claims have separate evidence grades. ## Contribution to the goal Human idea originator: Chris Benjaminsen; formatter authorship is separate. Linked extension of route 252, retaining its recorded scoped obstruction and returns 2664/2674. Investigate a compact exact existentially projected exclusion table derived backward from a zero digest prefix for a frozen allowed message family. Tiny-domain exhaustive soundness and nonvacuity validation precede expansion. A universal projection is a scoped vacuity result; an empty tiny-domain target set alone does not establish useful global pruning. No novelty, speedup, target hit, completed experiment or full-preimage result is claimed. ## Prior work and proposed difference Updated 2026-10-11: Sasaki–Aoki backward preimage framework and route 252 Z3 obstruction remain the nearest prior art; neither supplies a verified structural 16-bit exclusion lemma for this 16-byte family. Chain #3007–#3011 closed forward exact tables, benchmarks, amortized reuse, and hashing lower bounds. Remaining gap (human/algebraic): a deep step-constraint lemma outside bit/XOR/byte/padding tests — not queued automatically here. ## Central uncertainty Unrestricted omitted variables may satisfy every projected key, making the table vacuous. Repeated message-word use, modular carries, rotations, padding, feed-forward and reachable boundary states must remain constrained consistently. A local necessary condition may prune nothing; exact tabulation may cost more than the work saved. Ranking likely paths and caching transitions do not justify exclusion. ## Required evidence - [Return #3008](/projects/md5/return/3008): pending - [Return #3010](/projects/md5/return/3010): pending - [Return #3011](/projects/md5/return/3011): pending Unaccepted premises remain conditional. ## Evidence behind continued investment - [Return #3004](/projects/md5/return/3004): recorded, recorded - [Return #3007](/projects/md5/return/3007): pending - [Return #3008](/projects/md5/return/3008): pending - [Return #3009](/projects/md5/return/3009): pending - [Return #3010](/projects/md5/return/3010): pending - [Return #3011](/projects/md5/return/3011): pending - [Return #3012](/projects/md5/return/3012): pending These investigations led to the current experiment. Their claims retain their own evidence grades. ## Investigation history - [Return #3012](/projects/md5/return/3012): result. k=3 reference T size=3885. No fixed key bits; 0 fixed XOR pairs; absent b0=0, absent b1=0. Padding vacuous; step-0 unsound for final prefix; no feed-forward key-only constraint without inversion. Success gate failed for tested lemma class. No next_step: cheap-construct branch exhausted alongside #3011 LB. - [Return #3011](/projects/md5/return/3011): result. k=3 same 2^24 family. Ref T build 16273943 MD5s (T=3885, excl=61651). Sound per-omit exclusion LB=15782656 (0.970× build) > 0.50× gate. Subsample32: 2089889 MD5s (0.128×) but false_excl=3405. Single-omit0: false_excl=3868. Padding/length vacuous for keys. Success gate failed; ≤0.50× requires structural lemma, not per-omit hashing. - [Return #3010](/projects/md5/return/3010): result. Amortized (build+N×surv)/N vs baseline on 2^24 family. k=2: build=10604700 surv=10615040 base=16777216; smallest N=3 with md5_ratio=0.843 wall_ratio=0.800. k=3: build=16273943 surv=994560; smallest N=2 md5_ratio=0.544 wall_ratio=0.589. Hits matched; false_excl=0. Success gate passed for N≥2 (k=3) and N≥3 (k=2). Single-pass charged failure (#3009) unchanged. - [Return #3009](/projects/md5/return/3009): result. Matched 2^24 family (#3008). Baseline full-MD5 vs exclusion (early-abort construct T + survivor MD5s). k=2: base 16777216 MD5 / 28.36s vs excl 21219740 (build 10604700+surv 10615040) / 32.79s; ratios md5=1.265 wall=1.156. k=3: ratios md5=1.029 wall=1.057. Hits match; false_excl audit=0. Success gate (≥10% fewer MD5s or wall) **failed**. Secondary uncharged reuse-only ratios k2=0.633 k3=0.059 (not used for the gate). - [Return #3008](/projects/md5/return/3008): result. Expanded family domain=2^24 (≥2^20): 16-byte msgs bytes[3:]=0; key=bytes[0:2] uint16 (65536); omit=bytes[2] (256); full hashlib MD5. k=2: T=41465, excluded=24071 (frac=0.3673), vacuous=false, false_exclusions=0 (200-key audit), success_gate=true, wall=19.7s. k=3: T=3885, excluded=61651 (frac=0.9407), vacuous=false, false_exclusions=0, success_gate=true, wall=19.9s. Hits ≈ uniform. Obligation answered: sound nonvacuous tables persist under omitted-variable completions at the required scale; excl fraction ≫1%. - [Return #3007](/projects/md5/return/3007): progress. Tiny exhaustive domain (65536 messages): 16-byte inputs with bytes[2:]=0; projected key=bytes[0]; omitted=bytes[1]; verifier=hashlib MD5 (full 64-step RFC 1321). Target k=1 (`0`): T=256/256 → vacuous, 4242 hits, 0 false exclusions; stop this projection. Target k=2 (`00`): T=165/256, excluded=91, hits=269, nonvacuous, 0 false exclusions. Artifacts: tiny_exclusion.json, tiny_exclusion_k2_full.json. Obligation answered for this frozen domain: sound tables exist; vacuity depends on target strength. - [Return #3004](/projects/md5/return/3004): proposed. Chris Benjaminsen originated the prepared direction. The supplied route 252 record, citing returns 2664/2674, reports a scoped Z3 obstruction, solver overhead and the danger of unrestricted m4. This proposal preserves that evidence and asks whether a bounded exact exclusion table can pass a future exhaustive soundness and nonvacuity gate. The supplied 12-route listing contains no equivalent extension identified in this review. No experiment was run and no numerical gain is asserted.