C-D25-COMPOUNDING

D25 clause compounding VALIDATED-BOUNDED (pilot measurements): the rational-time clauses COMPOUND on reachable branches. Measured on the pilot: about 32 greedy rational times reduced a 4000-branch reachable sample to a handful, at about 0.95 per-clause survival. From that rate, roughly 555 clauses would project to bring the 2^84 reachable residue space below the 2^42 caps. That ~555 figure is an EXPLORATORY PROJECTION, NOT a certified bound: it does not yet account for the new residue variables each new denominator introduces, correlations between clauses, the SAT / decision-diagram size, the proof-certificate cost, or keeping one common tuple across all moduli. So the compounding is a genuine qualitative gain over D24, but the campaign-size claim is unproven

In plain language

Adding many separate clocks clearly multiplies the pruning, and a rough count suggests a few hundred could shrink the search below the limits. That count is an exploratory estimate, not a proof, since it ignores several real costs.

Exact statement

D25 clause compounding VALIDATED-BOUNDED (pilot measurements): the rational-time clauses COMPOUND on reachable branches. Measured on the pilot: about 32 greedy rational times reduced a 4000-branch reachable sample to a handful, at about 0.95 per-clause survival. From that rate, roughly 555 clauses would project to bring the 2^84 reachable residue space below the 2^42 caps. That ~555 figure is an EXPLORATORY PROJECTION, NOT a certified bound: it does not yet account for the new residue variables each new denominator introduces, correlations between clauses, the SAT / decision-diagram size, the proof-certificate cost, or keeping one common tuple across all moduli. So the compounding is a genuine qualitative gain over D24, but the campaign-size claim is unproven