[an664]

For a full-register restoring XOR word with m > 0 target writes, this proves that the actual image of I XOR projected injects into Fin (2^(m-1)). With no target writes the image is exactly the singleton zero vector. This extends #1598's concrete donor-row certificate to the full Boolean matrix action, preserving arbitrary dirty inputs, target feedback, chronology and repeated donor occurrences.

Only research/target-write-finite-image/ is added. The package includes the unchanged pinned #1598 dependency, the new Lean successor and original proof notes, a dedicated kernel replay, separate finite checks, complete declaration inventories and exact source/replay receipts. The four compilation repairs were supplied by GPT-6 Pro; no theorem statement or definition changed.

Local Lean 4.30.0 (d024af099ca4bf2c86f649261ebf59565dc8c622) replay accepts all 43 successor and 78 predecessor theorem reports. The axiom union is propext, Classical.choice, Quot.sound; no error, sorryAx, custom axiom or incomplete report is accepted. The dedicated wrapper completes in about five seconds locally. Its altered-source and mismatched-approval controls reject before compilation; eight reused report-parser controls pass.

The registered Python hook is separate from kernel acceptance. It passes 297 factorization models, 1,137 full-input evaluations, 511 bit lists, six word fixtures and five semantic controls. Normal and optimized results agree. An independent Pro semantic review reports no material mathematical or statement flaw. Its separately authored checker was authenticated and locally replayed normally and under -O, with identical results: 256 models, 1,024 inputs, 916 preimage choices, six words and ten rejections. The complete written review was recovered, authenticated and read locally; a compact review record and its unchanged checker are included. No human or hosted-CI review is claimed.

Reproduce the finite checks with python3.12 -I -B scripts/research_package.py --package research/target-write-finite-image. Run the dedicated replay.py with an already installed exact Lean compiler as documented in the README. This is an explicit finite-image injection; a conventional rank/dimension API bridge, helper-cycle necessity, helper reduction, BFS, 13-gate optimum and physical supplier consequences remain open or outside this package.

The revision-3 scoped successor claim, historical main/source pins and fresh focused overlap are retained. Credit #1546's written lemma, #1598's coefficient certificate, Gareth Davidson / @bitplane (#1420) and @woklerx (#1105). Andrey Mas with substantial GPT-6 Pro mathematical, Lean and checker assistance through ChatGPT; Codex handled coordination, source authentication, execution audit, local replay and mechanical packaging. Apache-2.0. The selected frontier is unchanged.

[Mister-Meeseeks]

Batch review at 85202a82a3980fdc6454290339219b6a74bf5e50.

Merged to main, preserving the original contributor commits and package attribution.

Reviewed scope: Lean finite-image target-write injection for full-register restoring XOR words, including zero-write case, dirty coordinates and repeated donors. Fresh Lean4.30 replay of all121 axiom reports passes; conventional rank bridge and supplier consequences remain outside scope.

The pinned scoped command passed; the batch ledger contains its command, input hashes, environment and log. This incorporates the research/tooling contribution and does not change the selected κ or discharge the inherited multiplication-theorem assumptions.

Batch review, attribution and evidence. Thank you for the contribution.