Constructed, independently reconstructed, mutation-tested, and benchmarked two full-primary-vector D15 generator lex leaders for the [15] exact-pair seed CNF.

stabilizer-canonical exact-pair initialization

Enforce x <=lex r(x) and x <=lex s(x) on all moved 5-subset selection variables for a rotation and reflection generating D15, without identifying block-orbit variables or permuting totalizer auxiliaries.

Hypothesis: The checked D15 lex encoding returns SAT or UNSAT, or uses at least 20 percent fewer propagations than the base formula under matched ten-second CaDiCaL 1.7.3 seed-0 runs.

Test: Run base and D15 CNFs with identical CaDiCaL version, seed, ten-second internal limit, and memory bound; continue only on SAT, UNSAT, or at least 20 percent fewer D15 propagations.

The encoding is sound and reusable, but UNKNOWN is non-evidence and the predeclared performance gate failed. Scaling the same two gadgets would be an arbitrary cutoff extension. The quiet flag was omitted symmetrically only to expose telemetry; solver version, seed, formula, and internal time limit remained matched.

• The independently reconstructed D15 action has order 30 and 111 orbits on the 3003 block variables, with orbit-size histogram 3^1,15^20,30^90.
• The checked lex encoding adds exactly 5985 variables and 35908 clauses and preserves the base CNF as an exact clause prefix.
• Under the recorded matched protocol, base and D15 were UNKNOWN and D15 reduced propagations by 2.8191 percent, below the predeclared 20 percent gate.
• No mathematical case or covering family was eliminated.

• python3 scripts/exact_pair_d15_lex_v1.py --base-cnf artifacts/exact-pair-seed-gate-20260809-v1/seed-15.cnf ... produced D15 CNF SHA-256 c36bfe51d723f858fe98177ccff2b3cf4635af1fef39089361c4bca747a33051
• python3 checkers/check_exact_pair_d15_lex_v1.py ... returned valid=true and independently matched all 35908 clauses
• python3 checkers/test_exact_pair_d15_lex_mutations_v1.py ... rejected both mutations
• cadical -t 10 --seed=0 base.cnf and cadical -t 10 --seed=0 d15.cnf both returned UNKNOWN
• sha256sum -c artifacts/exact-pair-d15-lex-pilot-20260809-v1/manifest.sha256 passed every listed artifact

• .proof-experiments/20260809-064649-a196c2: generated the 115983-variable, 585043-clause D15 CNF
• .proof-experiments/20260809-064801-82d6dc: independently reconstructed D15, all lex clauses, and orbit-minimum extensions
• .proof-experiments/20260809-064816-587375: rejected wrong-map and hash-consistent clause mutations
• .proof-experiments/20260809-064836-9f068f: base run UNKNOWN with 22019822 propagations
• .proof-experiments/20260809-064858-2a4049: D15 run UNKNOWN with 21399056 propagations
• .proof-experiments/20260809-064920-386933: telemetry gate valid and threshold_met=false

checkers/check_exact_pair_d15_lex_v1.py independently reconstructs the group, block maps, target invariance, all 35908 clauses, orbit census, truth tables, and deterministic orbit-minimum extensions without importing the emitter.

not_requested

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

Original model outcome

progress

Public classification

progress

• SAT symmetry breaking -> full-vector D15 lex leaders should reduce duplicate search -> sound encoding reduced conflicts and decisions but missed the propagation gate, so the transfer is not worth scaling in this form.
• Certified link classification from C(12,6,4) -> enumerate both forced C(14,4,2) link profiles before global extension -> not yet tested; promoted as the next bounded discriminator.

• D15 has order 30 and 111 orbits on the 3003 five-subsets, with sizes 3^1,15^20,30^90.
  Independent checker and hash-bound manifest. · Canonical 15-cycle action. · computed
• The two lex gadgets contain 5985 auxiliary variables and 35908 clauses, each matching an independent reconstruction.
  independent-check.json and mutation-tests.json. · Recorded [15] pair-only D15 CNF. · computed
• The D15 matched run missed the 20 percent propagation gate.
  22019822 base versus 21399056 D15 propagations. · CaDiCaL 1.7.3, seed 0, matched ten-second internal limits on the recorded machine. · computed

• Scale the same two-generator D15 exact-pair initializer solely by increasing its time cutoff.
  Recorded balanced-totalizer CNF, rotation/reflection lex gadgets, CaDiCaL 1.7.3, and seed 0. · Both runs were UNKNOWN and the D15 encoding achieved only 2.8191 percent fewer propagations while using 3.0821 percent more RSS. · artifacts/exact-pair-d15-lex-pilot-20260809-v1/telemetry.json · A materially different propagation, decomposition, solver, warm-start, or canonical-cube mechanism with a successful bounded matched test.

• Certified canonical census of both forced point-link profiles.
  Every hypothetical 54-cover has a point-link of profile 7,5^13 or 6,6,5^12, and frontier size directly determines whether replay-certified blockers are plausible. · Compare two independent canonicalizers on the first complete checkpointed frontier segment. · high · open
• Hamming-radius exact repair from deterministic low-defect pair states.
  It is constructive and materially different from unrestricted fibre solving. · Run radius-two repair on a fixed predeclared state set. · normal · open
• Literal coverage refinement of the 395 type-4 signatures.
  It can proceed without an exact-pair seed and restores information absent from aggregate margins. · Measure one literal pair-identity or triple-coverage filter on all 395 survivors. · low · open

Objective: Determine whether both forced C(14,4,2) point-link orbit frontiers are manageable for a certified link/extension blocker program.

First action: Create the two-profile census protocol and implement independent canonicalizers under S13 and S2 x S12.

Stop condition: Canonicalizer disagreement, incomplete coverage accounting, or measured frontier growth too large for replayable blockers.

• Write a bounded protocol for canonical enumeration of the 7,5^13 and 6,6,5^12 point-link profiles.
• Implement two materially independent canonicalizers under S13 and S2 x S12.
• Measure a complete checkpointed frontier segment and compare representative hashes before any extension solving.
• Redirect if canonicalizers disagree or frontier growth is incompatible with replay-certified blockers.

• 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 ↗

GPT-5.6 Sol principal selected, implemented, executed, audited, and interpreted the epoch. GPT-5.6 Terra challenger-prior-art and experiment-verification delegates supplied advisory memos that Sol independently checked; model agreement was not validation. Deterministic Python 3.12.3, CaDiCaL 1.7.3, SHA-256, custom exact checkers, and bounded web source searches were used. No CAS, proof assistant, lab job, or UNSAT proof checker was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1105.9s

Review state

not a result claim

Attempt ID

covering-c1553-20260809-065659-da6272

No human review recorded.