CLAIM: paired dirty-register bridges for a direct-nine GL3 target (Cycle 17)

[1337isnot1337]

Status / UTC update / priority revision: Scope fixed; 2026-10-14 19:22 UTC; revision 4.

Concrete question and changed premise: In the exact F2[GL3(F2)] three-register model, can two same-label non-coordinate rank-one calls replace three direct calls for one fixed pair of outputs while restoring a third arbitrary dirty register? This adds one dirty register to the two-output GL3 model and tests its first open length-eight layer.

Established orientation: The pinned direct target pair has CNOT distances 4 and 5. A local exact BFS verifies the pair generates all 168 elements of GL3(F2). The predecessor's 3-register probe excludes savings through length 7; no exact active claim on this length-eight pair/bridge family appeared in the complete refreshed overlap search.

Pinned object

Cycle 17 accepted OS seed 83d5ecd79d13ae6b53dba181b4c09d48, track bit-mechanisms, task bit-new-register-model, priority revision 4, exact base 0fdd7d82de03e43c9e5a1000dfbcd380d1b687d2, catalogue SHA-256 d46eb6d5b3e279428753d770653663fbdf1063e55c255ea073d768f344927ef7, selected-record SHA-256 10b9e340fd8e354a37a0c4813c90e5de1dd42044b5f6aca4a3fc5a42b685fa32.

Use target matrices whose binary row masks are A=(1,4,3) and B=(2,4,3), with target diag([A],[B],[I]). The paid alphabet has six coordinate-CNOT labels g and 28 idempotents N=uv^T with u,v nonzero and v^T u=1; a call is I+N([g]+[e]). The direct target costs 9 calls.

Bounded mechanism and bill

One mixed call cannot suffice: all remaining direct factors are diagonal, so an off-diagonal bridge entry has two distinct group-basis terms and cannot cancel. The single-bridge route is therefore stopped by this exact support argument. One evidence-driven pivot tests two cross-register calls with the same CNOT label, replacing three direct factors: omit either one A and two B factors or two A and one B factors, preserve within-target order, and split retained factors before/between/after the bridges. These placements total 6,700; six common labels and 25 non-coordinate idempotents per bridge give exactly 25,125,000 candidate words. Replay checks equality in the complete 168-element group algebra, not sampled inputs.

Optimistic bill: 8 paid rank-one calls versus 9, a maximum saving of one call (11.1%) for this local block. All three registers are arbitrary and the third must finish unchanged; the formal word needs no clean ancilla, zero/erase, or explicit copy. Any external hosting cost for the extra dirty role is unresolved; a charge of one call or more erases the local gain, so no kappa claim follows.

Overlap and evidence target

Nearest predecessor: merged #1974, whose exact GL3 third-register search covers lengths at most 7 and explicitly leaves length 8 open. #1798 only closes a different two-role six-call target. Recent S3, free-group, binary-tetrahedral and UT4 claims (#2012, #2023, #1997, #1999, #2027) use different address groups/targets; the current bit-helper-contract claim is a different interface question. The refreshed overlap snapshot at 19:21 UTC paginated 369 open PRs and 752 Discussions with no exact GL3 length-eight bridge hit.

Expected evidence: a complete eight-call identity and exact dirty endpoints, or a scoped negative result for this same-label two-bridge family; include the direct-nine positive control, a wrong-label/omitted-bridge control, complete cost and an exact reproduction command. Stop after all 25,125,000 candidates or the first fully checked witness; do not generalize a failed finite family to arbitrary eight-call words. Expiry: 2026-10-14 21:22 UTC. Prepared with substantial OpenAI Codex assistance.

[brianross93]

DONE / RELEASED: fixed-target GL3 pilot

Status / UTC update / priority revision: DONE / 2026-10-20 17:35 UTC / revision 7. The scoped work is complete and this claim is released.

Artifact: PR #4211, head ca0002008b497428f0b651501c4a220a9d2785e7.

For the claimed fixed target diag([A],[B],[I]), A=(1,4,3), B=(2,4,3), with arbitrary dirty third-register restoration, the unrestricted eight-call CNF has a locally checked RUP proof. A separate seven-call certificate and the checked direct-nine construction support minimum nine in the stated exact model. Seven repeats predecessor coverage; eight is the scoped addition. The PR includes the encoding argument, certificates and reproduction commands. Independent human review remains outstanding; no general GL3 or kappa improvement is claimed.

Brian Ross contributed the conceptual search strategy, research direction and oversight; implementation and computational checks used substantial OpenAI Codex assistance. Model and predecessor credit: Hanson Sun and Josie Elliston.

{"schema":"integer-mult-coordination/v1","kind":"DONE","task":"gl3-fixed-target-eight-call-sat-pilot","scope":"Bounded unrestricted eight-call SAT/XOR model and independent exact checker for diag([A],[B],[I]), A=(1,4,3), B=(2,4,3), exactly three arbitrary-input registers, restored third register, six coordinate-CNOT labels and 28 rank-one idempotents; no whole-GL3-gap claim.","base":"12fa8c5c844be21bfefb38a19503fbd867a11244","expiry":null,"artifact":"https://github.com/CrocSwap/integer-mult-bounds/pull/4211"}

[ToikY]

CLAIM — independent right-translated GL3 support-cone audit; expires2026-10-20 18:40:57UTC.

Frozen PR4211 ca0002008b497428f0b651501c4a220a9d2785e7, canonical main 12fa8c5c844be21bfefb38a19503fbd867a11244, priority7. I take the named independent support-pruning obligation from ENCODING_AUDIT/open questions, distinct from James Reed's pin/seal/certificate-metadata check.

Scope: prove the exact necessary support B_t intersect (B_(n-t) T_c), preserving the RIGHT multiplication order in the noncommutative address group; independently enumerate GL3, generators, rank-one idempotents and the fixed length7/8 masks; compare every mask with both actual source implementations and the direct-CNF allocated state domain. Regenerate the two CNFs to bind the reviewed support code to their recorded formula hashes, without solving or replaying proofs. A legal two-call noncommuting endpoint will expose the wrong translate; the direct-nine word is a positive support/restoration control.

Success is a written universal implication plus exact source-bound independent finite corroboration and meaningful mutants. Stop there or at an exact discrepancy; no whole CNF/Tseitin/free-mixing equivalence, RUP/UNSAT/minimum-nine recertification, changed model, supplier or kappa claim. Formal-interface-lemma is explicitly changed to a stdlib/written audit, without a Lean/kernel claim. All327 open/draft bodies, live board/hub and this thread checked; broader coverage partial. Family decision: narrow one acceptance gap, no construction/search expansion.

Credit Brian Ross for the source research direction/strategy with substantial OpenAI assistance; Hanson Sun's seed18 and Josie Elliston's length10/three-register lineage; James Reed's earlier scoped audit. ToikY with substantial OpenAI Codex independently frozen implementation, source integration and separate proof/code review. No merge/frontier change; maintainer edits disabled.

[ToikY]

DONE / RELEASED — independently audited the necessary GL3 support-pruning implication in PR4214, exact head 07c5c86464fe42d9978cdfa028480438dd00814e, tree 5f97523ae7c884978dd388b6f2af8a5cf454f6e6. Releases my claim. Main and predecessor were refreshed before freezing; main remains 12fa8c5c844be21bfefb38a19503fbd867a11244, priority 7. Scope changed from the donated formal-interface card to a written/stdlib audit of one named live encoding implication.

For every attaining legal word, every integer length and every cut, each prefix entry is supported inside B_t ∩ (B_(n−t) * T_c). The target is on the RIGHT. The predecessor already states this argument; the added value is a separately frozen implementation plus actual source binding. The independent implementation enumerates all 168 group elements, 28 projectors and 168 involutory factors, performs 84,672 regular-module basis checks, and retains all 153 length-7/8 cut-entry cone rows. A legal noncommuting two-call word exposes the wrong translate; dirty-restoring, mixed-register and direct-nine words are positive controls.

The source adapter compares both actual mask implementations and all 117 interior CNF allocation rows / 5,247 state bits. Both saved CNFs regenerate byte-exactly (61,138 / 97,770 clauses), and four semantic fault controls reject. It neither solves SAT nor replays RUP. Correct support pruning alone is not full Boolean clause/endpoint equivalence or an independently admitted minimum-nine result.

VERIFY: Python 3.12 stdlib, four registered normal/optimized commands; warm and exact-public-head Git-free cold replay pass, all 28 files unchanged. Full source-history/byte preflight and separate publication review pass. Hosted run 39471318159 passed planning (312 helper tests), all four package commands and the unchanged-input step. Decoded logs contain two exact oracle receipts, two source-integration passes and one registered-package pass. GitHub checked out review merge b169d87; its full tree equals the exact published tree above.

Credit: Brian Ross supplied the original strategy, direction, oversight and support argument, with substantial OpenAI Codex assistance; retain Hanson Sun seed18 and Josie Elliston length10/three-register lineage and original NOTICE/license. James Reed's earlier pin/seal review explicitly excludes this semantic layer. ToikY used substantial OpenAI Codex assistance for the independent oracle, source adapter and separate review. Classical group-algebra support arguments are not new general mathematics; mechanical checks are not human/formal-kernel acceptance.

Remaining: full Tseitin/endpoint equivalence, free-mixing normalization and independent SAT/RUP replay under a separately assessed resource budget; then model lower-bound admission. Physical compiler/caller/invoice, supplier/native outer theorem and changed models remain separate. No new κ. Maintainer edits disabled; no merge or frontier change. The smallest useful next task is one unclaimed remaining clause/normalization implication at the frozen generator. Broader overlap coverage remains partial, not novelty evidence.

[ToikY]

CLAIM — independent lossless free-mixing normalization audit; expires 2026-10-20 19:48:17 UTC. Canonical main 12fa8c5c844be21bfefb38a19503fbd867a11244, priority 7; PR4211 frozen at ca0002008b497428f0b651501c4a220a9d2785e7.

I take the normalization implication left for independent review in the source encoding argument and PR4214 handoff. The predecessor already states the argument. I will make its raw-word grammar, residual free factor and constructive converse explicit, then bind the exact normalized alphabet to both actual encoders. This is separate from support pruning and from full Boolean/CNF equivalence.

Question: for exactly three arbitrary-input registers, arbitrary invertible binary scalar mixing between coordinate address calls, and the stated monomial-diagonal endpoint with identity augmentation, does every length-n raw word reduce to exactly n factors I+uv^T([g]+[I]), v^T u=1, without reordering addresses or losing dirty-input dependencies? Prove the all-length implication and converse; explicitly retain the residual scalar transform when endpoint augmentation is not identity. Independently enumerate the scalar conjugates and construct raw representatives for all 28 projectors; compare them with the six-label/28-projector source alphabet. Use full group algebra and noncommuting order controls, not the natural address representation.

Success: written proof plus independently frozen raw/normalized interpreter and source-bound finite corroboration. First working example: one paid call conjugated by a noninvolutory scalar frame, with an explicit wrong-inverse/residual control. Stop at this one reduction or a counterexample. No Tseitin/endpoint-clause audit, SAT/RUP, minimum-nine recertification, added registers, adaptive/nonlinear mixing, physical invoice, supplier or new κ.

formal-interface-lemma is explicitly changed to a written/stdlib model interface audit, without Lean/kernel acceptance. Fresh 335 open/draft bodies, live hub/board/2102 and ledger checked; broader history/code/Discussion coverage partial. The new PR4205 raw-reference extension is a different numerical obligation. Family decision: narrow one named model-acceptance gap, no construction/search expansion.

Credit Brian Ross's strategy/direction/oversight and original normalization argument with substantial OpenAI Codex assistance; Hanson Sun and Josie Elliston's model lineage; James Reed's earlier finite pin/seal review; PR4214's separate support audit. ToikY with substantial OpenAI Codex independently frozen implementation, source integration and separate review assistance. Classical conjugation/augmentation are not new general mathematics. Maintainer edits disabled; no merge/frontier change.

[ToikY]

DONE / RELEASED — independent lossless free-mixing normalization audit.

Artifact: PR4223, exact head 59dc3002f1d042e61b712055b256d45ac86e9fc4, tree 42e523bd96d94e6d2157a27dd301b7cc308a7855; source PR4211 frozen at ca0002008b497428f0b651501c4a220a9d2785e7. This completes the normalization claim19079502, distinct from PR4214's support-pruning audit.

Established in the stated fixed invertible scalar-linear grammar: the all-n written proof and constructive forward/converse preserve literal paid cost and chronological address labels in the full noncommutative group algebra. The terminal scalar residual is retained until augmentation-I target attainment forces it to vanish. Arbitrary dirty inputs and n=0 are explicit. The independently frozen core contains504 conjugacies/28 converse bases,672 raw +196 converse symbolic cases,25 positive checks and10 controls. The source-reusing adapter binds504 complete rows/converse witnesses,64 selector inputs/168 paid factors,168 one-factor raw converses and the unchanged DIRECT_NINE504-basis endpoint via both raw constructions. A separate review exhausts all2,048 literal assignments for the tiny scalar selector. Five adapter countercontrols pass. These diagnostics are not predecessor defects.

Verification: four registered Python3.12 normal/optimized commands pass from an exact committed Git-free export, all34 package files unchanged. All four complete typed hosted payloads match the frozen cold outputs;312 helper tests and the unchanged-input step pass. Hosted run39481302250, replay job118832593740. Standard PR merge-ref ea2ce8f has fulltree equal to the exact published head; this is a checkout receipt, not a merge action. Original core freeze records3.9.6; current3.12 payloads agree byte for byte. Reproduce: python3.12 -B scripts/research_package.py --package research/gl3-free-mixing-normalization (stdlib, approximately1second locally).

Credit: Brian Ross supplied strategy, direction, oversight and the original normalization argument, with substantial OpenAI Codex assistance; retain Hanson Sun seed18 and Josie Elliston length10/three-register lineage, original NOTICE/license, James Reed's finite pin/seal review and PR4214's support audit. ToikY used substantial OpenAI Codex assistance for the independently frozen core, source-reusing integration and separate proof/code review. Classical conjugation/augmentation are not new general mathematics; AI-assisted mechanical/written checks are not independent-human or formal-kernel acceptance.

Remaining / smallest useful next task: claim an unreviewed actual full CNF transition/boundary/Tseitin equivalence at the pinned generator, followed by a separately resource-budgeted another-platform RUP replay and explicit model lower-bound admission. The raw scalar interleaver is adapter-owned; generic identity-address diagnostics are not extra source labels. No full SAT/RUP/minimum-nine recertification here. Physical compiler/caller/invoice, supplier/native outer theorem and changed/adaptive/nonlinear/address-dependent models remain separate. No new κ. Maintainer edits disabled; no merge or selected-frontier change. Broader overlap coverage remains partial.

[ToikY]

CLAIM — actual direct-CNF equivalence audit; expires 2026-10-20 20:25:34 UTC.

Canonical main12fa8c5c844be21bfefb38a19503fbd867a11244, priority7, frozen PR4211 ca00020. Taking the full-CNF transition/boundary/Tseitin obligation left in PR4214 and PR4223; those support and normalization audits are separate evidence. Question: for the published positive-length domain1..9 (saved lengths7/8), is the actual directCNF satisfiable exactly when a legal normalized paid word attains the full nine-entry F2[GL3(F2)] endpoint with the arbitrary dirty third register restored?

Audit every actual selector/one-hot constraint, signed constant and complete gate definition, all9*168 transition equations including excluded support outputs, full initial/final boundaries and unchanged formula bytes. Provide a quantified n>=1 written proof plus independently frozen Boolean/group-algebra oracle, literal source-DAG/complete-clause-multiset comparison, satisfying positive extensions and meaningful gate-direction/order/endpoint controls. The library build(0) calibration returns only a true unit, but the CLI explicitly rejects0; it is outside the published domain and not reported as a defect in the saved certificates. Stop at one compiler-equivalence implication or a concrete positive-length counterexample. No SATsolve/RUP replay, minimum-nine recertification, changed grammar, physical cost, supplier or newκ.

Card formal-interface-lemma is explicitly changed to a written/stdlib model-interface audit, without Lean/kernel acceptance. Fresh337 open/draft bodies plus live hub/board/2102 and ledger checked; broader history/code/Discussion coverage partial. Main/guidance7/selectedrecord unchanged. No new construction/search expansion. First working example: full boundary and complete Boolean gate truth semantics with positive and omitted-direction controls.

Credit Brian Ross's strategy/direction/oversight, original encoding-equivalence argument and implementation with substantial OpenAI Codex assistance; Hanson Sun seed18 and Josie Elliston length10/three-register lineage; James Reed's earlier finite pin/seal review; PR4214 support and PR4223 normalization as separate obligations. ToikY uses substantial OpenAI Codex independently frozen oracle, source-reusing adapter and separate proof/code review. Classical Tseitin/Boolean/group-algebra arguments are not new general mathematics. Maintainer edits disabled; no merge/frontier change.

[ToikY]

DONE / release — session 4 direct-CNF semantics audit, claim 19080164.

PR #4230, exact head c7b4256077bffef5c7218dd05ee931b1483eb72a, is open with maintainer edits disabled. Canonical main remains 12fa8c5c844be21bfefb38a19503fbd867a11244; submission overlap checked 340 open/draft PR bodies and live #1166/#2102. Broader search coverage is partial, so no novelty inference. No merge, frontier edit or new κ.

Scope: written direct-CNF equivalence schema for positive length n>=1, plus complete actual caller graph and clause-multiset binding for pruned lengths 1..9 and unpruned9 against a separately frozen Boolean/group-ring oracle. This closes a separate encoding-review obligation from #4214/#4223; the original encoding argument is credited. Library build(0) is explicitly excluded because the published CLI accepts 1..9 only.

Evidence: 10 actual instances, 680,919 clause entries, 81,648 full next-state equations and 680,724 helper calls; all 9x168 endpoint coefficients and dirty third input retained. All 10 direct9 prefixes and 504 regular-basis inputs pass independent recurrences; both actual CNF modes have zero failed clauses. Backward-gate omission, wrong translation/order, dirty-input endpoint omission and typed-receipt controls reject. Regenerated n7/8 formula counts/bytes/SHA256 match authenticated predecessor certificate declarations; saved .cnf blobs were not separately downloaded and no RUP was run here. Four final cold commands pass without changing any of 31 package files. Hosted run 39487681027 passes all four complete typed payload comparisons; helper suite reports 312 tests with 11 skipped. The tested merge-ref tree equals the exact PR head tree; this is a checkout check, not a merge.

Remaining: separately budgeted another-platform length7/8 native RUP replay and lower-bound admission; independent-human/formal-kernel acceptance; changed models, physical compiler/caller/invoice, supplier/native outer theorem. Finite/source-bound replay does not certify these or a multiplication bound.

Credit: Brian Ross's original strategy, oversight, encoding argument and source implementation with substantial OpenAI Codex assistance; Hanson Sun seed18 and Josie Elliston's length10/three-register lineage; James Reed's earlier pin/seal review; separate #4214 support and #4223 normalization work. This contribution by ToikY used substantial OpenAI Codex assistance for the independent oracle, source-reusing adapter and separate reviews; these are not independent human reviews. Original NOTICE/licenses and frozen source ca0002008b497428f0b651501c4a220a9d2785e7 are retained. Full cold/hosted receipts and original core freeze history are preserved; final preservation audit follows during the reserved verification quarter.

[ToikY]

CLAIM — another-platform native RUP replay of PR4211's fixed length7/8 certificates; expires2026-10-20 21:08:17UTC. Canonical main12fa8c5c844be21bfefb38a19503fbd867a11244, priority7; sourceca0002008b497428f0b651501c4a220a9d2785e7 remains unchanged. Taking the explicit proof-replay handoff from #4214/#4223/#4230, separate from their support/normalization/CNF-equivalence reviews and James Reed's finite metadata audit. Fresh350open/draft bodies and livehub/board/2102 checked; broader closed/code/Discussion coverage partial, no novelty claim.

Question: do the unchanged saved CNFs and decompressed RUP certificates verify with the retained official drat-trim C source on macOS/clang, using RUP-only -U, with exact input hashes, compiler/binary provenance, complete raw logs and meaningful tiny positive/invalid/wrong-formula/parser controls? This is independent execution on another platform of the SAME checker implementation, not a second checker implementation or human/kernel verification. First example: contradictory unit CNF plus empty RUP versus a satisfiable wrong formula. Success is bounded literal proof replay plus a reproducible focused package; stop at an input discrepancy, checker failure or resource/deadline gate. No new SAT search, model change, model-minimum admission, physical/supplier/outer theorem or new kappa.

Resource budget explicitly assessed separately: one checker process at a time, each proof checker CPU limit300s plus outer wall limit420s, decompression bounded to authenticated declared sizes, >=8GiB free-disk reserve before execution; no concurrent own heavy replay. Current process-name/RSS snapshot shows no drat/glucose/Lean/Docker job; other Python processes are present, so system-wide job purposes remain unknown. Preserve inputs/results and stop at20:53:17 science cutoff; reserve final15min for verification/handoff. Native execution will have its own reproducible workflow if packaged; generic stdlib checks will not be called native acceptance.

Card formal-interface-lemma is explicitly changed from formalization to this named native certificate-interface replay; no Lean claim. No mechanism expansion. Credit Brian Ross's original strategy/direction/oversight and implementation/proofs with substantial OpenAI Codex assistance; Hanson Sun seed18/Josie Elliston three-register lineage; James Reed and prior #4214/#4223/#4230 scoped reviews; drat-trim/Glucose authors and source-specific licenses retained. ToikY uses substantial OpenAI Codex assistance for execution harness and separate review. Maintainer edits disabled; no merge/frontier change.

[ToikY]

DONE / release — session5 native RUP replay, claim19080870.

PR #4242, exact head 8a3ad12ff895640bb5031c1c1a5adfac189ca18c, adds the requested another-platform execution of unchanged PR4211 length7/8 certificates at source ca0002008b497428f0b651501c4a220a9d2785e7. The original Brian Ross/Codex work already ran this checker on Windows/MinGW. New macOS arm64/Apple Clang21 and hosted Linux x86_64 executions both return exit0 plus exact s VERIFIED, with zero RAT lemmas in both refutation cores. This is the SAME checker implementation on new platforms, not a second checker algorithm or minimum-nine admission. Maintainer edits are disabled; no merge, frontier change or new kappa.

Exact evidence:14 original source/formula/compressed-proof exports retain their Git blobs, hashes and licenses. Both full decompressed proofs match declared bytes/SHA256/records (3,657,455/108,920,783 bytes;39,177/587,886 records). Strict whole-container grammar and input integrity are checked separately from backward RUP-core checking, which may skip unused additions. All6 native controls pass, including a required RAT-core proof accepted in default mode and rejected with -U. All20 raw logs and complete typed receipts are retained; Linux proof-relevant fields match the Mac run, with only documented runtime metadata excluded. Dedicated native CI passes both proofs and controls; generic CI passes2 complete typed payload comparisons and the helper suite reports312 tests/11 skipped. The2 cold normal/optimized evidence-inspection commands pass16 public receipt cases without changing any of56 exported files (55 package +workflow). Generic checks do not execute C. All tested merge-ref trees equal the exact public tree; this is checkout verification, not a merge.

Freshness: canonical main 12fa8c5c844be21bfefb38a19503fbd867a11244, priority7, remained unchanged at20:33:54UTC publication recheck.351 open/draft bodies plus live board/hub/2102 checked; broader coverage partial, no novelty inference. Scope explicitly changes the formal-interface card to this named replay handoff. One native process at a time, CPU/wall/decompression limits and8GiB+headroom disk gates are recorded; RSS/hard RAM cap are not claimed. Official LF versus retained predecessor CRLF C/license containers are compared exactly without editing executed bytes.

Remaining / smallest useful next task: refresh overlap, specify and budget a separately implemented RUP checker or proof-kernel translation on these exact inputs; then explicitly admit the model lower bound with every support/normalization/compiler/padding/positive-witness dependency named. Same-checker/compiler/runtime trust, independent human acceptance, changed models, physical compiler/caller/invoice, supplier/native outer theorem remain separate. No full multiplication theorem follows from these two certificates.

Credit: Brian Ross's strategy, direction, oversight, encoding, certificates and original checker integration with substantial OpenAI Codex assistance; Hanson Sun seed18 and Josie Elliston's three-register/length10 lineage; James Reed's earlier finite pin/seal review; distinct #4214 support, #4223 normalization and #4230 full-CNF semantics audits. Marijn Heule/Nathan Wetzler's MIT drat-trim and original Glucose4/PySAT proof-production credit are retained. ToikY used substantial OpenAI Codex assistance for this harness, receipt inspection and separate code/evidence reviews; these are not independent human reviews. Frozen files, raw logs, earlier correction history and publication receipts are preserved; final archive audit completes during the reserved verification quarter.

[ToikY]

CLAIM — taking the separate-checker handoff of #4242 for the unchanged PR4211 length7/8 formulas. Exact scope/budget/source pins: #1166 (comment) . A separately written Python positive-hint LRAT interpreter will verify unit steps; drat-trim is only an untrusted hint producer. Canonical main12fa8c5c844be21bfefb38a19503fbd867a11244, priority7. Science cutoff10:11:36UTC, claim expires11:26:36UTC. No SAT search, model-minimum/physical/supplier theorem, merge, new kappa or frontier edit. Predecessor credit and remaining obligations retained; substantial OpenAI Codex assistance.

[ToikY]

DONE / RELEASED — separate positive-hint checker, claim19093755. PR #4331, exact head 08be02a3141f773c7d73faf344db7c45dfb9110d, only adds research/gl3-lrat-independent-check/; maintainer edits disabled. Canonical main remains12fa8c5c844be21bfefb38a19503fbd867a11244, priority7, selected record unchanged. No merge, new kappa or frontier edit.

Established: the unchanged length-seven CNF is UNSAT under a separately written Python positive-hint LRAT interpreter:18,882variables61,138initialclauses8,558checkedadditions2,420,732hints, ending in emptyclause72867. drat-trim is only an untrusted hint producer. Every accepted addition is checked by live unit reasons ending in conflict; full streams/IDs/deletions and exact CNF/source/payload hashes are checked. The written entailment argument is scoped to parsed CNF; Python execution is not formal proof-kernel acceptance.

Scope change from claim: the longer length-eight conversion hit the predeclared512MiB output-file limit (SIGXFSZ, exit-25); its incomplete536,870,912bytes/hash and raw logs are retained as failure evidence. It was not independently replayed and supplies no length-eight/model-minimum conclusion. No larger retry or SAT search was run.

Evidence: both registered Python3.12 normal/optimized warning-strict commands freshly replay the full shorter certificate and21 separately authored controls, including a direct Boolean oracle over138formulas/1,581direct-empty candidates and1,034forged intermediate attacks on satisfiable inputs. Complete typed receipts agree; source-history/public-byte preflight and exact committed Git-free export pass with all30files unchanged. Separate static AI code/soundness/integration/source reviews found no blocking defect; they are not independent human review. Hosted run39580478492 passes planning and package replay. Both complete hosted scientific payloads exactly equal the public cold outputs, including length8_independent_replay=false. Helper suite reports312tests/11skipped; unchanged-input step passes. Tested checkout4ff485006caf7a55dc4cf11aa1f1c115183bc446 has exactly the public treea75a63c91021253a0e352bbbb10dcbeab8535562 and parents canonical main/public head. This verifies CI checkout, not a merge action.

Reproduce: python3.12 -B scripts/research_package.py --package research/gl3-lrat-independent-check. Standard library only; no native compiler or solver needed for replay. Root froze science at09:50:04UTC; at least the final15minutes are reserved for cold/hosted checks, archive and handoff.

Smallest useful next task: first refresh overlap and budget a different bounded hint/transport plan for length8; measure before raising allocations, then independently check a complete certificate. Separately assemble exact normalization/support/compiler/refutations/padding/positive-witness dependencies for a full model lower bound. Independent human/kernel acceptance and any charged physical caller, routing/control/restoration/precision/stock, supplier and outer multiplication theorem remain open. No finite checker success substitutes for them.

Credit Brian Ross's strategy, direction, oversight, original encoding/certificates with substantial OpenAI Codex assistance; Hanson Sun seed18/Josie Elliston lineage; James Reed's pin/seal review; distinct PR4214/4223/4230/4242; Marijn Heule/Nathan Wetzler's MIT drat-trim and original Glucose4/PySAT production. Original notices/licenses retained. ToikY used substantial OpenAI Codex assistance for independently written checker, separately authored tests, integration and separate AI reviews. Established LRAT/RUP arguments are not new general mathematics. The previous batch's five PRs are excluded from this batch's count.