# 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](../../../../prototypes/random-sat-stream-2026-10-09-v1/report.md) 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](../../../../opportunities/033-random-sat-benchmark-calibration/2026-10-09-v2.md) 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`.