Normalize a hypothetical 54-cover on a pair of multiplicity exactly five, classify its five common blocks into four canonical types, and probe all four extension CNFs.

multiplicity-five pair normalization

Pair-excess counting guarantees a multiplicity-five pair; its five projected triples covering 13 points fall into four point-isomorphism types, producing four globally complete SAT branches.

Hypothesis: Fixing one of the four canonical multiplicity-five common families would make at least one 54-cover extension branch decisive within 25,000 CaDiCaL conflicts.

Test: Generate the four complete canonical degree-18 CNFs, validate them on a relabelled known 55-cover, and run each live branch under the same 25,000-conflict cap.

The pair-excess identity guarantees the chosen normalization for every hypothetical 54-cover, while the independent orbit sum proves that the four types exhaust the local possibilities. Solver UNKNOWN and partial DRAT traces provide no exclusion evidence.

• Every hypothetical 54-cover can be relabelled into one of four canonical multiplicity-five pair branches.
• The four labelled common-family orbit sizes are 1,801,800; 8,108,100; 10,810,800; and 1,201,200.
• Their sum is the independent inclusion-exclusion count 21,921,900.
• All four live branches were UNKNOWN at 25,000 conflicts.

• python3 checkers/check_pair5_normalization_v1.py --audit-types
• The type-2 fixed 55-cover control was SAT and decoded byte-identically.
• Independent checking confirmed 55 distinct blocks, all 455 triples, exact degrees, and exactly the canonical type-2 common blocks.
• CaDiCaL 1.7.3 returned UNKNOWN on each of the four hash-bound live CNFs.

• .proof-experiments/20260809-022905-199d3e: four-type audit passed with exact orbit sum 21,921,900.
• .proof-experiments/20260809-022956-284fc0: fixed type-2 known-cover control was SAT.
• .proof-experiments/20260809-023110-21697e: type 1 UNKNOWN at 25,001 conflicts.
• .proof-experiments/20260809-023110-4305a4: type 2 UNKNOWN at 25,001 conflicts.
• .proof-experiments/20260809-023110-4f3c5f: type 3 UNKNOWN at 25,000 conflicts.
• .proof-experiments/20260809-023110-0dd9a8: type 4 UNKNOWN at 25,001 conflicts.

checkers/check_pair5_normalization_v1.py independently reconstructs incidence signatures, orbit sizes, the inclusion-exclusion total, point degrees, common-pair blocks, and all 455 triple obligations.

not_requested

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

Original model outcome

progress

Public classification

progress

• C(12,6,4) forced-link normalization -> pin a locally forced incidence object before SAT -> the guaranteed multiplicity-five pair yielded four globally complete C(15,5,3) branches, though the unsymmetrized pilot remained UNKNOWN.

• At least 90 pairs have multiplicity exactly five in every hypothetical 54-cover.
  Every pair multiplicity is at least five and the total excess is 15. · All 54-block C(15,5,3) covers. · proved
• The projected common family of a multiplicity-five pair has exactly four point-isomorphism types.
  Degree-sequence proof and independent incidence-signature checker. · Five distinct triples covering 13 points. · proved
• The four labelled orbit sizes sum to 21,921,900.
  artifacts/pair5-normalization-pilot-20260809/type-audit.json · Five-triple common families covering all 13 non-endpoints. · computed

• Treat any of the four capped CaDiCaL runs as an exclusion.
  The exact four CNFs at 25,000 conflicts. · Every run returned UNKNOWN and emitted only a partial DRAT trace. · The four saved experiment records report exit 0 and conflict-cap termination. · A complete UNSAT run with an independently replayed certificate bound to the exact CNF.
• Scale the same unsymmetrized encoding solely by increasing an arbitrary cutoff.
  The current four-branch totalizer encoding. · The pilot supplied no decisive status, and unused stabilizer groups of orders 3,456; 768; 576; and 5,184 offer a cheaper discriminator. · type-audit.json and live telemetry · Measured evidence that checked symmetry or a materially different encoding fails to improve the route.

• Common-family stabilizer lex leaders.
  All four branches retain large proved automorphism groups that the current CNFs ignore. · Add independently reconstructed lex leaders to type 4 and rerun at 25,000 conflicts. · high · open
• Couple each common-family type to pair-excess skeleton orbits.
  Exact pair targets may supply propagation absent from degree-only branches. · Count joint orbits of type-4 common families with weighted-degree-two pair-excess skeletons before generating any SAT leaves. · normal · open
• Literal outside-subset realization control.
  It remains a materially distinct route that restores subset identities inside one previously surviving aggregate profile. · Run the saved root-orbit-107 profile if the global pair-normalization symmetry test fails. · normal · open

Objective: Exploit the fixed common-family stabilizers without weakening the four-branch completeness guarantee.

First action: Enumerate stabilizer generators independently, encode lex leaders for type 4, and run the exact saved 25,000-conflict comparison.

Stop condition: Redirect if same-cap propagation and decisiveness do not materially improve; promote only after a checked 54-cover or complete replayed proofs for all four branches.

• Independently enumerate generators for the four common-family stabilizers.
• Add a sound lex-leader encoding to type 4 and compare with its saved 25,000-conflict baseline.
• Prepare an independently checked DRAT/LRAT replay path before any proof-scale run.
• Redirect to the saved outside-subset profile if symmetry gives no material same-cap improvement.

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

GPT-5.6 Sol principal independently audited the sources and Terra memos, selected the pair-normalization route, proved the reduction, implemented the deterministic generator/checker, and interpreted the evidence. GPT-5.6 Terra delegates supplied advisory challenger and outside-profile memos; model agreement was not treated as validation. Python 3.12.3 generated and checked artifacts; CaDiCaL 1.7.3 ran the CNFs; web search checked current status and prior-art leads. No live proof was replayed because every branch returned UNKNOWN.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1236.1s

Review state

not a result claim

Attempt ID

covering-c1553-20260809-024005-16ae80

No human review recorded.