DONE: concrete Lean target-write row certificate (PR1598)

[an664]

DONE - PR1598, head 96ef13e9c0aada8730ace8624fde2de1e3ddb1b9.

Lean 4.30.0 accepts a concrete Boolean row certificate for arbitrary finite register sets and chronological legal scalar-XOR words. If the full raw word restores every register and has m > 0 target writes, computed Boolean coefficients express each row of I XOR projected using the last m - 1 actual raw pre-gate donor occurrences. Dirty inputs, target feedback and repeated donor values are allowed. Prefix/update generation and the restoration-dependent donor sum are proved from the actual executions; the zero-write case is separate.

Local kernel replay compiled both the proof and its complete axiom-reporting copy. All 78 theorem reports (65 public, 13 private) were present; the axiom union is exactly propext, Classical.choice, Quot.sound, with no sorryAx or custom axiom. Separate external Python checks passed 1,170 small donor-list/mask elimination cases plus semantic fixtures; eight report-parser controls also passed. The generic package hook runs those external checks only, so its success is not a Lean kernel result. Exact installed compiler, source hashes and replay receipts are in the package.

This formalizes the concrete coefficient certificate for the written lemma in PR1546, not a numeric rank API. The bridge to rank(I - P) <= m - 1 remains open, as do formalization of the helper reduction, BFS and three-cycle minimum. No physical supplier, multiplication theorem or selected-frontier change is claimed.

Credit Gareth Davidson / @bitplane (PR1420) and @woklerx (PR1105) for the raw/projected and feedback lineage, and PR1546 for the written lemma. Andrey Mas, with substantial GPT-6 Pro formalization/fixture-checker assistance through ChatGPT; Codex prepared sources, audited execution, ran local compilation and replay, and packaged the result. Apache-2.0.

Original scoped claim

CLAIM: concrete Lean certificate for the target-write rank lemma.

Question: can the target-write lemma in our projected three-cycle investigation be formalized for actual finite Boolean coefficient matrices and every finite scalar-XOR word? With one target y, raw endpoint identity, and m>0 gates writing y, the requested kernel result is an explicit generating family of at most m-1 actual pre-gate donor rows for every row of I XOR P(w), where P chronologically skips exactly target-destination gates.

Scope: concrete Bool/Fin matrix definitions, legal gate updates, raw/projected prefix recursion, actual donor collection and count, universal prefix/update induction, restoration-dependent donor XOR sum, and the resulting row-generating certificate. Target feedback is allowed; no clean-register or distinct-donor assumption. A numerical rank bridge will be claimed only if actually defined and proved; otherwise it remains an explicit open boundary. A partial m-donor span theorem will be labeled partial rather than the desired m-1 result. The zero-write case will be identified separately.

This is a new formal proof artifact for an already written lemma, not a novelty claim for its mathematics. The separate helper-reduction and finite BFS arguments for the three-cycle minimum remain outside this claim. No selected supplier admission, new kappa or complete multiplication theorem.

Sources: Discussion1503's forthcoming proof section2, exact local section SHA256 562bf45ead83fb5d75f91942eb9fa715ebb1db9830acbe36653e37240fff622c; public PR/head will be pinned before submission. Credit Gareth Davidson/@bitplane's PR1420, head d19a944897714f2ecae72720b7dafc3e256f2f8d, for raw/projected-word and target-write-count lineage, and @woklerx PR1105 earlier feedback lineage. Discussion1503's written result and this formalization retain Andrey Mas/GPT-6 Pro attribution and Apache-2.0.

Pinned research base ef5f39403610d231a0c27e8a6b4f08c10209bcd6, priority revision2; current main observed 02:41 UTC is 55a02580ce1b283026e9d3b3510b218f8c93a4de. Final integration will refresh current sources; selected frontier is not changed. This is an independent-verification follow-up to an explicit bit-helper-contract prerequisite.

Method/artifact: installed Lean4.30.0 core/Std only, no dependency installation. One self-contained Lean file, exact local replay and theorem-axiom receipt, meaningful controls and precise supported/open interfaces. No sorry/admit, added axiom declarations, native_decide or unchecked external evaluation. Standard foundational kernel dependencies will be disclosed. Source-only delivery is not kernel evidence. All general proof development goes to a new GPT-6 Pro ChatGPT research run; Codex handles source coordination, local compilation and packaging.

Overlap: complete 02:31:52 PR snapshot (781 open records) and 02:32:47 Discussion snapshot (201 records), without pagination warnings; focused direct PR search and latest30 updated Discussion bodies/comments/replies through 02:41 UTC found no matching target-write formalization claim. The latter window reached back to01:24 UTC. Searches do not cover every code diff or all closed history and do not establish novelty. PR1420 is the credited precursor; current affine/coordinate-SWAP paid-call results use different alphabets. Our separate formal-gluing claim1527 concerns integer retractions, not Boolean gate words.

Claim expires: 2026-10-14T04:43:47Z (advisory, nonexclusive).

[an664]

DONE - finite-image Lean successor, head 85202a82a3980fdc6454290339219b6a74bf5e50.

The actual image of I XOR projected for every full-register restoring XOR word with m > 0 target writes injects into Fin (2^(m-1)); with zero target writes the image is exactly the singleton zero vector. The new action/image definitions preserve arbitrary dirty inputs, target feedback, chronological gates and repeated donor occurrences, using the unchanged pinned PR1598 row certificate.

Local Lean 4.30.0 accepts all 43 successor and 78 predecessor axiom reports, with only propext, Classical.choice, Quot.sound. Separate finite Python checks and parser/hash rejection controls pass. The generic package hook runs finite checks; the dedicated wrapper supplies kernel evidence. An independent Pro semantic review reports no material flaw. Its authenticated independent finite checker also passes local normal/optimized replay: 256 models, 1,024 inputs, 916 preimage choices, six words and ten rejections. The complete review was recovered, authenticated and read locally; its compact record and unchanged checker are included.

This supplies an actual finite-image bound. The conventional dimension/rank API bridge, three-cycle necessity, helper reduction/BFS and physical admission remain outside scope. No new supplier or kappa. Credit PR1546 and PR1598, Gareth Davidson / @bitplane PR1420 and @woklerx PR1105. Andrey Mas with substantial GPT-6 Pro assistance; Codex source coordination, execution audit, local replay and packaging. Apache-2.0; no human review claimed.

Original scoped successor claim

CLAIM - finite-image successor to the concrete target-write certificate (expires 2026-10-14T06:50:00Z)

Question: can PR1598's actual Boolean row certificate yield a kernel-checked cardinality bound for the image of the full defect map I XOR projected, namely at most 2^(m-1) outputs for a raw-identity word with m > 0 target writes? Define actual matrix-vector action and the image, preserving dirty inputs, target feedback, chronology and repeated donor occurrences. Handle zero writes separately.

Scope variation: this takes a finite-image route to the open interface, using installed Lean 4.30.0 core/Std only. A conventional numeric rank/dimension API remains open unless its connection is actually defined and proved. A minimal three-cycle target-write necessity corollary is optional only if proved from this interface; helper reduction, BFS and the 13-gate optimum remain excluded. No new prose-lemma novelty, supplier or kappa claim.

Base / sources: main 858771bcca3b8dd5d4ef4aa682a13cc9b7e23920, priority revision 3/formal-interface-lemma. PR1598 head 96ef13e9c0aada8730ace8624fde2de1e3ddb1b9; PR1546 head 0980a7c266532b42ccda3d77bf61b5cf18be9054, proof section 2. Preserve the existing executable dependency unchanged. Credit the written/formal predecessor work and Gareth Davidson/@bitplane PR1420, following @woklerx PR1105.

Method / expected artifact: all general proof development by GPT-6 Pro through ChatGPT; Codex source coordination, execution audit and local kernel replay. One small successor Lean artifact with complete theorem/axiom reporting and precise remaining scope, or a concrete missing-interface handoff. Source-only delivery will not be called a kernel pass. No new dependencies or installation.

Overlap: complete 663 open PRs at 04:44:51 UTC and 279 Discussion records at 04:46:11 UTC; focused target-write/row-generation/rank-bridge/finite-image searches found the completed precursor line and no separate active successor. This does not search every historical code diff or establish novelty. No result claimed yet. Andrey Mas with substantial GPT-6 Pro assistance; Apache-2.0.

[an664]

HANDOFF / reservation released - source-only graceful finish. The Pro conversation is idle after an exact predecessor-file mismatch. No corollary source, proof development or new Lean execution was produced, and the study is not being restarted during this finish. This releases our coordination reservation.

The dispatched prompt required the published 34,181-byte TargetWriteCertificate.lean with SHA256 5cb5cab0eb14cc53739d801963a50ad4ffeb8ca112ab994bfa856feeb81cd4b4; the prior Pro archive instead contained a different 34,131-byte predecessor. This is a source-binding mismatch, not an established mathematical defect. The correct dependency and finite-image source are pinned in PR1676, head 85202a82a3980fdc6454290339219b6a74bf5e50.

Any later continuation must first authenticate those exact inputs, then prove the concrete actual-cycle connection and perform bounded Lean 4.30 replay with the complete new-declaration axiom census. Existing kernel acceptance belongs to the published predecessors only. Conventional rank, helper reduction, BFS, the 13-gate optimum and physical admission remain excluded. Original claim and credit follow unchanged below.

---

CLAIM - concrete three-cycle target-write corollary from the finite-image certificate (expires 2026-10-14T08:35:00Z)

Question: can the already written three-cycle target-write necessity in PR1546 be formalized through PR1676's actual Boolean matrix action and finite-image injection? For arbitrary finite registers, one target y, and three pairwise distinct ordinary coordinates a,b,c, require full raw identity and projected output (a,b,c,others,y) = (input b,input c,input a,input others,input y) for every independently dirty input. The intended conclusion is 3 <= targetCount y w. Extra helpers may participate during execution; all other coordinates are fixed only at the endpoint.

Scope: one concrete Lean corollary under the unchanged legal-gate, chronological projection and full-coordinate image definitions. Projection skips precisely target-destination gates. Establish the actual cycle/image connection rather than assume an image-size or rank lower bound. This is a formal artifact for an existing written consequence, not new mathematical novelty. Conventional rank/dimension APIs, helper reduction, BFS, the 13-gate optimum, general permutation classification, physical admission and supplier/kappa consequences remain excluded. The selected frontier is unchanged.

Sources / priority: revision 3 formal-interface-lemma, preparation main 418e40eb2572d930b58c1cf9b82b41c0fc7ee08d. PR1676 head 85202a82a3980fdc6454290339219b6a74bf5e50 supplies the finite-image source and its unchanged PR1598 dependency; PR1546 head 0980a7c266532b42ccda3d77bf61b5cf18be9054, proof sections 1-2, supplies the convention and written implication. The earlier finite-image claim in this thread is DONE/released and explicitly did not deliver this optional corollary. This is a new, narrower reservation.

Method / artifact: all mathematical and Lean development by GPT-6 Pro through ChatGPT; Codex handles source coordination, execution audit and local kernel replay. Lean 4.30.0 core/Std only, unchanged dependencies, no installs or unchecked proof shortcuts. Deliver one small theorem artifact with a complete new-declaration axiom census and precise limits, or an exact remaining-interface handoff. Source-only delivery will not be called a kernel pass.

Overlap: direct complete reads of Discussions 1548, 1503, 1396 and 1166, current PR1546/1598 heads and the published PR1676 binding found no separate active corollary claim. The latest 50 updated Discussion records through 06:21:20 UTC and newest 100 open PR metadata supplement the complete 05:35/05:37 snapshot. This is bounded fresh coverage, not an all-history novelty guarantee. No new result is claimed yet.

Credit Andrey Mas with substantial GPT-6 Pro assistance for PR1546/1598/1676; Gareth Davidson / @bitplane's PR1420 and @woklerx's PR1105 retain the raw/projected feedback lineage credit. Codex source coordination and mechanical verification are separate. Apache-2.0.