Random SAT: finite benchmark evidence and computability limits

Selected reading now separates all four manuscripts and the four selected formal interfaces. Proper clauses have distinct variables; whole clauses repeat. The newer 3-SAT variance companion removes the older logarithmic upper bound, without extending the reviewed formal scope. Threshold computability supplies no practical efficiency estimate; its displayed lower penalty alone is at most one only at n>=2^402.

Detailed report records exact reading extents, coupon/censoring identities, a bounded stream audit, 679 passing controls and conventional CP-SAT comparisons. Solver-reported UNSAT remains separate from independent evidence. No source proof, kernel or threshold algorithm was executed. Carenini's priority is retained.

Opportunity 033 v2 remains a low-confidence benchmark integration. Existing solvers already handle the examples; customer value and a checked UNSAT-proof path are open. Facility planning remains first. Source revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb.