Compile the exact H6 threshold into each feasible minimum-intersection owner branch r=0,1,2, run cold CPU-pinned CaDiCaL preprocessing, and independently reconstruct formulas, ownership coverage, simplified outputs, and gate arithmetic.

incidence-matrix SAT with minimum-intersection owner decomposition

Exact degree 12 removes owner branches r>=3; canonical owner fixing, lower-intersection bans, residual-column lex ordering, and the threshold q(F)>=6 create three disjoint proof-oriented H6 branches whose active dimensions are measured before search.

Hypothesis: At least one of the three exhaustive feasible owner branches H6∧owner-r, r in {0,1,2}, reduces both active variables and active clauses by at least 5% versus H6 after one cold CaDiCaL 1.7.3 preprocessing round.

Test: Materialize all three owned H6 CNFs, run CaDiCaL 1.7.3 with -P1 -c 0 on one pinned CPU, and independently compare distinct used variables and clauses in the simplified DIMACS files against the H6 control.

The result is reproducible and independently checked at the exact claimed scope: formula construction, exhaustive owner coverage, preprocessing output, and gate arithmetic. It supports one further bounded calibration but supplies no satisfiability evidence.

• Every hypothetical simple 30-block cover, after fixing F, belongs to one of the minimum-intersection owner families r=0,1,2.
• The materialized owner-H6 r=0,1,2 formulas exactly combine their retained owner incidence formulas, correct lower-intersection bans, and the threshold sum of 450 internal pair-support variables at least 66.
• Under the recorded CaDiCaL 1.7.3 preprocessing protocol, r=1 and r=2 each reduce both active dimensions by at least 5% versus H6; r=2 is the deterministic best branch.
• No covering-number bound changed.

• python3 scripts/owner_h6_preprocess_v1.py --out-dir artifacts/epoch57-20260810/owner-h6-preprocess-v1/run
• python3 checkers/check_owner_h6_preprocess_v1.py --manifest artifacts/epoch57-20260810/owner-h6-preprocess-v1/run/preprocess-manifest.json --receipt artifacts/epoch57-20260810/owner-h6-preprocess-v1/independent-check.json
• sha256sum -c artifacts/epoch57-20260810/owner-h6-preprocess-v1/SHA256SUMS: all entries OK
• Independent scope: 5004 block orbits, 278256 owner profiles, 192 ban truth cases, threshold counts 65/66/67, four simplified formulas, and two mutations.

• .proof-experiments/20260810-153421-e837e7: producer completed in 8.314 seconds; r=1 and r=2 passed the two-dimension gate and r=2 was selected.
• .proof-experiments/20260810-153453-0f88fe: independent checker completed in 4.991 seconds and returned PASS.

checkers/check_owner_h6_preprocess_v1.py uses a separately implemented totalizer with semantic meanings, explicit stabilizer maps, bar-position profile enumeration, and independent DIMACS/log parsing.

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

• Certified C(12,6,4) forced-degree/orbit decomposition -> predict that exact pinning plus an owned structural split will shrink proof formulas -> r=1 and r=2 passed the preprocessing gate, but no terminal proof was attempted.
• Canonical augmentation in graph enumeration -> predict that exactly-one ownership must precede leaf solving -> exhaustive block and profile audits confirmed the r=0,1,2 partition under exact degree 12.

• A minimum-intersection owner r>=3 is impossible in a hypothetical 30-block cover.
  Exact degree 12 gives sum of incidences on F equal to 72, while r>=3 would give at least 6+29*3=93. · Simple 30-block covers after fixing F. · proved
• The three materialized owner-H6 formulas have 36314 variables and respectively 217291, 217319, and 217459 clauses before preprocessing.
  Independent clause reconstruction of the pinned owner sources, owner bans, and 3152-variable/60899-clause threshold suffix. · The immutable r=0,1,2 CNFs generated in epoch 57. · computed
• The selected r=2 formula preprocesses to 20695 used variables and 138806 clauses versus H6 at 22242 and 148192.
  Raw CaDiCaL logs and simplified DIMACS files independently parsed with matching hashes and counts. · CaDiCaL 1.7.3, one cold -P1 -c 0 round, recorded CPU and host. · computed

• Owned minimum-intersection branches r=3,4,5 can contain a 30-block cover.
  All simple 30-block covers conditional on the established exact degree-12 lemma. · Their minimum contribution to incidences on F exceeds 72. · 6+29*3=93>72, with exhaustive owner-profile audit. · A valid counterexample to exact degree 12 or to the incidence sum; neither is presently possible under the stated 30-block hypothesis.
• Use unchanged owned H6 r=0 as the next preprocessing-selected proof leaf.
  The recorded CaDiCaL 1.7.3 preprocessing protocol. · Its clause reduction was 4.8248%, below the frozen 5% gate. · owner-h6-r0.pre.log and independently parsed owner-h6-r0.pre.cnf. · A materially different encoding, terminal solver evidence, or at least 5% reduction in both dimensions under a new predeclared matched test.
• Use the six nominal second-block branches as a disjoint exhaustive proof partition.
  Fixed-first incidence search. · Containing an r-type block is overlapping; exact ownership is by the unique minimum r, and r>=3 is infeasible. · 278256-profile owner audit and explicit overlap controls retained from the owner frontier. · A separately proved exactly-once ownership construction with full union checking.

• Certificate-capped selected owner-H6 r=2 calibration
  It passed the static gate and is the cheapest test of whether the reduction changes proof-producing behavior. · Fresh replay controls followed by one seed-0 five-second CaDiCaL/LRAT run with 20-second wall and 4 MiB proof caps. · high · open
• Compressed E5 equality branch
  E5 remains the complementary global half, but its duplicated-counter encoding regressed; inheriting existing pair-totalizer outputs may repair it. · Reconstruct the threshold-five output map and require projected size at most 1.35 times the corresponding unrestricted base before solving. · normal · open
• Pair-excess-skeleton decomposition
  Every putative cover induces a loopless 4-regular excess multigraph, fixing all 105 pair multiplicities and offering a materially different outer split. · Compile the circulant and 3K5 skeleton controls and compare replay-compatible preprocessing against the direct-block pair-lower-bound model. · normal · open

Objective: Determine whether selected owner-H6 r=2 produces certificate-compatible terminal or materially improved proof behavior.

First action: Verify SHA-256 9433c83d98713fde1a76ef73e1f2c38fc8253f6daf26e9411f8100f77787e63d for owner-h6-r2.cnf and run fresh dual-replayer positive/truncation controls.

Stop condition: Stop after one five-second leaf or immediately on hash/control/replay mismatch, external wall over 20 seconds, or LRAT prefix over 4194304 bytes.

• Freshly build lrat-check and CakeLPR and require a retained complete LRAT positive control plus final-line truncation rejection.
• Run exactly one seed-0, five-second proof-producing CaDiCaL calibration on owner-h6-r2.cnf with a 20-second external wall cap and 4 MiB LRAT cap.
• Validate SAT directly in Python and C; accept UNSAT only after dual replay; require explicit dual rejection for UNKNOWN.
• Stop after the one leaf and rescore r=1, compressed E5, and pair-excess-skeleton routes.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://arxiv.org/abs/math/9502238 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol was principal investigator and designed, implemented, executed, and reviewed the epoch. GPT-5.6 Terra experiment-verification and challenger-prior-art delegates supplied advisory reconnaissance; their advice was audited and was not counted as evidence or independent validation. Python 3.12.3 generated CNF, enumerated finite ownership data, and ran the separate checker. CaDiCaL 1.7.3 performed preprocessing only. The reproducibility harness recorded commands, hashes, limits, logs, and memory. Web search checked the maintained-source context and primary literature. No SAT solve, LRAT proof generation, CAS, proof assistant, PB solver, cloud lab, external proof service, or human validator produced terminal evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1141.5s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260810-154328-3b6175

No human review recorded.