Node 4: close C4's code-deposit half by running the pinned init images under Ξ

[Th0rgal]

Stacked on #18. Base is main (same as #18), but #18 is not merged, so
the diff below includes its commits. Review only the top commit bf4a16c —
that is the entire Node 4 change. Do not merge this before #18.

What this strengthens

The registered parent P-CONTROL-1 (pcontrol1_forall_parent) — no new parent ID.
P-SUBMIT-1 and P-DRAIN-1 registered parents are unchanged.

C4 previously stopped at a CFG prefix. Ctor.lean's opcode facts are rfl on the
first ++ chunk of each init hex — 32 of 638 bytes for deposit, 64 of 503
for exit — and never execute the image. Three things were unchecked:

1. that the init image reaches its RETURN at all;
2. that the buffer it returns is the pinned runtime byte for byte, rather than
   merely a copy starting at a plausible offset;
3. that the exit ctor's SSTORE actually lands, as opposed to being present as
   an opcode 34 bytes in.

Eip8282/Audit/Guarantees/PControl1/CtorXi.lean executes the full pinned
638-byte deposit and 503-byte exit init images under EvmYul.EVM.Ξ and compares
the returned buffer — the value Λ's step (115) installs as the new account's
code — against the pinned runtime images, with the exit ctor leaving slot 0 at
INHIBITOR and slots 1–3 zero.

pcontrol1_ctor_xi_parent is added as a conjunct of pcontrol1_c4_ctor_forall,
so the registered parent is strictly stronger.

This is what ties pinned/bytecode/*/ctor.hex to pinned/bytecode/*/main.hex.
audit/artifacts.lock.json hashes the two files independently, so until this
theorem nothing in the repo ruled out a ctor that deploys something other than the
runtime every other guarantee is proved about.

Why this is not Λ / a CREATE trace

Deliberate. Λ derives its target address as KEC(RLP(sender, nonce)), and the
EIP-8282 contracts are genesis predeploys at 0x0000bFF4… / 0x000064D6…,
not CREATE outputs. Driving Λ here would pin an address that is provably not
the predeploy address, and would pull the opaque @[extern] keccak FFI into the
trusted base for no gain. The bytes an init image actually executes are its
preamble — 10 bytes for deposit, 45 for exit; everything after is the runtime
carried as CODECOPY data — and neither preamble contains SHA3, CREATE, a
call, or precompile dispatch, so A-NATIVE-DECIDE is disclosed exactly as Ctor
and Wave-1 already state it.

A-PINNED-SOURCE: still OPEN

Recorded honestly in audit/assumptions.yaml — no conjunct was invented. This
links ctor.hex to main.hex inside the pin; it observes nothing on chain.
Within the pin the two bytecode files are no longer independent, so
keccak(deployed code) is determined by ctor.hex. What remains assumed is that
these files are the images actually at the two predeploy addresses. The
removal_path is now a single observation: read the live codehash at those
addresses and check it against keccak of the pinned main.hex.

Kill-line

Cut on the init images rather than the runtimes — bytes no runtime trace can
reach, because the init code is not the deployed code:

image	offset	mutation	effect
deposit ctor	5	CODECOPY src 0x0a → 0x0b	deployed copy shifted one byte
exit ctor	34	SSTORE 0x55 → POP 0x50	exit contract un-inhibited at genesis

ctor_mutant_refutes_parent feeds each to the same ctorXiFacts the parent
contains. ctor_mutants_are_independent shows each cut refutes only its own half.
ctor_mutants_leave_runtime_guarantees_intact proves both cuts leave
controlFacts and PSubmit1.submitFacts true on the pinned runtimes — so the
new conjunct is load-bearing on bytes nothing else in this repository constrained,
not a restatement of a sibling.

The pre-existing one-byte runtime kill-lines still refute the parent, unchanged.

Files changed (top commit only)

• Eip8282/Audit/Guarantees/PControl1/CtorXi.lean (new)
• Eip8282/Audit/Guarantees/PControl1.lean — C4 conjunct
• Eip8282/Tests/PControl1Mutant.lean — C4 kill-line
• Eip8282/Audit/Trust.lean — #print axioms for the new theorems
• Eip8282.lean — import
• audit/guarantees.yaml, audit/assumptions.yaml, README.md

No sorry, no project axiom.