Independently test exact 31-cell root-flow refinement, then calibrate a hash-bound direct native-PB formulation of the certified partition-[15], root-mask-31 leaf with and without its reflection lex-leader.

native pseudo-Boolean constructive leaf search

Z3 directly searches 3002 residual block variables subject to 445 coverage inequalities and 105 exact pair equalities, avoiding totalizer auxiliaries; a matched control measures the optional C2 reflection lex-leader.

Hypothesis: Exact root-cell conservation eliminates at least one of the selected leaf's 20 profiles, or, after that refinement, native PB finds a model within 25000 conflicts.

Test: Produce independently checkable integer witnesses for every surviving flow profile, then run matched 25000-conflict direct-PB searches with and without the sound reflection lex-leader.

The positive evidence consists only of exact local witnesses, deterministic encodings, and validated telemetry. Neither solver run supplied a model or replayable proof, so the exact covering number and even the selected cube remain unresolved.

• For the certified partition-[15], root-mask-31 leaf, all 20 aggregate profiles satisfy the tested exact 31-cell root-flow conservation system.
• The checked direct-PB leaf contains 3002 primaries, 445 width-66 coverage constraints, 105 exact pair equalities, and 59390 incidence terms.
• At a 25000-conflict setting, Z3 4.13.0 returned UNKNOWN after 25001 conflicts in both configurations: 2.492 seconds with reflection and 1.448 seconds without reflection.
• No 54-block cover was found and no cube was excluded.

• python3 checkers/check_root_flow_refinement_v1.py --source-manifest artifacts/joint-orbit-census-20260808/manifest.json --result artifacts/root-flow-refinement-20260808/result.json
• python3 checkers/check_direct_pb_leaf_v1.py --source-manifest artifacts/joint-orbit-census-20260808/manifest.json --manifest artifacts/direct-pb-leaf-15-root31-v1/result.json --smt2 artifacts/direct-pb-leaf-15-root31-v1/instance.smt2
• python3 checkers/check_direct_pb_leaf_v1.py --source-manifest artifacts/joint-orbit-census-20260808/manifest.json --manifest artifacts/direct-pb-leaf-15-root31-v1/control-noref-result.json --smt2 artifacts/direct-pb-leaf-15-root31-v1/control-noref-instance.smt2
• All artifact SHA-256 manifests replayed successfully.

• .proof-experiments/20260808-201812-7b1e23: all 20 root-flow profiles SAT with arithmetic-checked witnesses
• .proof-experiments/20260808-201541-632cd6: reflection direct-PB UNKNOWN at 25001 conflicts after 2.492 seconds
• .proof-experiments/20260808-201636-bc96a6: no-reflection direct-PB UNKNOWN at 25001 conflicts after 1.448 seconds

check_root_flow_refinement_v1.py checks every integer witness without Z3. check_direct_pb_leaf_v1.py independently rebuilds all block, triple, pair, and reflection incidences, parses the SMT2 assertions, and exhaustively checks the lex formula on four-bit controls. No SAT witness existed for the two global cover checkers.

not_requested

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

Original model outcome

progress

Public classification

progress

• Sparse PB encoding -> predicted lower auxiliary overhead than totalizer CNF -> matched-cap wall time improved substantially, but status remained UNKNOWN.
• Group-theoretic lex-leader -> predicted smaller reflected search -> the constraint was sound but increased compiled variables, decisions, and wall time in this Z3 configuration.

• All 20 aggregate profiles for the certified root-31 leaf satisfy the tested 31-cell conservation system.
  Twenty explicit result witnesses, each checked by direct integer arithmetic. · Partition [15], root mask 31, using only total, root-point, root-pair, and profile equations. · computed
• The root-stabilizing reflection is a cycle automorphism, is involutive, and fixes 20 residual block variables.
  Independent reconstruction in check_direct_pb_leaf_v1.py. · The certified 15-cycle/root-01234 leaf. · proved
• Both recorded native-PB runs reached the 25000-conflict cap without SAT or UNSAT.
  Hash-bound result JSON and experiment receipts. · Exact recorded solver, parameters, and instances. · computed

• Exact root-cell conservation alone shrinks the selected leaf's 20 aggregate profiles.
  The displayed 31-cell system for partition [15], root mask 31. · Every profile has a valid explicit witness. · artifacts/root-flow-refinement-20260808/result.json and its arithmetic checker. · A new sound constraint involving information absent from the tested system, such as outside-triple or root-triple incidence coupling.
• The reflection lex-leader improves this Z3 configuration at the matched 25000-conflict cap.
  Pinned Z3 4.13.0, native PB, seed 0, selected leaf. · It increased solve time from 1.448 to 2.492 seconds and decisions from 167999 to 183124. · Matched result JSON files and experiment receipts. · A different solver/encoding or repeated matched measurements showing a decisive benefit.
• Treat either UNKNOWN status as a local exclusion.
  Both direct-PB runs. · Neither produced UNSAT or a replayable proof. · Both result files report max-conflicts-reached UNKNOWN. · A complete proof-producing UNSAT run with independent replay.

• One 250000-conflict no-reflection native-PB constructive follow-up.
  Measured throughput suggests it should remain cheaper than the prior 25000-conflict totalizer run while exploring ten times the native-PB conflict budget. · Reuse direct_pb_leaf_v1.py with --max-conflicts 250000 and no reflection; accept only a dual-checked model. · high · open
• Proof-producing OPB solver calibration.
  A native PB solver with replayable certificates could make an UNSAT leaf result admissible, unlike Z3 UNKNOWN or unchecked UNSAT. · Pin a project-scoped solver and checker, pass target-minus-one/target/target-plus-one semantic controls, then run only the calibrated leaf. · normal · open

Objective: Determine whether the fast no-reflection PB formulation can produce a 54-cover before investing in a proof-producing toolchain.

First action: Run direct_pb_leaf_v1.py on the same source with --no-reflection --max-conflicts 250000 --timeout-ms 120000 under run_experiment.py.

Stop condition: Stop and redirect after UNKNOWN or unchecked UNSAT; promote only a 54-block witness accepted by the PB checker and both global cover checkers.

• Run one 250000-conflict no-reflection direct-PB experiment on the same hash-bound leaf; dual-check any SAT witness and stop after UNKNOWN.
• Evaluate a pinned proof-producing OPB solver on semantic controls before any UNSAT search.
• Do not revisit the tested root-flow refinement unless an additional theorem-strength constraint couples cells to outside-triple coverage.

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

GPT-5.6 Sol principal audited, implemented, ran, and interpreted the epoch. GPT-5.6 Terra delegates supplied advisory root-flow and prior-art/challenger memos; Sol promoted their provenance, independently reproduced relied-on claims, and rejected the advised invalid Z3 parameter spelling. Python 3.12.3 generated artifacts and ran arithmetic/combinatorial checks. Z3 4.13.0 supplied native pseudo-Boolean search and the flow witnesses. No CAS, proof assistant, external publication, cloud lab job, or additional Sol-spawned sub-agent was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

990.8s

Review state

not a result claim

Attempt ID

covering-c1553-20260808-202319-498a53

No human review recorded.