Validate the factoring mechanism: low-bit residue lifting, carry propagation, and encoding robustness

[isPANN]

Context

This is a mechanism-focused follow-up to #56 and a concrete factoring case study for #53.

Issue #56 establishes the end-to-end CnC result, but it does not yet explain what the region brancher is exploiting inside the multiplier, nor separate three different notions that can easily be conflated:

1. the semantic mechanism in the multiplier circuit;
2. a local CNF rewrite of the same circuit (output-alias-v1 vs output-direct-v2);
3. a different multiplier decomposition (array-tseitin-v1 vs the current row-ripple/majority-carry circuit).

The paper claim should not be generic “encoding invariance.” The working claim is narrower and mechanistic:

Region branching discovers a low-order modular decomposition of multiplication. A shallow macro branch fixes a consistent residue class of the factor pair modulo 2^k; fanout through partial products and, especially, the carry network then amplifies those few semantic choices into a much larger closure.

Cover is sufficient for the SAT/CnC use here. Whether a branching formalism additionally requires a partition is orthogonal to this mechanism and is not a main objective of this issue.

Frozen setting

Use the same ten 30-bit UNSAT target integers and the same current CircuitSAT instances as the completed server run:

• artifact root: artifacts/factoring-unsat-main-w30-w32-v1/
• semantic cutoff: --cc-threshold 2048
• current CircuitSAT size: 5,280 variables
• frozen cuber SHA-256: 72c58f21fba3b0325bab2fced8052ea060bbda0a2c4fe73f5df4ad552d4ee928
• Kissat SHA-256: 07da6866c339de638458a7867f8d11a17162046878b552cadd22b265a8b5e7b1
• march SHA-256: a0236ad5634fb680fa84220ad6806e5def15bca4d9c8850f1abbc397cedec416

Primary audit directories:

• structural-audit-w30-t2048-v1/
• encoding-ablation-w30-t2048-v2/

Evidence already collected

1. The semantic frontier is shallow, but its propagation closure is large

Exact replay of the frozen trace gives:

• 3,331 leaf cubes;
• mean leaf macro depth: 2.672;
• mean rule size: 63.98 semantic variables;
• mean feasible branches per rule: 7.47;
• per branch edge: 58.78 explicit decisions and 394.93 newly propagated assignments on average;
• per leaf: 139.89 explicit decisions, 1,235.84 assigned variables total, and 973.31 additional assignments after excluding root propagation and decisions;
• assignment amplification: 8.089×.

Decision literals are concentrated in the multiplier rather than only at its inputs:

• factor bits: 12.50 per leaf;
• partial products: 43.83;
• sum wires: 24.16;
• carry components: about 59.4 combined;
• decisions reach only through row 9, with most mass in the earliest rows.

The additional BCP closure is even more concentrated:

• carry network: 728.94 assignments per leaf;
• partial products: 223.99;
• sums: 15.10;
• factor bits: 5.21.

Factor-false decisions correlate with newly fixed partial products (Pearson r=0.719) and with total additional propagation (r=0.675), consistent with a causal path
factor bit = 0 -> partial-product fanout collapses -> carry constraints propagate.

2. The branches behave like low-bit modular residue lifting

At the first macro branch, the median child fixes contiguous 6-bit prefixes of both factors, and every child satisfies a_<6 b_<6 = N (mod 2^6).

At the leaves, the median contiguous prefix is 10 bits for each factor, and every leaf satisfies a_<10 b_<10 = N (mod 2^10).

Almost no factor assignments lie outside those prefixes (mean 0.1009; p95 = 0).

Most importantly, replacing a full semantic leaf cube by only its contiguous factor-prefix assignment produces exactly the same BCP closure on all 5,280 original wires for 3,211/3,331 leaves (96.4%). Every prefix closure is a subset of the macro-cube closure; p95 missing assignments is 0, with a mean of 6.67 due to a small tail.

This is the strongest current evidence for the mechanism: the macro branch is usually a redundant, propagation-friendly certificate of a much simpler modular state.

3. output-alias-v1 vs output-direct-v2 is a pure representation ablation

For the exact same CircuitSAT instances and frozen semantic frontiers:

• v1: 11,280 variables / 31,050 clauses;
• v2: 6,120 variables / 20,730 clauses;
• all 3,331 paired cubes have identical BCP assignments when projected to the 5,280 original circuit wires;
• conquer geometric means, v2/v1: conflicts 0.9961 and CPU 0.9913; bootstrap intervals include 1;
• hard-cube ordering is similar but not identical (median Spearman 0.963; median hardest-5 overlap 0.770);
• march produces exactly the same cube count for all ten instances at the same active-variable cutoff;
• 1,827 paired march cubes have identical projected BCP closure on the original wires.

Therefore the observed equivalence is expected: v2 eliminates local output aliases without changing the projected propagation relation. It supports robustness to this rewrite, not robustness to arbitrary CNF encodings.

4. Old array-tseitin-v1 is a topology/decomposition change, not a clean encoding rewrite

The old and current benchmarks use the same ten target integers, but their internal circuits differ:

• old Array-Tseitin: 5,460 variables / 17,820 clauses, maximum clause width 3, regular 30×30 full-adder grid;
• current direct-v2: 6,120 variables / 20,730 clauses, including 840 width-4 clauses, constant-folded row-ripple circuit with majority carries;
• old full adder uses propagate/generate intermediates,
  t = x xor y; s = t xor cin; cout = (x & y) | (t & cin);
• current full adder directly encodes
  s = x xor y xor cin; cout = maj(x, y, cin).

Over all 167 consistent partial assignments to the external full-adder ports, projected unit propagation agrees on 161 and differs on 6; current is propagation-complete on 153, old on 151, and neither dominates.

Under the same portable low-factor-prefix assumptions:

• old extra fixed variables: mean 906.93;
• current extra fixed variables: mean 1,088.85;
• old/current ratio: 0.833;
• normalized extra fixed fraction: 0.1735 vs 0.2119.

This comparison mixes topology and gate encoding, so it must not be presented as a pure encoding ablation.

A CNF-native cuber is visibly sensitive to the difference. At the same post-preprocessing active-variable reduction (736 variables), old/current march cube counts have a geometric-mean ratio of 8.955. In an equal raw-offset diagnostic, march decisions on the old array are 92.4% partial-product variables, whereas on the current CNF they split roughly between factor bits (44.2%) and partial products (47.1%). One concrete mediator is maximum clause width: the old 3-CNF and current width-4 CNF select different march scoring regimes.

The paired monolithic Kissat run at 1,800 seconds per instance is still in progress under structural-audit-w30-t2048-v1/monolithic-kissat/. Its result is supplementary and should not gate the mechanism claim.

Predictions to test

If the low-bit residue-lifting account is correct:

1. Portable factor-prefix cubes should retain most of the propagation and conquer advantage across faithful multiplier encodings, even when internal auxiliary variables cannot be mapped.
2. A semantic region brancher should be substantially less sensitive than march to local Tseitin aliases and CNF variable numbering.
3. Changing the multiplier topology should move the propagation mass and possibly change the useful semantic regions:
   • ripple/array multipliers should emphasize low columns and carry chains;
   • carry-save/Wallace trees should reduce sequential carry propagation and expose a different layered mechanism.
4. Removing carry literals from the macro cubes should hurt propagation more than removing sum literals; removing the corresponding low factor-prefix information should destroy the modular interpretation.
5. The same abstraction should transfer to other bit-vector constraints with directional local propagation (adders, comparators, bounded arithmetic), but not automatically to CNF-native SAT families without a meaningful semantic interface.

Required experiments

A. Make the modular state portable

For every frozen leaf:

• extract the maximal contiguous prefixes of a and b;
• verify the residue equation modulo 2^k;
• compare full macro-cube and prefix-only BCP closures;
• deduplicate/subsume prefix cubes and independently verify that they still cover the original problem;
• conquer the resulting portable frontier on both current direct-v2 and old Array-Tseitin using the same worker policy.

This is the cleanest cross-encoding test because it maps only primary factor bits.

B. Separate gate encoding from circuit topology

Build two backends from one semantic multiplier IR:

• current direct XOR3/majority full adder;
• propagate/generate full adder.

Keep multiplier topology, constant folding, primary variables, outputs, and targets fixed. Compare:

• projected BCP on semantic ports;
• native region frontiers at t=2048;
• portable-prefix frontiers;
• full conquer cost and tail distribution.

Do not replay unmappable internal-wire cubes across different IRs.

C. Test topology as a mechanism intervention

Add at least one structurally different multiplier (carry-save/Wallace is preferable). Measure by column/layer:

• selected semantic roles;
• newly propagated assignments;
• prefix depth k;
• macro depth and frontier size;
• conquer conflicts/time.

The goal is not merely another performance point: it is to test whether the mechanism moves in the predicted way when carry propagation is changed.

D. Causal cube ablations

On the frozen current frontier, compare:

• full macro cube;
• factor-prefix-only cube;
• factor bits present in the macro cube;
• macro cube with carry literals removed;
• input-only binary branching at matched frontier size.

Report both mean and tail behavior, since the rare 3.6% prefix-mismatch leaves may matter disproportionately to conquer cost.

E. Algorithm-sensitivity matrix

Evaluate each representation with:

• semantic region branching;
• march, using a calibrated semantic stopping criterion rather than the same raw DIMACS variable offset;
• monolithic Kissat;
• Kissat conquer on one shared portable frontier.

This distinguishes an invariant problem decomposition from representation-specific behavior of a CNF-native heuristic.

Acceptance criteria

• One versioned analysis command reconstructs every reported number from raw traces/artifacts.
• Exact target list, generator/backend names, command lines, seeds, timeouts, worker counts, and binary hashes are recorded.
• Cover is independently verified for every new frontier; partition is reported only if explicitly enforced.
• Pure alias rewrite, gate encoding, and multiplier topology are never grouped into one “encoding” variable.
• The paper can include one auditable mechanism figure: low factor prefixes → partial-product collapse → carry-network propagation → large closure.
• The paper can include one encoding × algorithm table separating semantic branching, march, and CDCL effects.
• Claims are labeled at the right strength:
  • supported now: modular residue interpretation; carry-dominated propagation; v1/v2 projected equivalence;
  • open: topology robustness; causal performance mediation; transfer beyond multiplication.

Existing audit files

Under structural-audit-w30-t2048-v1/:

• semantic-trace-structure.json
• bcp-structure.json
• native-vs-bcp.json
• fanout-propagation.json
• modular-prefix.json
• macro-vs-prefix-bcp.json
• cnf-structure.json
• array-vs-current-prefix-bcp.json
• march-ablation/summary.json
• march-ablation/equal-active-reduction/summary.json

Under encoding-ablation-w30-t2048-v2/:

• paired-analysis.json
• bcp-audit.json
• march-v1-v2/summary.json