Generated and audited six canonical second-block incidence CNFs, benchmarked them against equal-budget unconditioned controls, then redirected to a root-link catalogue after proving a residual-excess pruning lemma.

incidence-orbit cube SAT with root-link structural redirect

Fix one canonical second block for each intersection r=0,...,5, lex-sort only columns 2 through 29, compare six branches against matched controls, and use the resulting gate decision to select the next route.

Hypothesis: The six audited second-block incidence branches produce at least twice the aggregate seed-4 conflict and decision counts of six matched unconditioned controls under equal 30-second budgets, with no larger median RSS.

Test: Twelve fresh CPU-pinned CaDiCaL 1.7.3 runs at seed 4 and five seconds each, paired by intersection type with alternating branch/control order.

The receipt validates the formulas and matched comparison, while the observed ratios fail the frozen continuation rule. The root-link inequality follows pointwise from nonnegative residual pair multiplicities and the established 4-regular pair-excess identity.

• The six generated formulas cover normalized existence and each has 33162 variables, 156392 clauses, 30 fixed units, and 27 lex comparators on columns 2 through 29.
• Under the exact twelve-cell seed-4 protocol, aggregate branch/control ratios were 1.04462 conflicts, 0.98741 decisions, and 0.98528 propagations.
• Every hypothetical 30-cover satisfies sum_{z != x,y} max(0,ell_yz-4) <= 8-r_y for every root-link point y.

• incidence_orbit_receipt.json SHA-256 a1fd30cd275ef555ba05fdc71708a33cc2f7ebfbbb5e728f8ff0297b0f69c333
• run-manifest.json SHA-256 fffb8242642a2fb059d069a1a834187a38c6ff65f81dbf432628344ad039625c
• root_link_residual_budget_receipt.json SHA-256 5e98f63c04424632f1ec85b963056c1881e882c9d0388d8a0d8fc46299dba0aa
• All twelve CaDiCaL statuses were UNKNOWN; no witness or proof log exists.

• .proof-experiments/20260808-210442-2f4010: six generated branches and twelve matched solver cells completed; every status UNKNOWN.
• .proof-experiments/20260808-210602-11dec4: independent final checker passed and selected redirect_to_root_link_catalogue.
• .proof-experiments/20260808-210855-82fe1e: exact compressed DP found no residual-budget violation for link degrees 4 through 8.

checkers/check_incidence_orbit_pilot_v1.py independently reparses formulas and logs and rejects four malformed controls. checkers/check_root_link_residual_budget_v1.py uses a separate compressed arithmetic encoding for the new lemma.

not_requested

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

Original model outcome

progress

Public classification

progress

• C(12,6,4) certified extremal-link SAT architecture -> fixing a complete root link should reduce residual memberships to 252 -> catalogue size remains unmeasured and is the next discriminator.
• Incidence orbitope plus second-block stabilizer split -> predicted at least 2x aggregate solver counters -> observed 1.045 conflicts and 0.987 decisions, falsifying scale-up for the current workflow.
• Global 4-regular pair-excess identity -> predicts a local high-codegree budget in every root link -> proved and verified as sum max(0,ell-4)<=8-r.

• The six generated branch formulas form a complete normalized search cover with the stated fixed units and comparator range.
  Explicit stabilizer audit over 5004 blocks and exact DIMACS structural comparison. · Global existence after fixing 012345; branches may overlap. · computed
• The current six-cube workflow failed both frozen 2x aggregate throughput gates.
  Hash-bound raw logs and independently reproduced incidence_orbit_receipt.json. · CaDiCaL 1.7.3, seed 4, CPU 0, five seconds per cell. · computed
• Every root-link point satisfies sum max(0,ell_yz-4)<=8-r_y.
  Residual multiplicity proof and exact DP arithmetic audit. · Every root link of every hypothetical 30-block cover. · proved

• Scale the current six second-block incidence-cube DIMACS workflow from structural reduction alone.
  The six audited formulas and exact twelve-cell seed-4 protocol. · Both predeclared aggregate 2x gates failed. · artifacts/epoch9-20260808/incidence_orbit_receipt.json · A material encoding change, proof-valid shared-prefix reuse, or terminal solver evidence.
• Infer existence or nonexistence from the twelve solver cells.
  The global exact covering target. · Every status was UNKNOWN and no certificate exists. · Hash-bound run manifest and raw logs. · A directly validated 30-block cover or independently replayed exhaustive UNSAT proof set.

• Canonical root-link catalogue with residual-budget filtering.
  It is materially different from global incidence search, reduces residual memberships to 252 after fixing a link, and now has a sound cheap pruning rule. · Run baseline and filtered canonical augmentation for one degree type under a 10000-node cap with an independently checked frontier. · high · open
• Degree-preserving constructive local search.
  A 30-block witness immediately settles the target and supplies information independent of exclusion search. · Run matched short seeded degree-preserving and unconstrained searches using best uncovered-triple count. · normal · open

Objective: Measure the size and filterability of one canonical root-link degree-type frontier.

First action: Implement a deterministic canonical augmenter with incremental degree, pair-coverage, codegree, and residual-budget state, then run baseline and filtered variants under the same 10000-node cap.

Stop condition: Redirect if canonical coverage cannot be independently certified or if the residual-budget filter never fires and does not reduce the frontier.

• Implement a deterministic canonical augmenter for one forced 12-block root-link degree type.
• Maintain degrees, pair coverage, link codegrees, and the residual-excess budget incrementally.
• Compare baseline and budget-filtered enumeration under the same 10000-canonical-node cap.
• Write a separate checker for canonical coverage and the replayable frontier before any scale-up.

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

GPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra delegates supplied advisory experiment-verification and challenger memos; adopted claims were independently rederived and deterministically checked, and model agreement was not validation. Deterministic tools were Python 3.12.3, CaDiCaL 1.7.3, GNU time, taskset, SHA-256, and the computational-researcher experiment harness. No proof assistant or DRAT/LRAT checker was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1383.4s

Review state

not a result claim

Attempt ID

covering-c1563-20260808-211546-ab17f3

No human review recorded.