Compiled canonical type 4 into the exact three-way lambda_45 count partition q in {5,6,7}, independently reconstructed it, and ran a matched 5000-conflict discriminator.

exact second-pair count branching

A shared truncated unary counter on the 275 blocks containing {4,5} generates three disjoint exact-count leaves.

Hypothesis: Conditioning canonical type 4 on lambda_45 in {5,6,7} produces a checked decisive leaf or at least 20 percent fewer decisions in every leaf than the unsplit control.

Test: Validate the exact partition, then run the control and q=5,6,7 leaves with CaDiCaL 1.7.3, seed 0, and 5000 conflicts.

The exact, compact encoding isolates branch quality as the failure. UNKNOWN results exclude no assignments.

• The three CNFs exactly partition canonical type-4 base models by lambda_45=5,6,7.
• The shared counter adds exactly 1092 variables and 6245 clauses.
• Decision ratios q5, q6, q7 versus control are 1.5633396637827952, 1.5578532742491384, and 1.8915382992192447; all statuses are UNKNOWN.

• Producer experiment 20260811-142843-ca2fdb generated and ran the three branches.
• Experiment 20260811-142926-207020 independently reconstructed 594090 base clauses and 6245 counter clauses per branch.
• Experiment 20260811-142943-1737cb rejected four material mutations.
• sha256sum -c artifacts/type4-pair45-count-split-20260811/manifest.sha256 passed.

• .proof-experiments/20260811-142843-ca2fdb: all four cases UNKNOWN; all leaf decision ratios exceeded one.
• .proof-experiments/20260811-142926-207020: independent reconstruction PASS.
• .proof-experiments/20260811-142943-1737cb: 4/4 mutations rejected.

check_type4_pair45_count_split_v1.py imports no producer code; it reconstructs the counter and branch suffixes, derives the range, reparses logs, checks SAT models, and replays LRAT if an UNSAT leaf arises.

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

• Certificate-first covering search -> validate a complete semantic split before scaling -> the split was exact and compact but all leaves regressed, falsifying aggregate pair count as a useful branch signal here.

• Every canonical type-4 base model has lambda_45 in {5,6,7}.
  Coverage lower bound and point-excess upper bound. · Canonical type-4 base semantics. · proved
• The saved q5, q6, q7 CNFs exactly partition the base-model set.
  Independent clause and threshold-unit reconstruction. · The three hash-bound CNFs. · computed
• All three leaves regress at the fixed telemetry protocol.
  Independently reparsed solver logs. · CaDiCaL 1.7.3, seed 0, 5000 conflicts. · computed

• Scale this exact lambda_45 split solely by increasing its cutoff.
  Canonical type 4, shared balanced counter, CaDiCaL 1.7.3 seed 0. · All leaves remained UNKNOWN and used 55.785 to 89.154 percent more decisions. · result.json and independent-check.json · A materially different solver or branching mechanism passes a matched multi-seed gate or produces a checked decisive leaf.
• Present the q range as a new structural constraint.
  Canonical type 4. · The pair identity and threshold semantics already existed in prior campaign artifacts. · sources/search/type4-pair45-count-split-audit-20260811.json · A genuinely stronger invariant.

• Strict-five deletion-cell signature quotient.
  It measures reusable bulk structure across the complete 3162510-cell constructive neighborhood. · Run a dual-checked 10000-cell signature pilot before enumerating completions. · high · open
• Variable-length exact-degree ejection chains.
  A checked 54-cover has a small verification surface and this differs from completed fixed-size neighborhoods. · Run one deterministic tranche accepted only on independently checked defect below ten. · normal · open

Objective: Measure whether the strict-five constructive neighborhood admits a large exact quotient before further completion search.

First action: Implement a count-only 10000-cell pilot keyed by exact insertion-demand vector and retained-coverage mask, with independent reconstruction.

Stop condition: Redirect on key disagreement, infeasible uncheckpointed runtime, or below-gate compression.

• Do not rerun this exact q split solely at a larger cutoff.
• Pilot the complete strict-five deletion-cell signature quotient on the locked defect-ten seed.
• Retain negative SAT work only when a branch yields a replayable proof or a new heuristic passes a matched gate.

• https://www.coveringrepository.com/systems.aspx?k=5&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?k=5&t=3&v=15 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol principal audited the Terra memos, rejected stale suggested routes, designed and executed the discriminator, and interpreted it. GPT-5.6 Terra delegates supplied advisory reconnaissance only. Python 3.12.3 generated and independently reconstructed CNFs; CaDiCaL 1.7.3 returned bounded UNKNOWN telemetry; drat-trim/lrat-check hooks were present but no UNSAT leaf arose; SHA-256 bound artifacts; the browser checked the maintained LJCR status and Krug's primary arXiv record.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1236.1s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260811-143826-283807

No human review recorded.