Construct and independently verify a redundant global pair-envelope extension of the canonical type-4 multiplicity-five CNF, then compare it with the exact base under matched bounded CaDiCaL runs.

multiplicity-five pair normalization

Define lambda_uv>=6 and lambda_uv>=7 threshold atoms for all 105 pairs and enforce exact excess-two conservation at every point to test whether theorem-implied redundancy improves CDCL propagation.

Hypothesis: The independently checked pair-envelope extension either decides canonical type 4 or reduces CaDiCaL propagations by at least 20 percent relative to the matched base.

Test: Run base and extension sequentially with CaDiCaL 1.7.3, seed 0, and the same conflict cap; accept only SAT, UNSAT, or an extension propagation count at most 80 percent of baseline.

The extension's semantics are independently verified, so the telemetry comparison measures the intended mechanism. Both runs reached the matched fallback cap, and the extension missed the predeclared threshold by a large margin. UNKNOWN supplies no feasibility or infeasibility evidence.

• The recorded pair-envelope CNF is an equisatisfiable definitional extension of the exact canonical type-4 base CNF.
• At seed 0 and 10000 conflicts, CaDiCaL 1.7.3 used 11093305 propagations on baseline and 20853327 on the extension.
• The pair-envelope propagation threshold was not met.
• The maintained range remains 54 <= C(15,5,3) <= 55.

• sha256sum -c artifacts/type4-pair-envelope-propagation-20260809/manifest.sha256 passed.
• Independent reconstruction checked 105 pair rows, 210 threshold aliases, 15 conservation rows, 530516 added clauses, and the 594090-clause base prefix.
• Five incidence, fixed-count, threshold-polarity, conservation, and base-prefix mutations were rejected.
• Matched CaDiCaL logs report UNKNOWN at 10001 and 10000 conflicts respectively.

• .proof-experiments/20260809-170511-172334: canonical extension regenerated byte-identically with 172304 variables and 1124606 clauses.
• .proof-experiments/20260809-170255-d81b46: independent reconstruction accepted the complete extension.
• .proof-experiments/20260809-170440-bd84e0: all five activated structural mutations were rejected.
• .proof-experiments/20260809-170633-de80f2: 25000-conflict extension pilot timed out at 17094 conflicts and is non-matched non-evidence.
• .proof-experiments/20260809-170932-80bc4b: fallback baseline returned UNKNOWN after 10001 conflicts and 11093305 propagations.
• .proof-experiments/20260809-171001-7d1bee: fallback extension returned UNKNOWN after 10000 conflicts and 20853327 propagations.
• .proof-experiments/20260809-171106-2708c8: independent telemetry parser recorded propagation ratio 1.879811922596557.

checkers/check_type4_pair_envelope_cnf_v1.py independently rebuilds the complete extension rather than importing the producer; checkers/test_type4_pair_envelope_mutations_v1.py rejected five targeted corruptions.

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

• Certified C(12,6,4) workflow -> require independently replayable proof evidence before any UNSAT promotion -> no promotion occurred because all live statuses were UNKNOWN.
• Layered exact-cover filtering -> test structural or propagation layers before proof-scale SAT -> the pair-envelope layer failed its bounded propagation gate.
• Pseudo-Boolean modelling -> direct cardinality rows may avoid totalizer overhead -> this yields the next falsifiable native-PB size and telemetry test.

• Every pair in a hypothetical 54-cover has multiplicity between five and seven, and every point has total pair excess two.
  Triple coverage gives 3*lambda_uv>=13; exact point degree 18 gives sum_v lambda_uv=72 and 72-14*5=2. · All hypothetical 54-block C(15,5,3) covers. · proved
• The recorded pair-envelope CNF preserves exactly the base primary solutions.
  Independent algebra and exact reconstruction of every emitted clause. · Canonical type-4 base CNF SHA-256 2146afbf93b8d914d4faf42e9c08a2bdcdebe4dc9e10bd358f98b8fde596754f. · proved
• The pair-envelope extension increased propagations by 87.9812 percent at the matched fallback cap.
  telemetry-10k.json and both hash-bound solver logs. · CaDiCaL 1.7.3, seed 0, canonical type 4, 10000 conflicts. · computed

• Scale the balanced-totalizer global pair-envelope extension on the strength of improved propagation.
  CaDiCaL 1.7.3, seed 0, canonical type 4, matched 10000-conflict protocol. · It remained UNKNOWN and increased propagations by 87.9812 percent. · artifacts/type4-pair-envelope-propagation-20260809/telemetry-10k.json · A materially smaller encoding, different solver with matched gain, or concrete evidence that longer behavior reverses the measured regression.
• Treat the incomplete 25000-conflict extension trace as matched evidence.
  The timed-out foreground extension run. · It reached only 17094 conflicts, whereas the comparison protocol required completed equal caps. · .proof-experiments/20260809-170633-de80f2/experiment.json · A completed hash-bound run at the exact matched cap.
• Rerun the saved mapping-1438 outside-subset profile with a larger arbitrary cutoff.
  Its existing native-PB and totalizer-CNF encodings. · Both already returned UNKNOWN; the prior route record requires a new decomposition, propagation mechanism, or certificate-reuse method. · 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.

• Compact native-PB pair-envelope control.
  It tests the same globally valid conservation information without 530516 added totalizer clauses. · Compile and independently count direct PB rows, then run a matched 5000-conflict control only if materially smaller. · high · open
• New global class-level structural reduction.
  A proved quotient or incompatibility test could remove whole type-4 classes before SAT. · Derive one labelled correlation not already contained in the complete fixed-pair link or five anonymous margins. · normal · open
• Exact-pair constructive seed generation.
  A checked target-fibre seed would reopen pair-preserving constructive trades and could ultimately produce a 54-cover. · Seek a materially improved initializer rather than increasing prior unsymmetrized cutoffs. · low · open

Objective: Determine whether direct native pseudo-Boolean pair-envelope rows avoid the failed totalizer overhead.

First action: Create protocols/type4-native-pb-pair-envelope-v1.json and scripts/type4_native_pb_pair_envelope_v1.py, then run `python3 scripts/type4_native_pb_pair_envelope_v1.py --mode count --type 4` with an independently reconstructed coefficient manifest.

Stop condition: Stop before solving if the extension is not materially smaller; after solving, redirect unless it is decisive or improves the matched exact solver-cost metric.

• Create a count-only native-PB compiler for matched type-4 base and pair-envelope formulas.
• Independently reconstruct all coefficient rows and require a material representation reduction before solving.
• If the size gate passes, run a seed-0 5000-conflict matched control; stop immediately without solver-cost improvement.
• Do not increase the saved mapping-1438 literal-profile cutoff without its recorded reopen condition.

• 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://arxiv.org/abs/2603.29548 ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol principal audited the supplied campaign state, designed and implemented the experiment, ran the deterministic checks, and interpreted the evidence. Supplied GPT-5.6 Terra challenger-prior-art and experiment-verification delegates provided advisory memos only; their agreement was not validation. Python 3.12.3 generated and independently reconstructed CNFs; CaDiCaL 1.7.3 produced bounded telemetry; web search checked current status and adjacent primary sources. No proof assistant or CAS was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1738.1s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260809-172033-7098eb

No human review recorded.