Hash-bound syntactic dominance audit joining four dual-replayed fixed-link equality predicates to the exactly-owned fixed-first 249-profile frontier.

cross-artifact syntactic proof-scope dominance audit

Bucket candidate implications by reconstructed raw-base CNF SHA-256, then permit elimination only when bases are identical and the owner's exact target map contains every terminal predicate key/value.

Hypothesis: At least one whole live owner in the exact 249-profile frontier is syntactically dominated by a dual-replayed fixed-link equality predicate with an identical raw base CNF.

Test: Check all 249 x 4 owner/predicate pairs for raw-base SHA-256 identity before exact predicate-map inclusion; advance only if at least one previously live whole owner is eliminated.

Raw-base identity was a predeclared necessary condition for safe syntactic proof reuse. Its failure on every pair, independently reproduced with intact proof replay and mutation controls, closes this mechanism without supporting any mathematical exclusion.

• The four audited fixed-link terminal formulas have a common reconstructed 6,725-variable, 28,552-clause raw base with SHA-256 1a6a0124e4a77d896c92198678671784495dfa1164a5169c862a127c5ca9183f.
• The exact fixed-first profile frontier contains 249 unique owners, of which 248 remain live.
• None of the 996 audited owner/predicate pairs shares an identical raw base; therefore none is eliminated by the declared syntactic dominance rule.
• No 30-block cover or exhaustive exclusion was produced.

• python3 scripts/audit_fixed_first_dominance_v1.py --out-dir artifacts/epoch80-20260811/fixed-first-dominance-v1
• python3 checkers/check_fixed_first_dominance_v1.py --artifact-dir artifacts/epoch80-20260811/fixed-first-dominance-v1 --out artifacts/epoch80-20260811/fixed-first-dominance-v1/independent-check.json
• A complete checker rerun produced byte-identical SHA-256 373619aac4f15f9c4a2fd76c339faf7812fb6daf7ef3da82c87258b4523dce00.
• Fresh lrat-check and CakeLPR builds accepted all four intact proofs and both rejected every final-line deletion.

• .proof-experiments/20260811-081231-a49aeb: primary manifest built in 0.223 seconds; 996 pairs, zero identical bases, zero eliminations.
• .proof-experiments/20260811-081243-1dc7c8: independent audit passed in 12.467 seconds with four dual replays and five rejected mutations.
• .proof-experiments/20260811-081528-fbb27f: complete checker rerun passed and was byte-identical.

checkers/check_fixed_first_dominance_v1.py uses an independent stars-and-bars profile enumeration and token-stream DIMACS parser, compiles lrat-check and CakeLPR once, replays four proofs, tests four truncations, and rejects five semantic mutations.

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

None recorded.

• Exactly 249 necessary fixed-first arithmetic profiles are reconstructed, with 249 unique canonical owners and 248 live owners.
  Independent enumeration of all 278,256 weak six-part compositions. · Simple normalized 30-cover models represented by the hash-bound fixed-first incidence CNF. · computed
• The four terminal fixed-link formulas share one reconstructed raw base distinct from the fixed-first shared formula.
  Four independent prefix reconstructions and SHA-256 comparison. · The audited epoch-72--74 terminal lineage. · computed
• All four retained terminal LRATs remain valid under fresh dual replay.
  lrat-check and CakeLPR accepted every intact proof and rejected every final-line deletion. · The four exact hash-bound local CNFs only. · computed

• Reuse the audited fixed-link terminal LRATs to eliminate whole fixed-first owners solely by raw-base identity and exact-map inclusion.
  All 249 fixed-first owners against four epoch-72--74 terminal predicates. · All 996 candidate pairs have different raw-base hashes. · manifest.json and two byte-identical independent-check receipts · A proved and independently checked semantic translation mapping a fixed-link equality cylinder to an exact union of whole fixed-first owners.
• Launch a ceremonial direct-LRAT owned leaf after this accounting gate.
  The current unchanged proof-production mechanism. · The predeclared gate required at least one newly eliminated live owner and produced zero. · gate_decision REDIRECT in the primary manifest · A material encoding or proof-emission improvement passing its own bounded calibration.

• Double-lex fixed-first incidence symmetry breaking
  Residual columns are already lex sorted, but the remaining S6 x S9 point stabilizer is not globally broken; a double-lex representative exists in every finite row/column orbit. · Compile adjacent row-lex comparators and compare independently audited one-round preprocessing dimensions against the epoch-7 base. · high · open
• Semantic fixed-link-to-profile bridge
  This is the only reopen path for reusing the existing local LRATs across encodings. · State a precise model map and test it on all 249 owners; reject immediately if any cylinder cuts through rather than unions whole owners. · low · open

Objective: Determine whether double-lex point-symmetry breaking materially compresses the proof-oriented fixed-first incidence encoding.

First action: Implement scripts/incidence_doublelex_preprocess_v1.py against artifacts/epoch7-20260808/incidence-matrix-pilot-v1/incidence-matrix.cnf and independently reconstruct its S6 and S9 adjacent row comparators.

Stop condition: Redirect on a double-lex soundness failure, checker disagreement, or less than 5% improvement in both post-preprocessing variables and clauses.

• Implement a double-lex fixed-first incidence compiler that adds row ordering within the S6 and S9 stabilizer cells.
• Independently prove the finite-orbit double-lex existence lemma and reconstruct every comparator.
• Compare one-round pinned CaDiCaL preprocessing against the epoch-7 base and stop below a 5% variable-and-clause reduction.
• Keep the raw-base reuse route closed absent a proved semantic translation.

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

GPT-5.6 Sol acted as principal investigator. GPT-5.6 Terra challenger-prior-art and experiment-verification delegates supplied advisory memos only; Sol independently audited every relied-on claim and promoted provenance into the main workspace. Python 3.12.3 generated and checked manifests. Fresh GCC builds of lrat-check and CakeLPR replayed LRAT proofs. Web search checked the maintained repository and literature status. No CAS, proof assistant, SAT solving, cloud lab, or human validator produced a new mathematical result this epoch.; orchestration: gpt-5.6-sol principal with gpt-5.6-terra delegates.

Duration

1166.9s

Review state

not a result claim

Attempt ID

covering-c1563-20260811-082036-12cad3

No human review recorded.