Gate degree-and-pair-preserving trade search by first constructing exact-pair 54-block seeds for four canonical weighted-degree-two cycle skeletons, then prepare an exhaustive common-core lifted-Pasch census.

degree-and-pair-preserving trade search

Solve sparse exact pair-multiplicity systems to enter a valid target fibre, then enumerate pair-preserving lifted-Pasch exchanges and measure uncovered-triple defect.

Hypothesis: Each of four fixed canonical weighted-degree-two pair-excess skeletons yields two independently checked exact-pair 54-block seeds under the bounded initializer, and at least one seed has a nonidentity common-core lifted-Pasch move.

Test: Solve the 105 by 3003 binary pair-incidence system for partitions [15], [13,2], [5,5,5], and [3,3,3,3,3] under eight-second per-seed limits; independently verify any model before enumerating lifted-Pasch moves. As a materially different control, solve a proof-capable balanced-totalizer CNF for [15] under a matched ten-second SAT limit.

The result is progress only as fail-closed infrastructure and route diagnosis. The artifacts establish that the intended target systems were encoded reproducibly, but UNKNOWN statuses provide no mathematical elimination. Holding the trade route until a checked seed exists prevents an invalid mobility inference.

• The four recorded canonical excess vectors each have total weight 15 and weighted degree 2 at every vertex.
• The deterministic [15] exact-pair CNF has 109998 variables, 549135 clauses, and SHA-256 a62e9c930313ccdd3c56788173a06c36f8df6a4aecfaacec1edaac663f4e7377.
• All four eight-second HiGHS runs and the ten-second CaDiCaL run returned UNKNOWN; none produced a seed, covering witness, or exclusion.
• The exact-cardinality emitter passed 516 exhaustive boundary controls through width six.

• python3 /root/proof-factory/skills/computational-researcher/scripts/run_experiment.py ... exact_pair_seed_gate_v1.py: four UNKNOWN statuses
• cadical -q -t 10 --seed=0 artifacts/exact-pair-seed-gate-20260809-v1/seed-15.cnf: c UNKNOWN
• python3 checkers/check_exact_pair_seed_gate_v1.py artifacts/exact-pair-seed-gate-20260809-v1/result.json: four structural rows accepted, zero seeds
• python3 checkers/check_exact_pair_seed_gate_v1.py ... --mutate-first-excess --expect-invalid: mutation rejected
• python3 checkers/test_exact_pair_seed_cnf_totalizer_v1.py: 516 controls accepted

• .proof-experiments/20260809-060305-80be65: four first-seed MILPs returned UNKNOWN after approximately eight seconds each
• .proof-experiments/20260809-060833-288b83: generated deterministic 109998-variable, 549135-clause [15] CNF
• .proof-experiments/20260809-060848-9283b8: CaDiCaL returned UNKNOWN at ten seconds
• .proof-experiments/20260809-060955-7a807d: independent checker accepted all four target specifications and recorded zero seeds
• .proof-experiments/20260809-060955-f158c2: checker rejected a one-unit skeleton mutation
• .proof-experiments/20260809-061107-57af82: 516 exhaustive totalizer boundary controls passed

checkers/check_exact_pair_seed_gate_v1.py independently reconstructs cycle skeletons, pair targets, degree vectors, triple defects, and Pasch mates. Because no seed was found, only target-system structure and UNKNOWN recording were exercised. checkers/test_exact_pair_seed_cnf_totalizer_v1.py independently tested the cardinality kernel with CaDiCaL on 516 assignments.

not_requested

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

Original model outcome

progress

Public classification

progress

• Clique-decomposition viewpoint -> pair-only target fibres should be treated as multigraph K5 decompositions before triple optimization -> bounded MILP and SAT initializers both returned UNKNOWN, so the transfer remains operationally unconfirmed.
• Design-trade theory -> adjoining a common pair to a Pasch trade yields a 5-uniform pair-preserving move -> the construction and independent census were implemented, but no seed existed on which to measure mobility.

• The four fixed cycle-partition skeletons used by the initializer have total excess 15 and weighted degree 2 at every point.
  Independent checker experiment 20260809-060955-7a807d and rejected mutation 20260809-060955-f158c2. · Partitions [15], [13,2], [5,5,5], and [3,3,3,3,3] in their recorded canonical labelings. · proved
• The generated [15] pair-only CNF contains 109998 variables and 549135 clauses and regenerates with SHA-256 a62e9c930313ccdd3c56788173a06c36f8df6a4aecfaacec1edaac663f4e7377.
  seed-15-cnf-manifest.json, generation experiment 20260809-060833-288b83, and byte-identical regeneration. · The exact recorded generator, Python version, block order, and [15] target. · computed
• No bounded initializer run produced an exact-pair seed.
  result.json records four UNKNOWN MILPs; CaDiCaL stdout records UNKNOWN. · The recorded four eight-second HiGHS runs and one ten-second CaDiCaL run only. · computed

• Begin degree-and-pair-preserving trade comparisons from an unchecked or non-target-fibre family.
  The current trade-search protocol. · Such moves preserve the wrong pair vector and cannot establish performance within a required 54-cover target fibre. · The seed-before-mobility protocol and independently reconstructed exact pair targets. · Supply at least one independently checked 54-block seed satisfying all 105 target equations.
• Interpret the bounded MILP or SAT timeouts as fibre exclusions.
  All four MILP systems and the [15] CNF. · Every solver status was UNKNOWN and no complete UNSAT proof exists. · result.json and .proof-experiments/20260809-060848-9283b8/stdout.txt. · A checked model or independently replayed complete UNSAT certificate for the exact instance.
• Increase the same unsymmetrized initializer cutoff without a mechanism change.
  The current sparse MILP and balanced-totalizer [15] CNF. · Larger arbitrary cutoffs have low decision value after all short controls returned UNKNOWN. · Matched bounded experiment packet. · Measured D15 symmetry, propagation, warm-start, or decomposition improvement.

• D15 full-state lex leaders for the [15] seed fibre.
  The target skeleton has a proved 30-element stabilizer, and full-state canonicalization is orbit-safe when independently reconstructed. · Generate a D15-lex CNF and compare it with the base CNF under identical ten-second CaDiCaL settings. · high · open
• Hybrid defect minimization plus Hamming-radius exact repair.
  A constructive heuristic can supply focused neighborhoods while the exact pair CNF provides a fail-closed repair test. · Predeclare a deterministic local-search budget, retain hash-bound best states, and test radius-two and radius-three exact repairs under equal evaluation budgets. · normal · open
• Coverage-aware type-4 signature refinement.
  This route remains materially distinct and can proceed without an exact-pair constructive seed. · Derive one literal pair-identity or triple-coverage signature and measure rejection on the 395 independently witnessed survivors. · normal · open

Objective: Determine whether safe D15 symmetry breaking makes the [15] exact-pair seed initializer materially easier.

First action: Adapt the full-primary-vector lex-leader emitter to the 30 D15 automorphisms and independently reconstruct the induced permutation of all 3003 block variables.

Stop condition: Stop or redirect if semantic controls fail, if the quotient is not orbit-safe, or if matched solver telemetry shows no material improvement and no seed.

• Adapt the previously validated full-primary-vector lex-leader construction to all 30 automorphisms of the canonical 15-cycle.
• Independently reconstruct the D15 block-variable action and test lex-leader orbit safety.
• Run the base and D15-lex CNFs under the same ten-second CaDiCaL seed and compare conflicts, decisions, propagations, and status.
• Decode and independently check any seed before running the saved lifted-Pasch census.
• If matched telemetry does not materially improve, redirect without increasing the cutoff.

• 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 served as principal investigator and independently designed, implemented, executed, audited, and interpreted the epoch. GPT-5.6 Terra delegates supplied bounded advisory prerequisite and control memos; their memo hashes and the exact accepted leads were promoted to sources/terra-exact-pair-seed-gate-20260809.json, and model agreement was not treated as validation. Deterministic Python 3.12.3, SciPy 1.11.4 with bundled HiGHS, Z3 4.13.0 for a bounded exploratory calibration not used as evidence, CaDiCaL 1.7.3, NumPy, and custom exact checkers were used. No CAS, proof assistant, cloud lab, or external publication action was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1505.7s

Review state

not a result claim

Attempt ID

covering-c1553-20260809-061756-422bbb

No human review recorded.