Emit supplemental-graph adjacency constraints lazily

[ciaranm]

The supplemental-graph adjacency constraints (exact-path/distance-2, distance-3, --k4 shape graphs) are derived in the PBP, not in the OPB, and were all emitted up front during model building. Most are never used. This makes them lazy — emitted only on first use — leaving the OPB byte-identical and the search tree unchanged (only PBP logging differs).

When is a supplemental needed?

A supplemental for antecedent (p,t) is needed exactly when x_p_t's value is decided by adjacency during search:

• assigned true — the forward-checking use (triggered from guessing / unit_propagating);
• removed from dom(p) by forward-checking — the branch-consequence a later Hall-set confinement cites in its RUP (triggered per removed value from the searcher's propagate_adjacency_constraints);

plus the root degree/NDS reads (materialised before their pol). Supplementals for (p,t) eliminated at the root (a kept unit suffices) or only removed by all-different (justified by a Hall pol) are never emitted.

This was established empirically first: keeping supplementals only for assigned (p,t) fails --distance3 proofs (the checker's RUP reconstructs a Hall confinement via the removed vertices' adjacency, in the reverse direction), whereas keeping assigned ∪ removed verifies across a 720-instance probe with 0 failures, deferring ~46% on average.

Implementation

create_*_graphs register a pending derivation keyed by (g,p,q,t) and indexed by antecedent (p,t); materialise_adjacency_for runs them on first use.

Mid-search materialisation needs care with proof levels: wiplvl N wipes every level ≥ N (that's how forget_level discards a subtree), and search uses levels depth+2, so a derivation scratches at active_level + 1 (its wiplvl clears only the scratch), emits the persistent @label at level 0, and the batch restores active_level once.

Results

• ctest 48/48 under release and sanitize (ASan+UBSan), including proof_*, the cake_* verified-pipeline, and random_proof_sweep.
• A 300-instance distance-3 / locally-injective / counting sweep all verify.
• OPB byte-identical to the eager version.
• Typically defers ~40–70% of supplemental derivations; on the search-light distance-3 instances that dominate those proofs, ~60% fewer PBP lines (e.g. 5405 → 2006).

🤖 Generated with Claude Code

[ciaranm]

Closing as won't-fix on master.

The lazy supplemental-adjacency work is landing on the pipeline/refactor integration branch instead, via #73 (now merged). There it's re-designed into the HomomorphismProofs middle layer and composes with the branch's other proof-economy phases — Phase 4 subsumption elision (strongest constraint per head) and the Phase 5 transient ensure/forget machinery — so lazy deferral (dropping heads never touched during search) is orthogonal and stacks on top rather than duplicating them.

This standalone master-based twin would diverge from that design and land the same mechanism twice, so it's being retired in favour of the integration-branch version. The refactor branch carries the capability forward to master when the umbrella PR (#69) merges. Branch proofs/lazy-adjacency left in place for reference.