Construct an exactly-once fixed-first 249-profile assumption manifest with reusable unary intersection counters, independently reconstruct it, and compare its rank-2 leaf against the prior fixed-second encoding.

fixed-first profile partition with shared unary-counter SAT prefix

A single incidence CNF exposes six exact intersection-count counters; each necessary profile is represented by 6--12 threshold assumptions and independently audited for exactly-one ownership.

Hypothesis: The fixed-first shared-count frontier is exactly-once for every simple 30-cover and its rank-2 leaf either terminates or exceeds the legacy leaf by at least 1.25x conflict rate without increasing LRAT bytes per conflict.

Test: Independently enumerate all 278256 weak profiles and evaluate all 249 assumption cubes, then run two five-second seeds per encoding and replay every emitted LRAT prefix with two fresh checkers.

The profile checker establishes a reusable, gap-free internal certificate frontier, which is net-new validated infrastructure. However, no new leaf received a witness or accepted UNSAT proof, and the engineering discriminator rejected scale-up of the unchanged fixed-first shared encoding.

• Every simple fixed-first 30-cover model has exactly one of the 249 recorded profile assumption cubes.
• The shared formula has 34210 variables and 174192 clauses and binds one closed profile plus 248 unresolved profiles.
• For the declared rank-2 calibration, all four runs were UNKNOWN and every incomplete LRAT prefix was explicitly rejected by both fresh proof checkers.

• python3 checkers/check_incidence_matrix_pilot_v1.py ... --receipt artifacts/epoch44-20260810/fixed-first-base-fresh-audit.json
• python3 scripts/build_fixed_first_profile_manifest_v1.py --out-dir artifacts/epoch44-20260810/fixed-first-profile-manifest-v3
• python3 checkers/check_fixed_first_profile_manifest_v1.py --manifest artifacts/epoch44-20260810/fixed-first-profile-manifest-v3/profile-manifest.json --out artifacts/epoch44-20260810/fixed-first-profile-manifest-v3/independent-check.json
• python3 scripts/run_shared_profile_calibration_v1.py --manifest artifacts/epoch44-20260810/fixed-first-profile-manifest-v2/profile-manifest.json --out-dir artifacts/epoch44-20260810/shared-profile-rank2-calibration-v1 --seconds 5
• python3 checkers/check_shared_profile_calibration_v1.py --run-receipt artifacts/epoch44-20260810/shared-profile-rank2-calibration-v1/run-receipt.json --out artifacts/epoch44-20260810/shared-profile-rank2-calibration-v1/independent-check-v3.json
• sha256sum -c artifacts/epoch44-20260810/SHA256SUMS

• .proof-experiments/20260810-054134-148cb2: fresh fixed-first base audit passed.
• .proof-experiments/20260810-054720-6508dc: scope-correct v3 manifest built with 249 profiles.
• .proof-experiments/20260810-054729-40dd12: independent v3 profile audit passed.
• .proof-experiments/20260810-054321-ed203f: four matched rank-2 solver runs all returned UNKNOWN.
• .proof-experiments/20260810-054555-6a70a1: independent timing, status, and dual-replay audit produced HOLD.
• .proof-experiments/20260810-054823-978158: v2 calibration bytes were proved identical to the v3 formula and assumptions.

checkers/check_fixed_first_profile_manifest_v1.py independently reconstructs profiles by bar positions, uses Cartesian truth tables for indicators, validates local totalizer semantics, evaluates every cube, checks mutations, and verifies retained proof identities. checkers/check_shared_profile_calibration_v1.py independently reparses logs and timing and freshly compiles two LRAT replayers.

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

• Incremental SAT shared-counter compression -> predicted better proof throughput -> observed 0.9566x conflict rate because removing fixed-second symmetry outweighed the smaller formula.

• There are exactly 249 necessary fixed-first intersection profiles for simple hypothetical 30-covers, occupying 30 nonempty (r,q) cells.
  profile-manifest-v3 and independent-check.json · Simple fixed-first 30-cover models · computed
• The 249 assumption vectors are mutually exclusive and exhaustive on the necessary profile vectors.
  Exactly 249 accepting memberships after evaluating every necessary profile against every cube. · The six intersection-count coordinates with no residual copy of F · computed
• Profile (0,1,25,0,0,3) remains dual-replayed UNSAT, leaving 248 unresolved profiles.
  Hash-bound epoch-42 proof and epoch-43 fresh dual replay embedded in the v3 manifest. · That normalized unique-minimum-owner profile only · computed

• Scale the unchanged fixed-first shared-profile proof-search encoding.
  Rank-2 profile (1,0,24,1,0,3), seeds 0 and 1, five seconds per arm, CaDiCaL 1.7.3. · It returned UNKNOWN in both runs and failed both matched continuation gates. · run-receipt.json and independent-check-v3.json · A material change retaining fixed-second symmetry, a different proof-producing solver, or terminal evidence.

• Compact fixed-second reusable-counter profile encoding.
  It combines the smaller profile mechanism with the representative symmetry whose loss explains the failed fixed-first calibration. · Build the r=0 rank-2 formula from the fixed-second source with full counters over columns 2..29 and repeat the frozen two-seed test. · high · open
• Proof-producing PB decomposition.
  Exact degree equations are natural PB constraints, but no admissible native-PB proof replayer is currently installed. · Qualify a pinned proof emitter and independent replayer before compiling any substantive PB cell. · normal · open

Objective: Test whether reusable counters and fixed-second representative symmetry compose into a materially better proof-producing rank-2 leaf.

First action: Extend incidence-orbit-r0.cnf with full counters over columns 2..29 and assumptions for profile (1,0,24,1,0,3).

Stop condition: Stop on semantic or hash mismatch, proof-replay disagreement, four UNKNOWN runs with conflict ratio below 1.25, or LRAT-bytes-per-conflict ratio above 1.0.

• Start from artifacts/epoch9-20260808/incidence-orbit-pilot-v1/incidence-orbit-r0.cnf.
• Add full reusable intersection counters over columns 2..29 and encode residual profile counts by assumptions.
• Independently reconstruct the compact fixed-second formula.
• Run the same two-seed five-second LRAT comparison and require both frozen gates or terminal evidence.

• https://ljcr.dmgordon.org/cover/show_cover.php?v=15&k=6&t=3 ↗
• https://doi.org/10.5281/zenodo.19735294 ↗
• https://arxiv.org/abs/math/9502238 ↗

GPT-5.6 Sol principal performed synthesis, implementation, audit, and reporting. GPT-5.6 Terra delegates supplied bounded advisory prior-art and verification reconnaissance only. Deterministic tools: Python 3.12.3, z3 in the retained base audit, CaDiCaL 1.7.3, GCC, lrat-check, CakeLPR, sha256sum, and repository scripts/checkers. No delegate or model agreement was treated as validation.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1715.5s

Review state

evidence receipt failure; not durable progress

Attempt ID

covering-c1563-20260810-055610-543c01

No human review recorded.