Prove and independently audit a reflection-normalizer lex quotient of the fixed C6-invariant family, then compare its compact CNF against the locked baseline at 25000 CaDiCaL conflicts.

fixed-C6 reflection-normalizer lex symmetry breaking

The reflection rho conjugates the fixed generator g to g^-1, inducing an involution on 509 block-orbit variables; a lower-transposition lex leader selects one representative per rho-pair.

Hypothesis: The audited reflection-normalizer lex leader either decides the fixed C6-invariant 54-block family or reduces both CaDiCaL decisions and process time by at least 20 percent at 25000 conflicts.

Test: Reconstruct the normalizer independently, require all mutation and regeneration controls to pass, then run CaDiCaL 1.7.3 with seed 1553 and a 25000-conflict cap; accept telemetry advancement only at no more than 50883 decisions and 2.232 process seconds.

The algebraic identity, complete orbit action, exact Burnside count, clause suffix, mutation sensitivity, and regeneration are independently checkable. These support a local structural result. They do not support a cover, an UNSAT conclusion, or any claim about arbitrary 54-block covers.

• rho=(1 5)(2 4)(7 11)(8 10)(13 14) satisfies rho*g*rho^-1=g^-1 for the specified fixed C6 generator.
• The induced action on 509 block-orbit variables has 61 fixed points and 224 transpositions.
• Exactly 698045137232 weighted-size-54 C6 selections are rho-fixed, giving exactly 9330497387791280156 normalizer-orbit representatives.
• The audited reduced lex encoding adds 223 variables and 670 clauses.
• The candidate run was UNKNOWN at 25002 conflicts and did not meet the advancement gate.

• python3 checkers/check_c6_normalizer_lex_v1.py --base-manifest artifacts/c6-symmetric-cover-20260810/compact-manifest.json --base-cnf artifacts/c6-symmetric-cover-20260810/compact.cnf --manifest artifacts/c6-normalizer-lex-20260810/candidate-manifest.json --cnf artifacts/c6-normalizer-lex-20260810/candidate.cnf --output artifacts/c6-normalizer-lex-20260810/independent-check.json
• python3 checkers/test_c6_normalizer_lex_mutations_v1.py --checker checkers/check_c6_normalizer_lex_v1.py --base-manifest artifacts/c6-symmetric-cover-20260810/compact-manifest.json --base-cnf artifacts/c6-symmetric-cover-20260810/compact.cnf --manifest artifacts/c6-normalizer-lex-20260810/candidate-manifest.json --cnf artifacts/c6-normalizer-lex-20260810/candidate.cnf --output artifacts/c6-normalizer-lex-20260810/mutation-controls.json
• /usr/bin/cadical --seed=1553 -c 25000 artifacts/c6-normalizer-lex-20260810/candidate.cnf artifacts/c6-normalizer-lex-20260810/candidate-proof.drat
• Candidate CNF SHA-256 0db3adffe2ee922fbbd9eb1f47d229859db190bc79f1f2aaedafc65f2bca1401.
• Result SHA-256 35202187f8a6f1a62417f55c868df913fb40b26172f1eddb726815f833269b16.

• .proof-experiments/20260810-223342-921554: generated the 5910-variable, 47785-clause candidate CNF.
• .proof-experiments/20260810-223359-dd7be8: independent orbit/action/count/encoding checker returned valid=true.
• .proof-experiments/20260810-223407-982438: unmodified input passed and all five mutations were rejected.
• .proof-experiments/20260810-223421-1516c4: CaDiCaL returned UNKNOWN at 25002 conflicts, 51841 decisions, and 2.34 process seconds.
• .proof-experiments/20260810-223545-9ec536: CNF and manifest regenerated byte-identically.
• .proof-experiments/20260810-223554-c6ee12: summary confirmed both advancement gates were false.

checkers/check_c6_normalizer_lex_v1.py reconstructs the point permutations, all 3003 blocks, all 509 C6 block orbits, the induced reflection action, fixed-point count, and exact lex suffix without importing producer tables. It can also directly check any SAT model against all 455 triples.

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

• Group-action involutions -> predict that only lower transposition endpoints can be first lex differences -> exhaustive toy checks and the exact 509-variable reconstruction confirmed a 224-comparison encoding.
• Burnside counting -> predict an almost twofold reduction when few selections are reflection-fixed -> exactly 698045137232 fixed selections yielded factor 1.9999999251867175.
• Local normalizer quotient -> predict materially improved CDCL telemetry -> observed improvements of 18.4941 percent in decisions and 16.1290 percent in time, insufficient for the predeclared gate.

• rho normalizes the fixed C6 action.
  Direct permutation composition independently checked on all 15 points. · The specified permutations g and rho. · proved
• The induced action has 61 fixed variables and 224 transpositions.
  Independent reconstruction of all 509 block orbits and every reflected orbit image. · The fixed C6 block-orbit variable set. · computed
• There are exactly 9330497387791280156 reflection-normalizer orbits of weighted-size-54 C6 selections.
  Independent subset-sum fixed-point count plus Burnside identity. · Weighted-size-54 selections in the fixed C6 family, without imposing coverage. · computed
• The bounded candidate run remained UNKNOWN and failed both telemetry gates.
  Hash-bound CaDiCaL stdout and deterministic summary. · Candidate CNF 0db3adffe2ee922fbbd9eb1f47d229859db190bc79f1f2aaedafc65f2bca1401, CaDiCaL 1.7.3, seed 1553, nominal 25000-conflict cap. · computed

• Scale the same fixed-C6 reflection-normalizer monolithic CNF solely by raising the conflict cutoff.
  The recorded candidate encoding and solver protocol. · It remained UNKNOWN and missed both predeclared advancement thresholds. · artifacts/c6-normalizer-lex-20260810/result.json · A complete proof-producing cube partition or materially different normalizer/encoding that passes an independently audited advancement gate.
• Treat the bounded UNKNOWN run or its partial DRAT trace as an exclusion.
  The fixed C6 family and, a fortiori, the global covering problem. · Conflict-cap termination produced no complete UNSAT proof. · .proof-experiments/20260810-223421-1516c4/stdout.txt · A complete UNSAT result with byte-bound DRAT-to-LRAT conversion and independent replay.
• Rerun the complete fixed-pair-link relaxation as a new discriminator.
  The prior 395 signatures and 754 targets. · The stronger completed experiment already retained every target. · artifacts/type4-complete-pair-link-gate-20260809/result.json · Genuinely new labelled information beyond the complete fixed-pair link.

• Automorphism lex quotient for the four globally complete pair-normalized branches.
  This transfers the validated mechanism to a branch system covering every hypothetical 54-cover. · Reconstruct each stabilizer action and count its induced fixed and moved primary variables before producing CNF. · high · open
• Constructive exact-degree search using a materially different repair neighborhood.
  A direct 54-cover is the cheapest terminal certificate, while the saved defect-10 seed and radius-four exclusion provide a concrete boundary. · Design a bounded degree-preserving move family that provably includes symmetric-difference radius at least five and compare it against the saved seed without merely enlarging an arbitrary iteration cutoff. · normal · open

Objective: Measure whether the audited involution lex mechanism yields a material, globally complete quotient on the four pair-normalized branches.

First action: Reconstruct the four saved branch stabilizer generators and emit their induced primary-variable cycle structures without generating CNF.

Stop condition: Stop or redirect if any action does not preserve its branch, the branch union is not globally complete, or the quotient is too small to offset encoding and checker cost.

• Reconstruct the stabilizer generators and induced primary-variable actions for each of the four globally complete pair-normalized branches.
• Before generating CNF, independently verify branch preservation and compute exact fixed/moved/transposition counts.
• Continue only if the projected quotient materially exceeds its encoding and audit cost.
• Do not rerun the complete fixed-pair-link relaxation or scale the fixed-C6 monolithic CNF without satisfying their reopen conditions.

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

Codex acted as the Sol principal, designing and auditing the experiment. Two injected GPT-5.6 Terra delegate memos supplied advisory reconnaissance only; Sol independently reconstructed every relied-upon mathematical and computational claim and diverged from Terra's larger lex encoding. Deterministic tools used: Python 3.12.3, CaDiCaL 1.7.3, the project computational-researcher harness, jq, sha256sum, and Git read-only diagnostics. The web search tool was queried for current prior art but returned no additional exact-parameter source beyond the pre-acquired maintained records. No CAS, proof assistant, external publication, or lab job was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1044.4s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260810-224204-f71a36

No human review recorded.