Literal outside-subset realization of the hash-bound mapping-1438 31-cell witness for the 15-cycle skeleton, root orbit 107 and profile 0.

literal outside-subset realization

Replace anonymous root-cell counts by Boolean variables for actual 5-subsets, enforce exact cell, point and pair counts plus complete triple coverage, and search the resulting native pseudo-Boolean instance.

Hypothesis: The frozen mapping-1438 31-cell witness can be realized by 53 distinct literal residual blocks satisfying the labelled 15-cycle pair targets and all triple-coverage constraints.

Test: Run the independently reconstructed 2772-primary native-PB instance with seed 0 to a predeclared 250000-conflict cap; accept only a directly checked 54-cover or a replayed proof-bound UNSAT result.

The exact input and its semantics are independently checkable, so the infrastructure result is durable. The lack of a model or replayable proof prevents any mathematical inference about feasibility or the global covering number.

• The exact frozen mapping-1438 instance contains 2772 primary variables and 572 independently reconstructed assertions.
• Zero-cell pruning safely omits exactly 230 residual block variables in this frozen subfamily.
• Z3 4.13.0 seed 0 returned UNKNOWN after 250001 conflicts; this excludes nothing.

• python3 scripts/outside_subset_profile_v1.py ... --max-conflicts 250000
• python3 checkers/check_outside_subset_profile_v1.py ...
• python3 checkers/check_outside_subset_regeneration_v1.py ...
• python3 checkers/test_outside_subset_profile_mutations_v1.py ...
• sha256sum -c artifacts/outside-subset-profile-20260809/manifest.sha256

• .proof-experiments/20260809-035520-3824e5: Z3 returned UNKNOWN at 250001 conflicts in 15.303068900946528 solve seconds.
• .proof-experiments/20260809-035556-0da66e: independent reconstruction accepted all 572 assertions and found no witness claim.
• .proof-experiments/20260809-035707-070175: selection and SMT2 regenerated byte-identically.
• .proof-experiments/20260809-035720-58c011: all four semantic mutations were rejected.

checkers/check_outside_subset_profile_v1.py independently enumerates blocks and rows without importing the producer, compares every SMT assertion, and directly checks any future witness. No witness was available in this epoch.

not_requested

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

Original model outcome

progress

Public classification

progress

None recorded.

• The frozen mapping-1438 vector has a reproducible 2772-primary literal-subset PB encoding with 572 assertions.
  independent-check.json valid=true and regeneration-check.json byte-identical=true · One frozen vector at partition [15], root orbit 107, profile 0. · computed
• The frozen cells imply residual degree 17 on each root point and residual multiplicity 4 on every root pair.
  The independent checker recomputed all 31 cell contributions. · The exact recorded cell vector. · computed
• The bounded native-PB run terminated UNKNOWN.
  artifacts/outside-subset-profile-20260809/result.json · Z3 4.13.0 seed 0, exact SMT2 hash, 250000 nominal conflict cap. · computed

• Treat the UNKNOWN result as exclusion of the frozen profile.
  Mapping 1438 and its recorded 31-cell vector. · No model or complete proof was emitted. · result.json status=unknown and witness absent · A directly checked SAT witness or independently replayed UNSAT proof for the exact instance.
• Scale the identical native-PB encoding solely by increasing its conflict cap.
  SMT2 SHA-256 71f9088b3f4d02f0811ddbcf3a81c194b0f1d8f9b73ac9140db00f7e192084c3. · A matched proof-capable CNF encoding offers more information than an arbitrary cutoff increase. · The predeclared native-PB pilot was UNKNOWN. · Matched evidence that the independently checked CNF cross-encoding is no better, plus a predeclared information-value justification.
• Rely on the Terra characterization that only root orbits 107 through 110 attain the minimum explicit integer-feasible profile count.
  The global mapping result. · Independent recounting found many additional tied rooted orbits. · Direct enumeration of status counts from artifacts/root-pair-excess-coupling-global-20260808/result.json · A corrected, precisely defined minimization property with an independent enumeration.

• Proof-capable totalizer CNF cross-encoding of mapping 1438.
  It changes solver representation, reuses checked incidence semantics and can emit a replayable proof. · Generate and independently compare a CNF for the exact 572 rows, then run a matched-cap CaDiCaL pilot. · high · open
• Coverage-aware signature invariant for the globally complete four-type normalization.
  Pair-target compatibility alone removed no class; a coverage-aware invariant is required for bulk elimination. · Derive one triple-coverage signature whose family-to-signature map can be checked independently before enumerating a full frontier. · normal · open
• Constructive local search respecting exact degree and pair-excess constraints.
  A 54-cover would settle the target and is much easier to validate than a global negative certificate. · Run a bounded deterministic swap-search pilot with exact uncovered-triple and degree/pair delta evaluation. · normal · open

Objective: Determine whether a proof-capable totalizer CNF materially changes the exact mapping-1438 literal-profile search.

First action: Implement scripts/outside_subset_profile_cnf_v1.py using the frozen selection and independently compare all 572 row incidences and targets before invoking CaDiCaL.

Stop condition: Semantic mismatch, unchecked UNSAT, or matched-cap UNKNOWN without a material propagation improvement ends or redirects the route.

• Generate a totalizer CNF with exactly the checked 2772-primary block ordering and 572 row targets.
• Independently compare every primary incidence and cardinality target against the frozen selection before solving.
• Run CaDiCaL at a matched conflict cap with proof logging; decode SAT directly and replay any complete UNSAT proof.
• Stop if the cross-encoding is UNKNOWN without a material propagation 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/2607.23766 ↗

GPT-5.6 Sol acted as principal investigator. Supplied GPT-5.6 Terra delegate memos were advisory only; Sol independently reconstructed the selected record and rejected an erroneous minimum-orbit characterization. Python 3.12.3 generated, hashed, regenerated and checked artifacts. Z3 4.13.0 built and searched the native pseudo-Boolean instance. Web search rechecked the maintained status. No CAS, proof assistant, cloud lab or external solver service was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1408.8s

Review state

not a result claim

Attempt ID

covering-c1553-20260809-040548-24d7c8

No human review recorded.