Exact second-block stabilizer quotient and matched SAT telemetry for the fixed size-1 rooted [3,2^6] leaf.

canonical one-unit cube decomposition

Quotient one additional selected block by the root-and-skeleton stabilizer, then test representative unit cubes against the shared exact CNF.

Hypothesis: The 3002 residual block choices quotient to at most 32 exhaustive representative cubes, and at least one cube decides or reduces matched CaDiCaL decisions by at least 20 percent at 2000 conflicts.

Test: Independently reconstruct the exact orbit union, then compare all representative positive-unit cubes with the unassumed CNF under identical solver settings.

The exact orbit census is a valid local structural reduction with a separate checker. The solver observations are reproducible telemetry only; uniform LIMIT statuses support no covering or exclusion claim.

• Under the fixed leaf's root-and-skeleton stabilizer, the 3002 residual five-subsets form exactly 31 orbits with sizes summing to 3002.
• The 31 representative positive-unit branches form an overlapping exhaustive cover of the fixed size-1 leaf.
• At seed 0 and nominal 2000 conflicts, all 31 cubes returned LIMIT; orbit 27 reproducibly used 4057 decisions versus 8295 for the baseline.

• python3 scripts/skeleton_326_second_block_orbits_v1.py --output artifacts/skeleton-326-second-block-cubes-20260810/orbits.json
• python3 checkers/check_skeleton_326_second_block_orbits_v1.py --input artifacts/skeleton-326-second-block-cubes-20260810/orbits.json --output artifacts/skeleton-326-second-block-cubes-20260810/independent-check.json
• Two executions of scripts/pilot_skeleton_326_second_block_cubes_v1.py with CaDiCaL 1.7.3, seed 0, and 2000 conflicts.
• Independent verification of all 31 augmented formula hashes and deterministic telemetry projections.
• Hash manifest c7c2c2f5509f169d32084dc2fd37b08620675b36af10a28ff781284e9686ffae checked with zero mismatches.

• .proof-experiments/20260810-170805-609478: producer found 31 orbits totaling 3002 blocks.
• .proof-experiments/20260810-170849-ba8f2f: independent orbit checker passed all checks and five mutations.
• .proof-experiments/20260810-170904-7e3514: all 31 cubes returned LIMIT; best cube used 4057 decisions.
• .proof-experiments/20260810-171112-fc273e: deterministic replay reproduced semantic counters.
• .proof-experiments/20260810-171325-d799c3: all formula-hash, replay, gate, and mutation checks passed.
• .proof-experiments/20260810-171723-080a68: all 14 manifest entries matched their recorded hashes.

The orbit checker uses feature fibres and a closed size formula rather than generator traversal. The telemetry checker independently rebuilds all unit-augmented DIMACS hashes and compares deterministic metric projections across a second solver execution.

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 orbit/SAT case analysis for C(12,6,4) -> predict a second stabilizer quotient can expose tractable leaves here -> observed an exact 31-cube cover and a strong best-cube propagation signal, but no solved cube.

• The local residual block universe has exactly 31 stabilizer orbits.
  Producer and independent feature-fibre checker agree, sizes sum to 3002, and five mutations fail. · Fixed root [0,1,12,13,14] in the canonical [3,2^6] leaf. · computed
• Orbit 27 reproducibly reduces 2000-conflict decision count by 51.0910186859554 percent relative to the unassumed baseline.
  Two deterministic CaDiCaL runs and independent semantic-projection comparison. · CaDiCaL 1.7.3, seed 0, this encoding and nominal conflict cap only. · computed

• Rerun the free-C3 constructive quotient without a new normalizer or encoding improvement.
  The fixed-point-free action (0 1 2)(3 4 5)(6 7 8)(9 10 11)(12 13 14). · Epoch 36 already generated and checked the same 1001-block-orbit quotient; matched 25000-conflict formulas remained unresolved. · records/attempts/epoch-0036-c3-symmetric-cover-20260809.json · An independently audited normalizer/cube reduction or materially better encoding followed by a solved certificate.
• Repeat the complete fixed-pair link gate.
  All 754 type-4 signature/e_45 targets under simultaneous coverage of all {4,5,z} triples. · Every target already survived an independently checked exact-capacity relaxation. · artifacts/type4-complete-pair-link-gate-20260809/result.json and independent-check.json · Add genuinely new labelled correlation rather than another isolated link relaxation.

• Proof-producing orbit-27 exact cube.
  It has the strongest reproducible propagation signal and satisfies the prior leaf's reopen condition. · Create the standalone unit CNF and run one 25000-conflict CaDiCaL test with a DRAT output path. · high · open
• Remaining 30 representative cubes.
  Together with orbit 27 they exhaust the fixed leaf, but their aggregate proof cost is unknown. · Only score or run them if orbit 27 decides or supplies a materially improved proof/cube method. · normal · open

Objective: Decide whether orbit 27 is a proof-tractable exact subleaf.

First action: Generate and independently hash-check the orbit-27 standalone CNF, then invoke /usr/bin/cadical --seed=0 -c 25000 with a DRAT output.

Stop condition: Stop on a directly checked SAT cover, fully replayed UNSAT proof, or LIMIT; LIMIT triggers redirect without a larger cutoff.

• Generate a persistent standalone CNF for orbit 27, representative [0,2,12,13,14], whose expected hash is 080610491ce6b8a91749596c3b904e10c5c9ad64d19a230d2642822f26dad7fd.
• Independently reconstruct that CNF and run CaDiCaL once at 25000 conflicts with a DRAT log.
• Accept SAT only after decoding and two direct 455-triple checks; accept UNSAT only after DRAT-to-LRAT conversion and LRAT replay.
• On LIMIT, redirect without increasing the cap or launching the other 30 cubes.

• 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 ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol principal selected, implemented, audited, ran, and interpreted the discriminator. GPT-5.6 Terra delegates supplied advisory memos; their free-C3 proposal was rejected as a stale epoch-36 route, and model agreement was not treated as validation. Python 3.12.3 exact enumeration, CaDiCaL 1.7.3, SHA-256, web search, and the computational-researcher experiment harness were used. No subagents, CAS, proof assistant, package installation, lab job, external write, or publication occurred.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1311.8s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260810-172012-38c9ac

No human review recorded.