Matched two-seed comparison of the globally complete root-block native-PB encoding with and without all 105 theorem-implied pair floors.

global native-PB propagation control

Fix block 01234 by S_15 transitivity, enforce exact degree 18 and triple coverage, then add lambda_uv >= 5 directly for every pair without auxiliary variables.

Hypothesis: Adding all 105 pair floors reduces deterministic Z3 resource usage by at least 20 percent at matched 5000-conflict caps on seeds 0 and 1, without a seed-level regression.

Test: Compare fresh base/floor Z3 processes at seeds 0 and 1 under identical 5000-conflict caps; require no seed-level rlimit regression and at least 20 percent aggregate rlimit reduction.

The hypothesis required no seed-level regression and at least 20 percent aggregate rlimit reduction. The independently reproduced reductions were -13.0206 percent and -5.8678 percent, so both predicates fail. UNKNOWN provides neither a witness nor an exclusion.

• The base formula has 3002 primary variables and 460 native-PB assertions.
• The floor formula adds exactly 105 inequalities and 30020 primary incidences with no auxiliary variables.
• At matched 5000-conflict caps, aggregate rlimit-count rose from 9442780 to 10333883.
• The bounded runs exclude no assignment or covering family.

• python3 scripts/global_native_pb_pair_floor_v1.py --mode base|floor --seed 0|1 --max-conflicts 5000 --timeout-ms 60000
• python3 checkers/check_global_native_pb_pair_floor_v1.py on all four formula packets returned valid=true
• python3 scripts/test_global_native_pb_pair_floor_mutations_v1.py returned accepted_clean=1 and rejected_mutations=7
• python3 checkers/check_global_native_pb_pair_floor_result_v1.py returned valid=true with zero mismatches

• .proof-experiments/20260810-074204-9f75ac: one clean formula accepted and seven mutations rejected
• .proof-experiments/20260810-074240-a7e96d and 20260810-074240-edf603: seed-0 base/floor UNKNOWN; rlimit regression 13.0206 percent
• .proof-experiments/20260810-074240-7bf57a and 20260810-074240-af18c6: seed-1 base/floor UNKNOWN; rlimit regression 5.8678 percent
• .proof-experiments/20260810-074317-0227ad, 623226, ac0a11, ce91e2: all four independent formula checks valid
• .proof-experiments/20260810-074503-359f37 and 20260810-074508-d3b990: fail-closed summary and independent arithmetic audit valid

checkers/check_global_native_pb_pair_floor_v1.py reconstructs every incidence using recursive 15-bit masks; checkers/check_global_native_pb_pair_floor_result_v1.py independently recomputes telemetry aggregates and gate predicates.

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

• C(12,6,4) certificate workflow -> require proof-compatible measured reductions before scale-up -> native pair floors failed the measured gate and were closed.
• Redundant-constraint propagation engineering -> predict direct sparse PB rows outperform implicit triple consequences -> observed only 2.2867 percent fewer PB propagations but 9.4369 percent higher deterministic resource use.

• Every pair in a hypothetical 54-block cover has multiplicity at least five.
  Thirteen containing triples divided by three third points covered per containing block. · All hypothetical 54-block C(15,5,3) covers · proved
• The checked pair-floor encoding adds 105 rows and 30020 incidences to the 460-row global base.
  Four independent bit-mask reconstructions and mutation controls. · Protocol global-native-pb-pair-floor-v1 · computed
• Pair-floor protocol v1 regressed aggregate rlimit-count by 9.4369 percent at its matched two-seed cap.
  Result SHA-256 166f89a1647212cfceb89ee540c81fe708c9f37ed9e0449e5b6c253ff03d8188 and independent audit. · Z3 4.13.0, seeds 0 and 1, 5000-conflict protocol · computed

• Rerun the complete fixed-pair-link relaxation as a new discriminator.
  All 395 type-4 signatures and 754 signature/e_45 targets under the complete 13-triple fixed-pair link. · The existing independently checked artifact retains every target. · Result SHA-256 b5eb3ccf2ad757c0f2ec3098553a6c89ac47adb7c8cd68d10a2fa11ddd5ae9fb; checker SHA-256 4370846c3d0de118174b9187680477b9338c0db72655199575cd0bfbaad35b49. · Add genuinely new labelled information beyond the full fixed-pair link.
• Scale global native-PB pair-floor protocol v1 by raising its cutoff or changing only the seed.
  Root-block-normalized Z3 native-PB base/floor formulas at seeds 0 and 1. · Both seeds regressed in deterministic resource usage and all runs remained UNKNOWN. · artifacts/global-native-pb-pair-floor-20260810/independent-check.json · A materially different representation that beats a matched base and preserves replayable proof production, or a checked 54-cover.

• Proof-replayed 12-by-256 layer-five successor around the verified defect-10 seed.
  Its 288-cell predecessor was independently certified UNSAT and it is the strongest measured local route. · After explicit owner approval, submit exactly 3072 hash-bound cells as twelve independently replayed 256-cell union formulas. · high · open
• Genuinely different proof-preserving global encoding.
  Only a global SAT model or complete replayable exclusion can settle the exact target; pair floors, pair uppers, lex leaders, and fixed-pair relaxations are closed. · Predeclare one matched proof-producing encoding calibration with independent reconstruction and a small replayed UNSAT control. · normal · open

Objective: Resolve whether to run the exact 3072-cell proof-replayed layer-five successor.

First action: Present the epoch-44 predecessor receipt and request explicit human-owner approval for exactly twelve 256-cell unions.

Stop condition: Approval dispatches only the hash-bound scope; rejection or silence redirects to a genuinely different proof-preserving global encoding.

• Do not rerun the completed 754-target fixed-pair-link gate.
• Do not increase the native pair-floor v1 cutoff or retry it with seed-only changes.
• Request explicit owner approval for exactly twelve proof-replayed 256-cell layer-five unions, totalling 3072 hash-bound cells.
• If approval is withheld, design a materially different proof-preserving global encoding and require a matched improvement before scale-up.

• 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/math/9502238 ↗

GPT-5.6 Sol served as principal investigator. GPT-5.6 Terra delegates supplied advisory reconnaissance only; Sol independently audited and rejected the stale fixed-pair recommendation. Python 3.12.3, Z3 4.13.0, exact tuple generation, recursive bit-mask checking, mutation controls, SHA-256, shell utilities, the computational-researcher experiment harness, and official-source web search were used. No sub-agent, CAS, proof assistant, lab job, DRAT/LRAT solver run, or external publication was used this epoch.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1234.3s

Review state

not a result claim

Attempt ID

covering-c1553-20260810-075136-2d8b70

No human review recorded.