Explain the CnC span reduction with a verified residual-structure audit

[isPANN]

Background

The current demo suggests that structure-aware region cubing can preserve aggregate conquer work while reducing maximum cube time and maximum conflicts. A performance table alone does not explain this effect. Moreover, region frontiers are much larger on disk than march_cu frontiers, creating a serious alternative explanation: region cubes may simply contain more assumptions or condition the problem more deeply.

This issue turns the observed span effect into a falsifiable and self-consistent mechanism claim. The easy demo instances are acceptable for exhaustive instrumentation; the hard-regime instances from #51 provide the external-validity check.

Objective

Determine whether region cubing lowers conquer span because it suppresses structurally large residual hard cores, or because it trivially leaves smaller/deeper residual CNFs per frontier task.

Positive, null, and reversed findings are valid. The deliverable must support one of the following evidence-backed conclusions:

1. Structural-core suppression: at comparable semantic residual size, region cubing reduces the upper tail of unresolved structural components, which predicts lower Kissat conflicts and maximum cube time.
2. Deeper conditioning: the apparent span advantage is explained by fixing more variables or information per frontier task.
3. Mixed mechanism: both effects contribute, with their measured contributions reported separately.

Falsifiable hypotheses

H0: depth/conditioning explanation

After matching or controlling for unit-propagated residual variables, clauses, primary inputs, and explicit decision information, the region-versus-CNF difference in maximum conflicts and cube time disappears.

H1: structural residual explanation

Region cubing reduces the upper tail of at least one preregistered structural residual measure, and that measure predicts held-out Kissat conflicts beyond generic CNF size/depth measures.

Candidate structural measures must be defined before inspecting their correlation with conquer time. The initial set is:

• largest unresolved connected component;
• longest unresolved carry-propagation chain;
• largest active tensor region;
• active-region boundary/interface size;
• unresolved partial-product and carry cells.

Required per-cube instrumentation

For every complete frontier, record:

• serialized assumption literal count and bytes;
• explicit decision count;
• implied assignment count and implied/decision ratio;
• unit-propagated remaining CNF variables and clauses;
• remaining original multiplier input bits;
• active native gates/cells;
• every preregistered structural residual measure;
• Kissat CPU time, wall time, decisions, conflicts, and terminal state;
• hashes linking the cube, native state, residual summary, CNF, and solver record.

Distinguish serialized literals from a semantically minimal decision basis. Re-propagate any minimized basis and verify that it produces the same residual formula or an explicitly defined equivalent state.

Controlled contrasts

Coordinate with #42 and include at least these matched arms:

1. region selector with region/multi-variable branching;
2. structure-blind selector with matched block arity and cutoff;
3. region ranking with single-variable branching;
4. region frontier serialized with all current assumptions;
5. the same region frontier serialized from a verified minimal decision basis.

The first three arms separate structural selection from branching arity and depth. The last two determine whether frontier size and solver behavior are affected by redundant implied literals rather than decomposition semantics.

Every labeled contrast must change only its declared mechanism. Configuration fingerprints must make accidental cutoff, propagation, encoding, or conquer-solver changes detectable.

Analysis

Residual audit

For each method and instance, report distributions and upper tails of:

• decision and assumption counts;
• unit-propagated CNF size;
• primary variables remaining;
• structural residual measures;
• conflicts and solve time.

Predictive mechanism check

Fit a preregistered model for log Kissat conflicts and log cube time using only calibration instances. Evaluate prediction on held-out instances in two stages:

1. generic predictors: decisions, remaining variables, and clauses;
2. generic predictors plus structural residual measures.

Report held-out error and whether structural features add predictive value. Do not infer a mechanism solely from in-sample correlation.

Method-effect check

Estimate the region effect before and after controlling for semantic residual size and the preregistered structural measures. Use the factoring instance as the statistical unit for confidence intervals; individual cubes are nested observations, not independent paper-level replicates.

Required figures:

• structural residual measure versus Kissat conflicts, colored by method and faceted by instance/width;
• upper-tail or survival curves for maximum residual-core size and cube time;
• an ablation table separating structure, block arity, cutoff/depth, and serialization.

Execution plan

Phase A: exhaustive demo audit

Instrument the existing 40/46/52-bit demo suite, where every cube can be analyzed cheaply. Use this phase to validate metric definitions, state reconstruction, minimal-basis equivalence, and plotting code. Do not present its runtime results as hard-regime CnC evidence.

Phase B: hard-regime validation

Apply the frozen instrumentation and analysis to the 9-instance pilot from #51. Do not add or remove structural measures after viewing hard-regime conquer results.

Proceed to the full 30-instance mechanism analysis only if instrumentation overhead and artifact volume are tractable and the Phase B records pass verification.

Verification

Provide an executable verifier that rejects:

• mismatched cube/residual/solver hashes;
• claimed explicit decisions that are actually implied;
• minimized cubes that do not reconstruct an equivalent residual state;
• contrasts that change more than their declared mechanism;
• structural metrics computed from test outcomes rather than pre-solve state;
• calibration/test overlap;
• cube-level pseudoreplication in reported confidence intervals;
• missing or silently censored tail cubes.

A negative-control fixture must deliberately add redundant implied literals. It should change serialized bytes but leave the verified semantic residual and structural metrics unchanged.

Deliverables

• Versioned per-node and per-cube residual schema.
• Instrumented demo and hard-pilot artifacts.
• Verified minimal-cube-basis transformation or a documented proof that the current representation is already minimal.
• The three required figures and attribution table.
• A short mechanism report selecting conclusion 1, 2, or 3 from the Objective and stating which observations falsified the alternatives.

Dependencies

• Attribute CnC outcomes to reductions, multiway branching, and rule optimization #42 for isolated selector, branching-arity, and reduction contrasts
• Evaluate candidate frontiers under finite-worker scheduling #44 for finite-worker consequences of the measured tail
• Build the hard-regime CnC work/span table on 64–80-bit UNSAT factoring #51 for hard-regime instances and held-out execution

Out of scope

• Treating correlation alone as a causal explanation.
• Designing a new selector after inspecting held-out mechanism results.
• Using task-specific CNF encodings.
• Claiming that smaller serialized frontier files imply easier semantic residuals.