Added 13 theorem-forced high-point pair equations to the fixed-link residual CNF, independently checked their derivation and cardinality semantics, and compared baseline, exact-36, and pair-aware formulas under a matched 5000-conflict CaDiCaL pilot.

pair-excess-strengthened local-link residual SAT

The root–high pair has multiplicity seven and exhausts the high point's weighted pair-excess degree two, forcing its other 13 total pair multiplicities to five; the resulting residual targets are encoded as exact totalizers.

Hypothesis: The 13 globally forced high-point pair equations materially improve the bounded fixed-link extension search, or produce a directly checkable 54-block cover.

Test: Compare baseline, redundant exact-36, and pair-aware formulas with CaDiCaL 1.7.3 at a nominal 5000-conflict cap; retain pair-aware only if decisive or at least 20% faster than baseline without increased memory.

The pair equations are sound, but bounded telemetry shows no search benefit. UNKNOWN carries no mathematical force, so the legitimate progress is the validated constraint packet, negative method comparison, and evidence-based route redirect.

• For the displayed fixed link, every hypothetical 54-cover extension has residual high-point pair targets 4^6,3^6,2^1.
• The fixed-link totalizer accepted exactly the requested weights in all 192 exhaustive six-variable controls for targets 2, 3, and 4.
• Baseline, exact-36, and pair-aware matched runs all returned UNKNOWN.
• Pair-aware was 21.28% slower and used 8.92% more memory than baseline on the recorded machine and solver.
• The exact range remains 54 <= C(15,5,3) <= 55.

• python3 scripts/test_fixed_link_totalizer.py --solver /usr/bin/cadical
• python3 scripts/fixed_link_extension_cnf.py generate --link artifacts/local-link-pilot-20260808/live-7-5x13-witness.txt --forced-pair-point 0 --output artifacts/fixed-link-pair-pin-pilot-20260808/pair-a.cnf
• python3 checkers/check_fixed_link_pair_pin.py --link artifacts/local-link-pilot-20260808/live-7-5x13-witness.txt --point 0 --cnf artifacts/fixed-link-pair-pin-pilot-20260808/pair-a.cnf
• /usr/bin/cadical -c 5000 -w artifacts/fixed-link-pair-pin-pilot-20260808/base-5000.model artifacts/fixed-link-pair-pin-pilot-20260808/base-a.cnf
• /usr/bin/cadical -c 5000 -w artifacts/fixed-link-pair-pin-pilot-20260808/count-5000.model artifacts/fixed-link-pair-pin-pilot-20260808/count-a.cnf
• /usr/bin/cadical -c 5000 -w artifacts/fixed-link-pair-pin-pilot-20260808/pair-5000.model artifacts/fixed-link-pair-pin-pilot-20260808/pair-a.cnf
• python3 checkers/check_matched_telemetry.py --baseline .proof-experiments/20260808-173213-47fcf4/stdout.txt --exact-36 .proof-experiments/20260808-173216-a40a1d/stdout.txt --pair-aware .proof-experiments/20260808-173219-790249/stdout.txt
• sha256sum -c artifacts/fixed-link-pair-pin-pilot-20260808/manifest.sha256

• .proof-experiments/20260808-173014-b3a339: all 192 exact-cardinality controls passed
• .proof-experiments/20260808-173154-ffe696: independent target derivation and CNF metadata check passed
• .proof-experiments/20260808-173213-47fcf4: baseline returned UNKNOWN at 5000 conflicts
• .proof-experiments/20260808-173216-a40a1d: exact-36 returned UNKNOWN at 5000 conflicts
• .proof-experiments/20260808-173219-790249: pair-aware returned UNKNOWN after 5013 reported conflicts
• .proof-experiments/20260808-173831-54b580: independent telemetry comparison reproduced all figures and rejected retention
• .proof-experiments/20260808-173856-d0ba8d: final packet integrity check passed

checkers/check_fixed_link_pair_pin.py independently parses the link and recomputes every target; checkers/check_matched_telemetry.py independently parses all solver logs. No SAT witness or UNSAT certificate arose for global checking.

not_requested

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

Original model outcome

progress

Public classification

progress

• Pair-excess multigraph degree -> predict exact residual high-point pair counters -> targets 4^6,3^6,2^1 were independently confirmed, but bounded search slowed.
• Certified-SAT workflow from C(12,6,4) -> require proof replay and treat UNKNOWN as non-evidence -> no local or global exclusion was claimed.
• Exact-cardinality testing -> predict the shared counter emitter is semantically correct on small exhaustive cases -> all 192 cases passed.

• Any 54-cover extending the displayed link has residual pair targets 4^6,3^6,2^1 at local point 0.
  Pair-excess derivation and experiment 20260808-173154-ffe696. · Extensions of the displayed labeled link only. · proved
• The pair-aware CNF has 2002 primary variables, 58753 total variables, and 400531 clauses.
  Byte-identical CNFs with SHA-256 26d7f585ebf20a908d7257d3333678f47b88bcbca0605a4ed9ce461368adc8c3. · The recorded generator, link, and forced-pair-point 0. · computed
• Pair-aware failed the predeclared retention threshold.
  Experiment 20260808-173831-54b580. · Recorded formulas, machine, CaDiCaL 1.7.3, and nominal 5000-conflict cap. · computed

• Scale the monolithic fixed-link formula merely by adding exact-36 or the 13 forced-pair counters.
  This displayed link and matched CaDiCaL 5000-conflict protocol. · Both variants remained UNKNOWN and were slower and larger than baseline. · artifacts/fixed-link-pair-pin-pilot-20260808/result.json · A materially faster encoding, an audited proof-producing cube, or measured evidence of useful propagation.
• Treat any matched UNKNOWN result as evidence for or against extendability.
  Experiments 20260808-173213-47fcf4, 20260808-173216-a40a1d, and 20260808-173219-790249. · No model or UNSAT proof was produced. · Each solver result file contains UNKNOWN and each receipt has return code zero. · A directly checked SAT model or independently replayed UNSAT certificate.

• Root-block-only constructive SAT calibration.
  It retains every point-link type and SAT directly settles C(15,5,3)=54. · Generate and control-test the fixed-01234 exact-degree CNF, then run at 5000 conflicts. · high · open
• Joint skeleton-and-distinguished-block certified exclusion.
  It is the verification-compatible negative route if constructive calibration is prohibitive. · Enumerate and independently audit joint orbits before producing any UNSAT leaves. · normal · open
• Pseudo-Boolean semantic control for the root-block encoding.
  A materially different formulation can catch variable-map or exact-degree errors before scale-up. · Fix a known model or small mutation in both CNF and PB encodings and compare status. · low · open

Objective: Calibrate root-block-normalized constructive SAT across all point-link types.

First action: Implement a deterministic generator fixing block 0,1,2,3,4 with all 15 exact degree-18 constraints and all 455 triple clauses, then run a fixed-model control.

Stop condition: SAT advances to independent global validation; replay-checked UNSAT settles the target globally under block normalization; prohibitive UNKNOWN redirects to joint-orbit census.

• Implement a deterministic global generator fixing block 01234 while leaving the complete point link free.
• Enforce all 15 point degrees exactly 18 and all 455 triple coverage clauses.
• Add a decoder and a fully fixed positive encoding control before live search.
• Run a 5000-conflict CaDiCaL calibration.
• Validate any SAT model with both existing global checkers and a separate fixed-model encoding.
• Accept global UNSAT only with a replayed DRAT/LRAT certificate.

• 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 and independently audited advisory GPT-5.6 Terra delegate memos; Terra suggestions were not treated as evidence. Python 3.12.3 generated and checked artifacts, CaDiCaL 1.7.3 performed exact SAT controls and bounded searches, and sha256sum bound the packet. No CAS, proof assistant, external lab job, or unverified LLM agreement was used as decisive evidence.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1158.9s

Review state

not a result claim

Attempt ID

covering-c1553-20260808-174207-c109e4

No human review recorded.