Construct and independently audit the fixed-point-free C5 orbit quotient, then run a bounded sparse feasibility MILP for a C5-invariant 30-block cover.

C5-invariant orbit-level constructive search

Select six length-five block orbits using exact cycle-degree equations and 91 orbit-cover inequalities; directly expand and verify any solver witness.

Hypothesis: A fixed-point-free C5-invariant 30-block cover exists and a ten-second orbit-level feasibility MILP finds it.

Test: Solve the 1001-binary, 95-constraint orbit model for ten seconds and, on a hit, independently expand six selected orbits and check all 455 triples.

Complete orbit reconstruction and a materially different checker establish the reduction and model translation. The solver returned neither a feasible vector nor infeasibility evidence, so it supports only a neutral route calibration. The lack of telemetry makes longer generic-MILP execution low value.

• The specified C5 action partitions the 5005 blocks into exactly 1001 length-five orbits and the 455 triples into exactly 91 length-five orbits.
• The 1001 block orbits realize exactly 25 profiles; the independent checker verified every profile-to-point-degree translation.
• The orbit model has 1001 binary variables, 95 constraints, and 22996 nonzeros.
• Every one of the 333 long block orbits of an explicitly compatible regular Z15 action splits into exactly three selected C5 block orbits.
• The clean ten-second HiGHS run returned a time-limit status without a primal solution; this is not an exclusion.
• No 30-block cover was found and no lower bound was improved.

• Primary: python3 scripts/c5_invariant_milp_screen_v1.py --output artifacts/epoch28-20260809/c5_invariant_screen_result_v2.json --time-limit 10 under experiment 20260809-164548-4769d8.
• Checker: python3 checkers/check_c5_invariant_screen_v1.py --input artifacts/epoch28-20260809/c5_invariant_screen_result_v2.json --receipt artifacts/epoch28-20260809/c5_invariant_screen_checker_receipt_v2.json under experiment 20260809-164607-7b540e.
• Hash manifest audit checked every listed file with zero mismatches.
• Checker receipt records PASS, 1001 checked profile translations, witness_independently_validated=false, and mathematical_exclusion_validated=false.

• .proof-experiments/20260809-164548-4769d8: clean ten-second C5 MILP screen returned LIMIT_OR_OTHER with no witness.
• .proof-experiments/20260809-164607-7b540e: independent checker returned PASS and explicitly validated no mathematical exclusion.

checkers/check_c5_invariant_screen_v1.py uses destructive set partitioning rather than the primary canonical-representative construction. It independently reconstructs every orbit, coverage and incidence histograms, all 1001 profile-degree translations, and directly checks any future block list 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

• Regular-Z15 invariant search -> predict every compatible long orbit decomposes into three C5 orbits -> observed exactly three pieces for all 333 long orbits.
• Exact-pinnability incidence encoding -> predict orbit profiles can enforce degree 12 with three equations -> independently verified profile equality for every developed orbit.

• There are exactly 1001 block orbits and 91 triple orbits under the specified fixed-point-free C5 action, all of length five.
  Primary result v2 and independent checker receipt v2. · All 6-subsets and 3-subsets of the labelled 15-point set. · computed
• Each block-orbit profile coordinate equals the incidence degree contributed to every point in the corresponding point cycle.
  Independent checker tested all 1001 block orbits. · The specified C5 action. · computed
• All 333 long orbits of the explicit compatible regular Z15 action split into exactly three C5 block orbits.
  Primary result v2 compatible-Z15 control. · Long 6-subset orbits of that explicit compatible 15-cycle. · computed
• The ten-second sparse feasibility MILP produced no candidate witness.
  Experiment 20260809-164548-4769d8 and result v2. · One bounded SciPy 1.11.4/HiGHS run; not the full C5 family. · computed

• Scale the unchanged generic C5 feasibility MILP merely by increasing its time limit.
  The present 1001-variable SciPy/HiGHS encoding and zero-objective configuration. · The bounded run returned no incumbent, node count, gap, or other projection-quality telemetry. · artifacts/epoch28-20260809/c5_invariant_screen_result_v2.json · A material encoding change, useful incumbent/dual telemetry, or a matched pilot showing certificate-compatible throughput.
• Normalize the fixed seed-6 anchor into an r=5 incidence production leaf.
  The epoch-24 seed-6 U=2 anchor. · Its complete block-pair intersection histogram has maximum intersection four. · artifacts/epoch25-20260809/degree_u2_q3_checker_receipt.json · A demonstrated defect in the anchor binding or independently reproduced intersection histogram.

• C5 rarest-uncovered-triple bitset DFS
  It exploits the measured 167/209/218 incidence imbalance and six-orbit depth directly, unlike generic MILP. · Build the orbit database once, branch on the least-supported uncovered triple orbit, enforce degree residual bounds, and stop at a predeclared node cap. · high · open
• Corrected seed-6 r=4 proof leaf
  The proof pipeline is replayable, and twelve r=4 anchor pairs exist; a normalization preflight is sub-second. · Choose one r=4 pair, construct and independently verify its relabelling and lex-compatible 28-fixed/2-free placement. · high · open
• Proof-producing C5 SAT/profile decomposition
  If deterministic DFS suggests tractability, six-orbit profile cubes may admit complete DRAT/LRAT coverage more naturally than MILP infeasibility output. · Encode one profile cube in CNF and replay one bounded UNSAT leaf before designing a complete frontier. · normal · open

Objective: Determine whether the C5 family can be searched or certified efficiently, while correcting the global proof route to r=4.

First action: Implement a node-capped rarest-uncovered-triple C5 bitset DFS and independently enumerate its degree-profile partition.

Stop condition: Redirect if throughput cannot plausibly cover the profile frontier, completeness cannot be independently certified, or the r=4 normalization fails; stop immediately on a directly checked 30-cover.

• Implement a deterministic rarest-uncovered-triple bitset DFS over C5 block orbits, initially with a strict node cap and measured throughput.
• Independently enumerate exact feasible profile multisets and use them as a complete search partition, not as an assumed symmetry quotient.
• Design a hash-bound subtree or profile manifest before treating any exhaustive C5 miss as evidence.
• Normalize one of the seed-6 anchor's twelve r=4 block pairs and independently check lex-compatible placement before a 60-second LRAT leaf calibration.
• Do not repeat or lengthen the generic HiGHS feasibility run without a material encoding change.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol served as principal investigator, designed and audited the experiment, corrected the compatible-Z15 labeling, and interpreted the evidence. GPT-5.6 Terra delegates supplied advisory C5 reconnaissance and the r=5 challenge; model agreement was not treated as validation. Deterministic tools were CPython 3.12.3, SciPy 1.11.4 using HiGHS MILP, Python integer/set enumeration, SHA-256, jq, py_compile, GNU/Linux, and the Proof Factory run_experiment harness. Web search was used for source-status and prior-art triage. No CAS, proof assistant, SAT solver, external proof service, human validator, or cloud lab was used in this epoch.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

993.9s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260809-165025-6ed65d

No human review recorded.