Matched all-four-type native pseudo-Boolean pilot for 13 endpoint-collision inequalities, with fresh base and 104-pair-upper controls.

compact pair-excess propagation

Represent the 325 forbidden endpoint-excess header collisions by 13 joint pair-multiplicity inequalities and measure their propagation value without materializing internal skeletons.

Hypothesis: The 13 endpoint-collision PB rows retain at least half the aggregate rlimit saving of 104 pair-upper rows while reducing base rlimit by at least 20 percent, never regressing a type, and using at most one quarter of incidences.

Test: Run fresh base, 13-row collision, and 104-row upper formulas on all four canonical pair types at seed 0 and 5,000 conflicts, then independently reconstruct all formulas and recompute the aggregate gate.

All twelve formulas and the aggregate comparison were independently reconstructed, and six mutations failed closed. The three predeclared performance requirements failed, so more cap or seeds for this encoding have lower expected value than conditioned proof-producing alternatives. UNKNOWN runs exclude no object.

• Every hypothetical 54-cover satisfies lambda_az+lambda_bz<=12 for all distinct points a,b,z.
• The 13-row collision encoding uses exactly 5,720 incidences per canonical type versus 27,170 for the 104-row upper encoding.
• At the matched four-type seed-0 5,000-conflict protocol, collision aggregate rlimit is 11,617,893 versus 13,838,445 base and 6,499,880 upper; type 4 regresses to 3,665,458 from 3,517,193.

• Experiment 20260811-061718-3c9678 completed in 71.431 seconds with return code 0 and peak child memory 76,988 KiB.
• independent-check.json accepted 12 formula receipts, recomputed every aggregate, and identified type 4 as the sole rlimit regression.
• mutation-controls.json rejected all six semantic corruptions.
• manifest.sha256 binds the protocol, generators, checkers, all raw formulas/results/checks, aggregate result, and toolchain.

• .proof-experiments/20260811-061718-3c9678: twelve matched UNKNOWN runs; independently recomputed gate failed with type-4 regression.

check_cross_type_endpoint_collision_pb_v1.py reconstructs all formulas using bit masks and requires byte-identical SMT2; check_cross_type_endpoint_collision_summary_v1.py separately recomputes all resource aggregates and the gate; neither imports the producer.

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

• Weighted-degree-two pair-excess graph -> predict 13 joint endpoint bounds encode collision headers compactly -> observed exact 5,720-incidence encoding but insufficient robust type-4 search gain.

• Every 54-block C(15,5,3) cover has pair multiplicities at least five and pair excess weighted degree two at every point; hence any two incident pair multiplicities sum to at most 12.
  Human-checkable exact double count, independently instantiated in all four formula types. · Any hypothetical 54-cover on 15 points. · proved
• The endpoint-collision abstraction excludes exactly 325 of 8,281 ordered weight-two endpoint headers.
  Closed count 13+2*13*12 and the predecessor exhaustive type-4 enumeration. · Each normalized-pair canonical type's abstract endpoint header universe. · proved
• The compact collision protocol fails its matched performance gate.
  Accepted independent-check.json: 16.0463% base reduction, 30.2587% retained upper saving, and type-4 regression. · Z3 4.13.0, seed 0, 5,000 conflicts, all four canonical types. · computed

• Scale the global 13-row native-PB endpoint-collision encoding after the seed-0 pilot.
  All four canonical types under Z3 4.13.0 at the frozen 5,000-conflict protocol. · It misses the aggregate and retained-saving thresholds and regresses on type 4. · result.json and independently recomputed independent-check.json · A materially different proof-producing or conditioned encoding with a predeclared mechanism explaining reversal of the type-4 regression.
• Rerun the complete fixed-pair link as a new discriminator.
  The 754 frozen targets and canonical baseline CNFs. · All targets already survive the relaxation and the globally complete CNF link clauses have zero delta. · artifacts/type4-complete-pair-link-gate-20260809/independent-check.json and artifacts/pair-link-cnf-delta-audit-20260811/independent-check.json · New labelled information beyond link coverage with an independently checked nonzero semantic delta.

• Header-conditioned proof-producing collision encoding on type 4.
  Conditioning may convert globally weak redundant rows into local propagation while retaining a replayable certificate path. · Generate one matched conditioned base/collision CNF or VeriPB instance, audit clause delta, and stop unless decisions fall at least 20%. · high · open
• New constructive neighborhood beyond verified defect 10.
  A checked 54-cover remains terminal and methodologically distinct, but prior 2-for-2 and strict 3-for-3 neighborhoods are exhausted. · Derive a new exact move family and precompute its incremental defect delta before any sweep. · normal · open

Objective: Test proof-capable conditioned pair-excess propagation on the hardest canonical branch.

First action: Select one globally complete saved type-4 cube/header split, freeze base and collision proof encodings, and run an independent clause-delta audit before solver telemetry.

Stop condition: Stop on zero delta, any semantic mismatch, less than 20% matched decision reduction, or another type-4 regression; promote only a directly checked cover or replayed proof result.

• Freeze one proof-producing type-4 conditioned collision encoding and independently audit its nonzero clause delta before solving.
• Require at least 20% matched decision reduction and replay any UNSAT proof; redirect on another type-4 regression.
• Keep the constructive route on hold until a new exact neighborhood has a credible defect-below-10 discriminator.
• Do not repeat the complete fixed-pair link, explicit weighted-skeleton quotient, or this global 13-row seed-0 PB protocol.

• 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://github.com/dmgordo/LJCR ↗
• https://arxiv.org/abs/2607.23766 ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol principal investigator designed, implemented, ran, audited, and interpreted the epoch. GPT-5.6 Terra delegates supplied bounded advisory reconnaissance only; their stale fixed-link proposal was rejected and model agreement was not validation. Python 3.12.3, Z3 4.13.0, exact combinatorial derivation, separate bit-mask and aggregate checkers, SHA-256, mutation testing, the computational-researcher experiment harness, and current web source checks were used. No CAS, proof assistant, lab job, package installation, system change, external write, publication, or Git operation was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1668.8s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1553-20260811-062643-9a3205

No human review recorded.