Independently reconstruct the canonical type-4 common-family stabilizer, add sound generator lex leaders on the 2,717 primary block variables, and compare pointwise, full, and unsymmetrized CNFs at the identical 25,000-conflict protocol.

common-family stabilizer symmetry

Exact point-group closure generates primary-projection lex inequalities; matched deterministic SAT telemetry tests whether they improve the complete type-4 branch.

Hypothesis: At seed 0 and a fixed 25,000-conflict cap, checked type-4 stabilizer lex leaders will reach SAT/UNSAT or reduce propagations by at least 20% relative to the exact unsymmetrized baseline.

Test: Run the base, 5,184-element pointwise-stabilizer, and 10,368-element full-stabilizer CNFs sequentially with CaDiCaL 1.7.3 and compare hash-bound statuses, conflicts, decisions, and propagations.

The result is reproducible and useful as a route decision because the base clauses, group actions, lex gadgets, CNF hashes, solver protocol, and telemetry were checked independently. UNKNOWN supplies no mathematical exclusion, so the outcome is progress rather than candidate.

• The canonical type-4 common family has endpoint-pointwise stabilizer order 5,184 and full stabilizer order 10,368 after adjoining endpoint swap.
• These actions have respectively 59 and 41 orbits on the 2,717 free block variables.
• The recorded generator lex CNFs retain at least one primary assignment from every relevant stabilizer orbit.
• At the saved protocol, pointwise and full lex increased propagations by 96.0196% and 113.3717%, and both remained UNKNOWN.
• The maintained range remains 54 <= C(15,5,3) <= 55.

• sha256sum -c artifacts/type4-stabilizer-lex-pilot-20260809/manifest.sha256: every listed file OK
• Independent pointwise checker: group_order=5184, primary_variable_orbits=59, valid=true
• Independent full checker: group_order=10368, primary_variable_orbits=41, valid=true
• Matched telemetry checker: all statuses UNKNOWN, threshold_met=false, valid=true
• CaDiCaL commands used -c 25000 with seed 0 default on the three hash-bound CNFs

• .proof-experiments/20260809-031205-f848a3: generated pointwise CNF with order 5,184
• .proof-experiments/20260809-031153-4fd53d: generated full CNF with order 10,368
• .proof-experiments/20260809-031611-8dbf46: pointwise independent audit passed
• .proof-experiments/20260809-031611-1027d7: full independent audit passed
• .proof-experiments/20260809-031702-284868: base UNKNOWN with 22,085,371 propagations
• .proof-experiments/20260809-031722-d39b09: pointwise UNKNOWN with 43,291,657 propagations
• .proof-experiments/20260809-031748-53317d: full UNKNOWN with 47,123,935 propagations
• .proof-experiments/20260809-031956-13eac4: independent matched telemetry check passed

checkers/check_type4_stabilizer_lex_v1.py independently reconstructs the groups and checks the CNF semantics; checkers/check_type4_lex_telemetry_v1.py independently parses and compares solver logs.

not_requested

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

Original model outcome

progress

Public classification

progress

• Classical SAT symmetry breaking -> generator lex leaders should reduce redundant search -> on this totalizer encoding they increased propagation by 96–113%, falsifying the transfer in its raw sequential form.
• Sparse group-action computation -> packed supports should accelerate orbit controls -> audit time dropped from a timeout to 22–40 seconds while preserving exact results.

• The type-4 endpoint-pointwise stabilizer has order 5,184 and 59 free-block-variable orbits.
  type4-pointwise-independent-check.json, valid=true · Canonical type-4 common family · computed
• Adjoining endpoint swap gives group order 10,368 and 41 free-block-variable orbits.
  type4-full-independent-check.json, valid=true · Canonical type-4 common family with interchangeable endpoints · computed
• Both tested lex variants fail the saved continuation threshold.
  matched-telemetry-check.json, threshold_met=false and valid=true · CaDiCaL 1.7.3, seed 0, nominal 25,000-conflict protocol · computed

• Scale the recorded six- or seven-generator sequential lex type-4 encoding solely by increasing the conflict cutoff.
  The hash-bound pointwise and full CNFs under CaDiCaL 1.7.3 seed 0. · Both remained UNKNOWN and increased propagations by 96.0196% and 113.3717%. · artifacts/type4-stabilizer-lex-pilot-20260809/matched-telemetry-check.json · A materially different symmetry encoding with independent soundness validation and matched evidence of at least 20% fewer propagations or a decisive status.

• Signature-first type-4 residual-block and pair-excess filtering.
  It can eliminate whole invariant classes without paying the propagation cost of long sequential lex gadgets. · Enumerate the complete stabilizer-quotiented signature frontier and independently check skeleton compatibility. · high · open
• Literal outside-subset realization for the saved root-orbit-107 profile.
  It restores subset identities lost by exhausted aggregate projections and is materially distinct from raw symmetry. · Encode and independently decode the saved minimum-survivor profile. · normal · open

Objective: Find a complete, small type-4 signature frontier that removes whole residual classes before SAT.

First action: Specify the exact residual-block intersection/pair-excess signature and write a deterministic enumerator plus independent skeleton-witness checker.

Stop condition: Stop or redirect if the signature map is incomplete, yields no strict frontier reduction, or fails to improve matched propagation.

• Define a finite residual-block intersection/pair-excess signature for type 4.
• Enumerate signatures modulo the checked full stabilizer and enforce exact degree, block-count, and pair-excess totals.
• Independently verify that every retained signature has a weighted-degree-two skeleton witness.
• Run matched SAT only if the complete signature frontier strictly shrinks or supplies stronger propagation.
• Redirect to the saved literal outside-subset realization profile if the signature discriminator fails.

• 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://cdn.aaai.org/KR/1996/KR96-012.pdf ↗

GPT-5.6 Sol principal selected, reconstructed, implemented, audited, and interpreted the route. GPT-5.6 Terra delegates supplied bounded advisory leads; their agreement was not treated as validation, their ephemeral files were not claimed as evidence, and discrepancies in their orbit/encoding counts were corrected. Deterministic Python 3.12.3 generated and independently checked the artifacts. CaDiCaL 1.7.3 performed the capped SAT probes. No DRAT/LRAT checker was used because every live run remained UNKNOWN.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1470.2s

Review state

not a result claim

Attempt ID

covering-c1553-20260809-032621-79584e

No human review recorded.