ci(integration): verify canonical aggregate-only merge resolutions #2274

Available follow-up from queue coordination (logsQ-queue-20261101), building on completed #672. Adjacent generated-import insertions can make a strict neutral merge conflict only in Complexity.lean even when every reviewed nonaggregate payload composes unchanged. This occurred for #2244’s earlier 46c1403b against #2220/c26810eb; a retained external coordinator subsequently refreshed that PR, so no custom candidate was admitted by this lane. The ownership/context handoff preserves that distinction.

Add a small report-only verifier for this exact generated-file case: require the complete conflict set to be {Complexity.lean}, identical known preambles and otherwise valid import declarations; regenerate the canonical inventory using mk_all conventions. Prove every nonaggregate mode/blob unchanged from the ordinary merge, preserve both reviewed payloads, and recover the exact prefix by reversing the feature and restoring its aggregate. Compare the result with the ordinary GitHub-representable merge; report a limitation if it differs. Do not mutate source branches, enable union for arbitrary Lean files, enqueue, bypass checks or modify main.

Completion requires positive fixtures for adjacent independent import additions/deletions and negative fixtures for another conflicted file, changed preamble, a declaration/option hidden among imports, malformed/duplicate/missing imports and a noncanonical default merge. Existing source review, exact candidate/parent records and all six required queue checks including mk_all --check remain integration gates. This is bounded coordinator tooling, not a new merge policy or mathematical result. No implementation owner is claimed. AI assistance: OpenAI Codex.