Continuation checkpoint: random-SAT evidence and computability limits

9 October 2026. Previous turn: community scope/benchmark progress, pushed and deployed at 48c315cf4dffafd43675e1029b7789f2e79acd19. This turn: progress through four selected family-235 manuscripts, a bounded proper-clause stream utility, independent finite controls and existing-solver comparisons. The perpetual goal remains active; no completion or blocked audit applies.

Findings and implementation

Proper clauses use distinct variables with fair signs; whole clauses repeat. Threshold existence, the older k=3 logarithmic variance upper bound, the newer linear-variance companion and threshold computability are separate claims. Selected formal scope still carries the older bound. Carenini retains priority for threshold existence. No source proof, native theorem algorithm or kernel ran.

The threshold computation proof supplies no efficiency estimate. Its displayed lower-certificate penalty alone requires n>=2^402 to fall to one. This is a condition on one term, not a universal runtime lower bound or sufficient total-accuracy guarantee. Its relaxed Poisson auxiliary model differs from the proper deterministic-clause-count fixtures.

The new utility preserves ordered repeated clauses, exact tiny first failures, independent SAT witnesses, distinct solver-claimed UNSAT bounds, right-censoring and explicit resource unknowns. A declaration is not proof of a random law. Exact mode stops beyond sixteen variables or its work budget. The optional CP-SAT adapter checks every SAT witness but does not independently certify solver UNSAT. Existing output directories are preserved.

For n=k=3, H is an eight-type coupon collector with mean 761/35 and variance 838034/11025. Removing replacement makes H=8; separately, clipping the correct process at eight makes min(H,8)=8. The exact figure shows how clipping changes moments. No limiting density or asymptotic variance fit is inferred.

Evidence and editions

• Report, exact coupon figure, summary.
• 679 passing controls: all 256 three-variable clause subsets, 200 independent assignment-oracle cases, twelve complete rank bijections, 101 inclusion-exclusion identities, caps/invalid inputs/resource limits and preserved CLI output.
• Sixty exact streams at n=6/10/16, twenty seeds per size, all complete by 10n. Nine CP-SAT first-failure claims agree with the exact oracle. Six larger n=40/80 cases remain solver-only UNSAT. A real 1e-9-second solver call returns UNKNOWN. Timing is not a fair solver comparison, and generated streams are not industrial customer evidence.
• Manifest: eighteen artifact files, including four inert tooling copies, and eighteen selected-source hashes. Ledger v18: 51 selected-section manuscripts, 147 source hashes and 668 pending/earlier-not-imported. Four PDF first pages were visually inspected; precise TeX/interface extents are recorded.
• Dossier 033 v2, catalog v30, directory v25, coverage v30.
• 41 utilities v27, priorities v27, feasibility v25: 32,107 controls in 65 reports. Facility Plan Auditor remains first; the SAT integration stays low confidence with no buyer or revenue claim.

Publication and continuation

Integrity v30 passed with zero issues: 32,107 controls, 157 current Python syntax checks, 1,546 local links, 147 reading-source hashes and all eighteen artifact/eighteen source-file hashes in the new manifest. The full rendered-site check follows this result.

Validate rendered routes, then push to strykesg/mathideas and verify Dokploy application 6yFD3JCmfp0uZcCuJGex2 serves the current report, figure and evidence bytes. Normal pushes/deployment remain authorized. No deletion, force push, outreach, purchase or paid compute occurred.

The 02:56:08 UTC upstream check found no change at source revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. Do not repeat before 03:56:08 UTC without a signal. The existing hourly heartbeat remains active while the app/host are available.

Continue with unreviewed manuscripts or substantive facility-product gaps. Stronger independently checked capacity bounds, standard-browser export completion and permissioned customer-study validation remain open. SAT follow-up would require a checked UNSAT-proof path and a realistic structured regression corpus before commercial priority increases.