Constructive C3-invariant block-orbit CNF split into the four possible fixed/length-three orbit-count cases.

constructive cyclic-orbit SAT

Restrict to invariance under five disjoint 3-cycles, select whole block orbits, impose orbit coverage and exact degree-12 equations, and directly validate any expanded SAT model.

Hypothesis: At least one of the four C3-invariant orbit-count cases yields a directly checked 30-block cover within 20 seconds of seed-0 CaDiCaL search.

Test: Independently reconstruct the orbit quotient and then run four fresh 20-second CaDiCaL cases, accepting only a model that expands to 30 distinct blocks covering all 455 triples.

The only terminal positive signal was a directly checked SAT model, and none was emitted. UNKNOWN logs provide no negative mathematical conclusion. The independently validated orbit model is reusable infrastructure but does not meet the field-progress gate.

• The specified order-three action partitions the 5005 blocks into 10 fixed and 1665 length-three orbits.
• It partitions the 455 triples into 5 fixed and 150 length-three orbits.
• The 155 coverage rows have arity histogram 5x76, 60x211, and 90x219.
• All four 20-second searches returned UNKNOWN; the range remains 30 <= C(15,6,3) <= 31.

• python3 scripts/c3_orbit_cnf_discriminator_v1.py --out-dir artifacts/epoch82-20260811/c3-orbit-cnf-v1 --solve-seconds 20 --solver /usr/bin/cadical
• python3 checkers/check_c3_orbit_cnf_discriminator_v1.py --producer-receipt artifacts/epoch82-20260811/c3-orbit-cnf-v1/producer-receipt.json --out artifacts/epoch82-20260811/c3-orbit-cnf-v1/independent-final-check.json
• python3 checkers/check_c3_bounded_run_v1.py --receipt artifacts/epoch82-20260811/c3-orbit-cnf-v1/producer-receipt.json --out artifacts/epoch82-20260811/c3-orbit-cnf-v1/independent-run-audit.json
• Hash-manifest replay passed for 24 immutable files.

• .proof-experiments/20260811-093730-985a65: producer preflight generated four hash-bound CNFs in 6.151 seconds.
• .proof-experiments/20260811-093743-5d1318: independent orbit and primary-clause reconstruction passed.
• .proof-experiments/20260811-093824-890401: four 20-second searches all returned UNKNOWN.
• .proof-experiments/20260811-094007-dceb02: final independent semantic audit passed with no witness or exclusion.
• .proof-experiments/20260811-094125-7d4110: separate raw-log/status audit passed.

checkers/check_c3_orbit_cnf_discriminator_v1.py independently reconstructs set orbits, coverage records and primary clauses; checkers/check_c3_bounded_run_v1.py separately hashes and reparses raw logs and model files.

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

• Cyclic covering search -> quotient whole block and triple orbits under an order-three action -> the predicted 1675/155 exact quotient was observed, but no witness appeared within the bounded search.

• The specified C3 action has 1675 block orbits with length histogram 10 fixed and 1665 length-three.
  Independent set enumerations and orbit-manifest hash 27e5e888bedb913ae117e935ac3f1dc04aedf5f2d96955b416470baff27c778f. · All 6-subsets of the labelled 15-point set under the declared action. · computed
• The same action has 155 triple orbits with length histogram 5 fixed and 150 length-three.
  Independent set enumerations and independent-final-check.json. · All 3-subsets of the labelled 15-point set under the declared action. · computed
• A C3-invariant 30-block family must use one of four orbit-count profiles.
  Orbit-stabilizer lengths and the exact integer equation f+3l=30 with 0<=f<=10. · The declared C3-invariant family. · proved
• All four bounded runs returned UNKNOWN.
  Four raw CaDiCaL logs, producer receipt, and independent-run-audit.json. · CaDiCaL 1.7.3, seed 0, -P0, 20 seconds per retained formula. · computed

• Scale the unchanged sequential-counter C3 encoding solely by increasing the cutoff.
  The four retained formulas and current propagation mechanism. · Every bounded arm remained UNKNOWN, and a larger arbitrary cutoff would not itself be a contribution. · 42400 aggregate conflicts with no model or proof. · A matched materially smaller encoding, at least fivefold measured improvement, a proof-producing restricted-exclusion plan, or new structural justification for C3 invariance.
• Rerun the unfiltered canonical root-link catalogue suggested by reconnaissance.
  The epoch-19 canonical-parent construction without a new bulk completion filter. · Epoch 19 already independently validated a 10001-node cap breach in the first degree type. · artifacts/epoch19-20260809/root_link_canonical_primary_receipt.json and its checker receipt. · A sound completion filter or decomposition with a measured pilot projecting at least tenfold certified subtree elimination.

• Proof-producing completion filtering of recorded depth-four root-link nodes.
  It can eliminate whole canonical subtrees and directly addresses the prior catalogue cap breach. · Select a deterministic stratified sample from the 2258 depth-four nodes, compile exact completion CNFs, and require dual-replayed UNSAT proof logs with a tenfold projection gate. · high · open
• Compact alternative encoding of the four C3 cases.
  The orbit quotient is validated, but unary counters dominate the formula size. · Compile matched native MILP or BDD cases and compare completion or propagation under identical 20-second budgets. · low · open

Objective: Determine whether exact completion proofs can bulk-eliminate existing canonical root-link depth-four subtrees.

First action: Read artifacts/epoch19-20260809/root_link_canonical_primary_receipt.json, deterministically sample its 2258 type-0 depth-four nodes, and predeclare completion-CNF/LRAT limits.

Stop condition: Redirect on reconstruction disagreement, proof replay failure, certificate-budget breach, absence of a sound subtree interpretation, or less than tenfold projected elimination.

• Read the epoch-19 canonical root-link receipt and select a deterministic stratified sample from its 2258 complete depth-four nodes.
• Predeclare an exact completion-CNF and LRAT budget with independent reconstruction and dual replay.
• Continue only if certified dead subtrees project at least a tenfold frontier reduction.
• Hold the current C3 encoding unless a matched compact alternative improves the measured search signal by at least fivefold.

• 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/c-12-6-3.pdf ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol served as principal investigator. Two GPT-5.6 Terra delegates supplied advisory route and verification memos; Sol independently reimplemented every relied-on computation, and model agreement was not validation. CPython 3.12.3 generated and checked exact set orbits and DIMACS. CaDiCaL 1.7.3 performed four seed-0 bounded searches. The computational-researcher harness captured commands, limits, logs, hashes, platform and memory. Web search checked the maintained source and searched for a superseding result. No CAS, proof assistant, cloud lab, external proof service or human validator produced terminal evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1081.2s

Review state

not a result claim

Attempt ID

covering-c1563-20260811-094646-4cc0af

No human review recorded.