Matched native external-LRAT and no-proof calibration on the frozen q0-m0 type-0 depth-four completion cylinder.

proof-producing incidence/PB cube decomposition

Hold the exact q0-m0 incidence CNF and CaDiCaL search settings fixed, replace ASCII DRAT with native external LRAT under the same 8-MiB cap, and compare with a no-proof control.

Hypothesis: On the exact q0-m0 CNF, CaDiCaL 1.7.3 native external LRAT reaches SAT or UNSAT before the same 8388608-byte cap that stopped ASCII DRAT.

Test: Run native LRAT and no-proof arms on the identical hash-pinned CNF; require a checked cover or independently replayed complete proof for a mathematical result.

A solver exit without a certificate cannot satisfy the negative-result verification contract. Both retained LRAT traces are incomplete and rejected, so they support only a mechanism-level redirect.

• The frozen q0-m0 CNF has 49962 variables, 191161 clauses, and SHA-256 d81a3160db2fa07522fed34a4ea8aad678aeb0d7d955caf06394d72e7993f924.
• Two matched native external-LRAT runs produced the same exact 8388608-byte prefix with SHA-256 f7c45ddb7d04a73536acb499484705f2acfa95419fa396edcb95e4edd6a02c98 before any SAT/UNSAT result.
• The matched no-proof arm returned solver-UNSAT after 9310 conflicts and 3.84 process seconds; this is uncertified telemetry.
• No covering bound changed.

• python3 scripts/q0_m0_native_lrat_calibration_v1.py --out-dir artifacts/epoch88-20260811/q0-m0-native-lrat-v2 --seconds 60 --wall-seconds 75 --proof-cap-bytes 8388608
• python3 checkers/check_q0_m0_native_lrat_calibration_v1.py --artifact-dir artifacts/epoch88-20260811/q0-m0-native-lrat-v2 --manifest artifacts/epoch87-20260811/type0-32-leaf-pilot-manifest.json --independent checkers/check_root_prefix_global_completion_v1.py --cardinality-source scripts/fixed_block_sat_pilot_v1.py --out artifacts/epoch88-20260811/q0-m0-native-lrat-independent-check-final.json
• sha256sum -c artifacts/epoch88-20260811/SHA256SUMS passed.

• .proof-experiments/20260811-140735-52424e: initial native-LRAT run produced the same capped prefix but exposed a witness-status parsing defect.
• .proof-experiments/20260811-140908-007de3: corrected reproduction returned UNKNOWN_PROOF_CAP for native LRAT and solver-UNSAT for the no-proof control.
• .proof-experiments/20260811-141006-2ac372 and .proof-experiments/20260811-141039-d1a06c: fail-closed checker controls detected incorrect expected argv lengths.
• .proof-experiments/20260811-141114-72be0f: corrected independent checker PASS and REDIRECT_NATIVE_LRAT_SCALEUP.

checkers/check_q0_m0_native_lrat_calibration_v1.py independently reconstructs the CNF and builds both lrat-check and CakeLPR. Both rejected the capped prefix; therefore no UNSAT certificate exists.

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) certified SAT case analysis -> require independently replayable per-leaf proofs -> the q0-m0 capped prefix was rejected and no local exclusion was promoted.

• The frozen q0-m0 formula reconstructs byte-for-byte to the retained CNF.
  artifacts/epoch88-20260811/q0-m0-native-lrat-independent-check-final.json · The single q0-m0 graph6 key and declared constructors. · computed
• The 8-MiB native-LRAT prefix is deterministic across two matched runs.
  Both prefixes have SHA-256 f7c45ddb7d04a73536acb499484705f2acfa95419fa396edcb95e4edd6a02c98. · CaDiCaL 1.7.3 seed-0 -P0 on q0-m0 with native external LRAT. · computed
• The matched no-proof solver run exits 20 after 9310 conflicts.
  q0-m0-no-proof.cadical.log and witness, independently reparsed. · Solver telemetry only; not a certified UNSAT theorem. · computed

• Use unchanged native external LRAT to obtain a terminal q0-m0 certificate under an 8-MiB raw-proof cap.
  Exact q0-m0 CNF, CaDiCaL 1.7.3, seed 0, -P0, external LRAT, internal checking disabled. · Two runs filled the exact cap with an identical incomplete prefix; both proof checkers rejected it. · artifacts/epoch88-20260811/q0-m0-native-lrat-independent-check-final.json · A materially different emitter/compressor or a complete proof under a separately justified budget.

• Sixteen-MiB ASCII-DRAT q0-m0 completion.
  The prior DRAT cap occurred at 7481 conflicts, while no-proof termination occurs at 9310, a narrow 1829-conflict gap. · Run one capped DRAT process, convert only if terminal, and dual-replay the resulting LRAT. · high · open
• Constructive six-representative incidence search with a material propagation enhancement.
  A checked cover remains the smallest terminal certificate and avoids proof-volume scaling. · Predeclare one new sound propagation constraint and compare it with the retained six-case baseline. · normal · open
• Canonical ownership bridge for root-link cylinders.
  Even certified sampled leaves cannot aggregate without exact coverage and ownership. · Formalize an exactly-once deletion ownership predicate and test it on bounded completed-link controls. · normal · open

Objective: Test whether q0-m0's narrow raw-search gap permits a complete replayable ASCII-DRAT certificate within 16 MiB.

First action: Run CaDiCaL 1.7.3 seed-0 -P0 on the frozen q0-m0 CNF with ASCII DRAT, RLIMIT_FSIZE=16777216, then invoke pinned drat-trim, lrat-check, and CakeLPR only if exit 20 occurs before the cap.

Stop condition: Stop on cap, tool/CNF hash drift, conversion failure, replay disagreement, final-line-deletion acceptance, or any attempted extrapolation beyond q0-m0.

• Run exactly one 16-MiB ASCII-DRAT q0-m0 calibration.
• If terminal, convert with pinned drat-trim and require intact replay by lrat-check and CakeLPR plus final-line-deletion rejection.
• Do not start the 32-leaf sample unless this one-leaf certificate gate passes.

• https://www.coveringrepository.com/systems.aspx?k=6&t=3&m=-1 ↗
• https://ljcr.dmgordon.org/cover/show_cover.php?v=15&k=6&t=3 ↗
• https://arxiv.org/abs/2607.23766 ↗

GPT-5.6 Sol was principal investigator. Two pre-completed GPT-5.6 Terra delegates supplied advisory route and verification memos; they were not independent validators, and their artifacts were not used as mathematical evidence. CPython 3.12.3 implemented the runner, reconstruction, and audit. CaDiCaL 1.7.3 performed SAT search and native LRAT emission. GCC 13.3.0 built lrat-check and CakeLPR; both rejected the incomplete trace. SHA-256 and the computational-researcher experiment harness recorded identities, commands, limits, logs, and peak memory. Web search checked the maintained LJCR entry and arXiv comparator. No PB solver, CAS, proof assistant, cloud lab, external proof service, or human validator was used.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1165.0s

Review state

not a result claim

Attempt ID

covering-c1563-20260811-141702-43f65e

No human review recorded.