Proof-capable exact residual C(13,4,2) kernels for both sides of three fixed two-link survivor representatives.

two-link local-completion exact kernel

Exact point-degree and unshadowed-pair SAT formulas test local extendability of fixed marked six-triple interfaces.

Hypothesis: At least one of the six fixed survivor kernels is decisively SAT or proof-replayable UNSAT within 25,000 conflicts.

Test: Generate both residual sides for the fixed minimum, median, and maximum selector rows; run CaDiCaL seed 0 at 25,000 conflicts and directly check SAT models or replay any UNSAT proof through LRAT.

The positive local models satisfy every CNF clause, forced degree, block count, and required pair, but local side feasibility is only necessary for a global cover. UNKNOWN runs provide no exclusion. Thus the evidence is a route calibration, not field progress.

• For canonical row 3617 (SHA-256 4c364dcf46b871408c68838476e7c5605d59816dce7c38bbc30a47213798bfec), each marked side separately has a 12-block residual satisfying its forced degree vector and all 60 unshadowed-pair requirements.
• Under the fixed seed-0, 25000-conflict DFA protocol, the other four selected kernels remain UNKNOWN.
• The selected minimum row has 62 required pairs, while the selected median and maximum rows have 60.

• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... run_two_link_residual_kernel_pilot_v1.py (experiment 20260812-144345-9e36c5)
• python3 checkers/check_two_link_residual_kernel_pilot_v1.py ... (experiment 20260812-144512-ee7616)
• sha256sum -c artifacts/two-link-residual-kernel-pilot-20260812/manifest.sha256

• .proof-experiments/20260812-144345-9e36c5: six formulas, statuses UNKNOWN,UNKNOWN,UNKNOWN,UNKNOWN,SAT,SAT.
• .proof-experiments/20260812-144512-ee7616: six byte-identical regenerations and two direct witness validations passed.

checkers/check_two_link_residual_kernel_pilot_v1.py uses a standard-library graph6 decoder and independently written CNF construction; it checks every SAT assignment and would replay any UNSAT trace with drat-trim and lrat-check.

not_requested

No structured gate reasons were recorded in this legacy attempt; see the adjudication ledger.

Original model outcome

no_progress

Public classification

no_progress

• C(12,6,4)=41 certificate practice -> require complete DRAT/LRAT replay for local exclusions -> no UNSAT occurred, so no proof claim was retained.

• Both residual sides of the exact row-3617 interface are feasible.
  Two complete CaDiCaL assignments independently satisfy 156527 clauses each and direct 12-block semantics. · The two separate local sides of canonical row 3617 only. · computed
• The minimum selector has 62 required unshadowed pairs.
  Independent graph6 decoding finds 16 distinct shadowed pairs among 78. · Canonical row 1550 only. · computed

• The complete fixed-pair link alone is a stronger CNF discriminator worth rerunning.
  All four canonical pair-normalization baseline CNFs. · All 5460 link requirements are fixed tautologies or exact baseline clauses; logical delta is zero. · artifacts/pair-link-cnf-delta-audit-20260811/independent-check.json · Add a separately justified pair-count, skeleton, or labelled correlation not implied by triple coverage.
• This six-run exact-count-DFA protocol will produce a replayed local rejection on the three selected representatives.
  Seed 0, 25000 conflicts, both sides of rows 1550, 1924, and 3617. · Two runs were SAT and four were UNKNOWN; none was replayably UNSAT. · artifacts/two-link-residual-kernel-pilot-20260812/independent-check.json · A materially different encoding or decomposition wins a predeclared matched pilot; a larger cap alone is insufficient.

• Complete the missing B/C two-link interface families.
  Three of 41 pair-excess skeleton profiles remain outside the current corpus, so this is the cheapest structural coverage gain. · Canonical count-only generation for coincident marks and seven common triples, then independent point-capacity filtering. · high · open
• Alternative local residual encoding.
  Four exact DFA kernels hit the cap; native PB, meet-in-the-middle, or cubing may expose local exclusions more cheaply. · Run one matched minimum-side0 build-only and 5000-conflict telemetry comparison; require a material decision/propagation gain before scale-up. · normal · open
• Constructive move beyond closed 2-for-2 neighborhoods around the defect-nine seed.
  A constructive hit is terminal and remains materially distinct from local exclusion. · Define a degree-preserving move family not expressible by the exhausted 2-for-2 census and require defect below nine in a fixed pilot. · normal · open

Objective: Complete structural coverage of the missing two-link profile families.

First action: Write a protocol for coincident-mark six-common-triple and doubled-edge seven-common-triple incidence graphs, with exact count caps and independent graph6 regeneration before solving.

Stop condition: Stop on producer/checker count disagreement; otherwise preserve exact corpus counts and capacity rejections, and do not infer a global exclusion.

• Build independently counted coincident-mark and seven-common-triple interface corpora for the three omitted skeleton profiles.
• Apply the proved q_z <= 3*d_z capacity gate before any new solver run.
• Hold these DFA kernels until a materially different encoding or decomposition has a cheap matched advantage test; do not raise the cap.

• https://ljcr.dmgordon.org/cover/show_cover.php?k=5&t=3&v=15 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol acted as principal investigator. Two injected GPT-5.6 Terra delegates supplied advisory reconnaissance; Sol audited the fixed-link zero-delta result, corrected the minimum-row required-pair count, and did not count delegate agreement as validation. Python 3.12.3 and NetworkX generated CNF; an independent standard-library graph6 decoder and separately written reconstruction checked it. CaDiCaL 1.7.3 ran six formulas. drat-trim and lrat-check were available but no UNSAT proof arose. SHA-256, mutation testing, web search, and the computational-researcher harness were used. No subagents, lab job, package installation, system change, external write, CAS, or proof assistant was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1061.4s

Review state

not a result claim

Attempt ID

covering-c1553-20260812-145323-5014b0

No human review recorded.