Independently compile the frozen mapping-1438 literal profile into a proof-capable balanced-totalizer CNF while algebraically discharging ten redundant outside-point degree rows, validate the complete encoding, and run one bounded CaDiCaL pilot.

proof-capable totalizer CNF

Exact pair equalities imply the outside-point degree equalities, allowing ten large totalizers to be omitted before a proof-logging CDCL run.

Hypothesis: The independently audited reduced totalizer CNF for the frozen mapping-1438 profile is decided within 110 wall-clock seconds and 250000 conflicts.

Test: Run CaDiCaL 1.7.3 once on the exact hash-bound CNF with textual proof logging; accept only a twice-checked SAT cover or independently replayed UNSAT proof.

The compiler and checker establish a reusable exact representation and a sound local row-reduction. However, the verification contract requires a checked 54-cover or a complete replayed UNSAT certificate. The live run produced neither, and its finalized trace was explicitly rejected as incomplete.

• Within the frozen mapping-1438 system, all ten outside-point degree-18 equations are implied by the 95 retained pair equations.
• The reduced exact CNF has 101734 variables, 504789 clauses, 2772 primary variables, 117 totalizer equalities, and 445 raw coverage clauses.
• The exact reduced CNF received status UNKNOWN after the predeclared 110-second CaDiCaL run; this excludes no assignment.
• The maintained global range remains 54 <= C(15,5,3) <= 55.

• python3 checkers/check_outside_subset_profile_cnf_v1.py ... returned valid=true and reconstructed 572 original rows plus all 504789 clauses.
• python3 scripts/test_outside_subset_totalizer_v1.py ... passed 72 controls: 24 SAT and 48 UNSAT.
• python3 checkers/test_outside_subset_profile_cnf_mutations_v1.py ... rejected all four semantic mutations.
• python3 scripts/proof_stack_c532_control_v1.py ... replayed DRAT, converted LRAT, and direct LRAT, and rejected a wrong-formula proof.
• /usr/bin/timeout --signal=TERM 110s /usr/bin/cadical -c 250000 --binary=false instance.cnf live-250k.drat returned UNKNOWN.
• Pinned drat-trim replay of the finalized trace returned NOT VERIFIED: no conflict.

• .proof-experiments/20260809-044141-10bbca: deterministic CNF build produced 101734 variables and 504789 clauses.
• .proof-experiments/20260809-044205-e738b6: independent reconstruction accepted all original rows and emitted clauses.
• .proof-experiments/20260809-044205-cf1d0b: four semantic mutations were rejected.
• .proof-experiments/20260809-044205-cc2cdd: all 72 totalizer boundary controls passed.
• .proof-experiments/20260809-044205-850edc: DRAT/LRAT proof-stack controls passed.
• .proof-experiments/20260809-044254-ce1191: CNF and manifest regenerated byte identically.
• .proof-experiments/20260809-044315-fcd393: live CaDiCaL run reached the 110-second wall limit with UNKNOWN.
• .proof-experiments/20260809-044535-4669bf: finalized incomplete proof trace was NOT VERIFIED.
• .proof-experiments/20260809-044915-b6b1a8: compact result regenerated after pruning the unusable partial trace.

checkers/check_outside_subset_profile_cnf_v1.py is separately structured and does not import the producer. It reconstructs the block universe, all four row families, ten redundancy coefficient vectors, every totalizer interval, and the complete CNF clause sequence. Pinned drat-trim and lrat-check provide materially different proof replay.

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) proof pipeline -> a proof-capable totalizer encoding should provide independently replayable negative certificates -> the proof stack passed controls, but the live local profile remained UNKNOWN.
• Linear redundancy in exact block incidences -> pair equations may imply degree equations through sum_q lambda(p,q)=(k-1)d(p) -> all ten mapping-1438 outside-degree counters were safely removed.
• Group-action class filtering -> class-level canonical signatures may eliminate work that primary-variable lex constraints only reorder -> this is the next count-only discriminator and is not yet tested.

• For every outside point in the frozen mapping-1438 instance, its degree-18 equation follows from the retained pair equations.
  Independent coefficient-vector reconstruction gives coefficient 4 on exactly the incident block variables and pair-target sum 72 for each of ten points. · The exact recorded 15-cycle skeleton, root, primary order, and frozen cell vector. · proved
• The reduced CNF has 101734 variables and 504789 clauses and encodes the same primary solutions as all 572 original PB rows.
  Independent checker reconstructed all source rows and compared the exact complete clause sequence; regeneration and mutations passed. · Frozen mapping-1438 vector only. · computed
• The bounded reduced-CNF run returned UNKNOWN after 110 seconds and 226499 conflicts.
  .proof-experiments/20260809-044315-fcd393/experiment.json and stdout.txt · CaDiCaL 1.7.3, exact CNF SHA-256 e54ae79f4cc733689ae7b1c9d8a7dcd002ea135d57ce715ec271088e82b55ae2. · computed

• Treat the reduced-CNF UNKNOWN status or its partial trace as exclusion of the frozen profile.
  Mapping 1438 and the recorded frozen cell vector. · No empty conflict or completed proof exists; final drat-trim replay returned NOT VERIFIED. · .proof-experiments/20260809-044535-4669bf/stdout.txt · A directly checked SAT model or complete independently replayed UNSAT proof for the exact instance.
• Increase the mapping-1438 native-PB or totalizer-CNF cutoff without a new mechanism.
  The two current exact encodings of the same frozen primary semantics. · Both bounded representations returned UNKNOWN, and a larger arbitrary cutoff supplies little new information. · artifacts/outside-subset-profile-20260809/result.json and artifacts/outside-subset-profile-cnf-20260809/result.json · A measured decomposition, new propagation mechanism, or certificate reuse method that materially changes the expected decision value.

• Stabilizer-canonical residual-signature frontier for common-family type 4.
  It returns to a globally complete normalization and can remove whole compatibility classes before SAT. · Enumerate and independently check exact orbits of residual intersection and pair-demand signatures under the recorded 10368-element action. · high · open
• Degree-and-pair-preserving constructive trade search.
  It is materially distinct from repeated exact feasibility solving, and any 54-block witness settles the global problem directly. · Run a short seeded comparison of constraint-preserving trades against unconstrained block swaps using uncovered triples as the decisive defect. · normal · open

Objective: Count and validate a skeleton-compatible type-4 residual-signature frontier under the full checked stabilizer before generating any SAT leaves.

First action: Implement scripts/type4_signature_frontier_v1.py using artifacts/type4-stabilizer-lex-pilot-20260809 and artifacts/root-pair-excess-coupling-global-20260808, with a count-only output and a separately reconstructed checker.

Stop condition: Any group-action or compatibility mismatch, or no class-level reduction, redirects to the constructive trade route; a substantial reduction promotes independently checked SAT leaf generation.

• Implement a count-only type-4 residual-signature frontier under the checked 10368-element stabilizer action.
• Intersect signature classes with weighted-degree-two pair-excess compatibility before creating any further SAT leaves.
• Independently reconstruct the action, invariants, orbit coverage, and compatibility predicate.
• If no class-level reduction appears, redirect to the degree-and-pair-preserving constructive trade pilot rather than increasing solver cutoffs.

• 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 ↗
• https://github.com/marijnheule/drat-trim ↗

GPT-5.6 Sol served as principal investigator. Two GPT-5.6 Terra delegates supplied advisory prior-art and verification memos; Sol independently reconstructed every relied-upon claim, and model agreement was not treated as validation. Deterministic Python 3.12.3 generated and checked the encoding. CaDiCaL 1.7.3 performed SAT controls and the live run. Project-pinned drat-trim revision 2e3b2dc0ecf938addbd779d42877b6ed69d9a985 and lrat-check replayed proof controls and rejected the incomplete live trace. Z3 4.13.0 supplied only the prior-epoch native-PB baseline. Web search checked current source status. No CAS or proof assistant was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1519.6s

Review state

not a result claim

Attempt ID

covering-c1553-20260809-045343-f6bfdf

No human review recorded.