diff --git a/Eip8282.lean b/Eip8282.lean
index 1e997a0..3974e8a 100644
--- a/Eip8282.lean
+++ b/Eip8282.lean
@@ -15,6 +15,7 @@ import Eip8282.Audit.Guarantees.PControl1.Gate
 import Eip8282.Audit.Guarantees.PControl1.Excess
 import Eip8282.Audit.Guarantees.PControl1.Count
 import Eip8282.Audit.Guarantees.PControl1.Ctor
+import Eip8282.Audit.Guarantees.PControl1.CtorXi
 import Eip8282.Audit.Reachable
 import Eip8282.Audit.AllGuarantees
 import Eip8282.Audit.XiTransport
diff --git a/Eip8282/Audit/Guarantees/PControl1.lean b/Eip8282/Audit/Guarantees/PControl1.lean
index 1bd429a..7ae29d0 100644
--- a/Eip8282/Audit/Guarantees/PControl1.lean
+++ b/Eip8282/Audit/Guarantees/PControl1.lean
@@ -5,6 +5,7 @@ import Eip8282.Audit.Guarantees.PControl1.Gate
 import Eip8282.Audit.Guarantees.PControl1.Excess
 import Eip8282.Audit.Guarantees.PControl1.Count
 import Eip8282.Audit.Guarantees.PControl1.Ctor
+import Eip8282.Audit.Guarantees.PControl1.CtorXi
 import Eip8282.Audit.Reachable
 
 namespace Eip8282.Audit.Guarantees.PControl1
@@ -701,11 +702,22 @@ def pcontrol1_c3_count_forall :=
     (@Count.system_count_reset)
 
 /-- C4: exit init stores `INHIBITOR` at slot 0 then returns runtime;
-deposit init does not `SSTORE`. Closes `initial_gating` on bytes. -/
+deposit init does not `SSTORE`. Closes `initial_gating` on bytes.
+
+The trailing conjunct is the code-deposit half. `Ctor`'s three facts are
+`rfl` on the first `++` chunk of each init hex — 32 of 638 bytes for
+deposit, 64 of 503 for exit — and never run the image.
+`CtorXi.pcontrol1_ctor_xi_parent` executes the *full* pinned init images
+under `EvmYul.EVM.Ξ` and pins the buffer each one returns to be
+`depositRuntime` / `exitRuntime` byte for byte, which is the `code` that
+`Λ`'s step (115) installs. That is the only thing in this repository
+connecting `pinned/bytecode/*/ctor.hex` to `pinned/bytecode/*/main.hex`;
+`audit/artifacts.lock.json` hashes them independently. -/
 def pcontrol1_c4_ctor_forall :=
   And.intro Ctor.initial_gating_bytes <|
-  And.intro (@Ctor.exit_ctor_stores_inhibitor)
-    (@Ctor.deposit_ctor_storage_zero)
+  And.intro (@Ctor.exit_ctor_stores_inhibitor) <|
+  And.intro (@Ctor.deposit_ctor_storage_zero)
+    CtorXi.pcontrol1_ctor_xi_parent
 
 /-- R5 constructor roots and preservation of the four control words across
 the two modelled calls. `EndpointAgrees` remains required to connect these
@@ -760,9 +772,19 @@ The leading conjunct pins what the CFG layer stepped against: the jumpdest
 tables the C1/C2/C3 runtime lemmas step against are the tables
 `EvmYul.EVM.Ξ` itself derives from the pinned runtime image, kernel-checked by
 `decide +kernel` (EVMYulLean 0ff72b2), not hand-written arrays that happen to
-look right. C4 is a no-jump init preamble and steps against no table, so the
-two init-image equalities in that conjunct stand on their own; they do not
-transport into or constrain `pcontrol1_c4_ctor_forall`.
+look right. C4's CFG half is a no-jump init preamble and steps against no
+table, so the two init-image equalities in that conjunct stand on their own;
+they do not transport into or constrain `pcontrol1_c4_ctor_forall`.
+
+C4's code-deposit conjunct is cut separately, on the **init** images rather
+than the runtimes: `Eip8282.Tests.PControl1Mutant.ctor_mutant_refutes_parent`
+flips the deposit `CODECOPY` source operand at ctor byte 5 (`0x0a` → `0x0b`)
+and the exit `SSTORE` at ctor byte 34 (`0x55` → `0x50`), and shows
+`CtorXi.ctorXiFacts` is `false` on each. Those bytes are unreachable from
+every runtime trace — `ctor_mutants_leave_runtime_guarantees_intact` proves
+`controlFacts` and `PSubmit1.submitFacts` stay true on the pinned runtimes
+under both cuts — so the code-deposit conjunct is load-bearing on bytes
+nothing else in this repository constrains.
 -/
 def pcontrol1_forall_conj :=
   And.intro Eip8282.Audit.Step.validJumps_are_Xi_tables <|
diff --git a/Eip8282/Audit/Guarantees/PControl1/CtorXi.lean b/Eip8282/Audit/Guarantees/PControl1/CtorXi.lean
new file mode 100644
index 0000000..42ca539
--- /dev/null
+++ b/Eip8282/Audit/Guarantees/PControl1/CtorXi.lean
@@ -0,0 +1,140 @@
+import Eip8282.Audit.EvmRunner
+
+/-!
+C4, code-deposit half: the pinned **init** images run under `EvmYul.EVM.Ξ`.
+
+`Ctor.lean` closes C4 on a CFG prefix. Its own note is explicit about the
+gap: `fromHex` of the full init blobs times out in the kernel, so the
+opcode facts there are `rfl` on the *first* `++` chunk of `depositInitHex`
+and the first two chunks of `exitInitHex`. That reads the first 32 / 64
+bytes of a 638 / 503-byte image and never runs it. Three things were
+therefore unchecked:
+
+* that the init image reaches its `RETURN` at all;
+* that the buffer it returns is the pinned runtime **byte for byte**
+  rather than merely "a copy starting at the right offset";
+* that the exit ctor's `SSTORE` lands, as opposed to being present as an
+  opcode 34 bytes in.
+
+This module closes all three by executing the full pinned init images and
+comparing the returned buffer against the pinned runtime images.
+
+## What this is, and what it is not
+
+`Λ` (`EvmYul.EVM.Semantics.Lambda`, EVMYulLean `0ff72b2`) is `Ξ` on the
+init code followed by the code-deposit step (115): on success it writes
+`code := returnedData` into the new account. `initDeploys` below is
+exactly that `Ξ` half, plus the equality step (115) would use, stated
+against the pinned runtime image.
+
+It is deliberately **not** `Lambda` itself. `Lambda` derives its target
+address as `KEC(RLP(sender, nonce))`, and the EIP-8282 contracts are
+genesis predeploys at `0x0000bFF4…` / `0x000064D6…`, not `CREATE`
+outputs. Driving `Lambda` 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 that is the runtime carried as `CODECOPY` data — and
+neither preamble contains a `SHA3`, `CREATE`, call or precompile-dispatch
+opcode, so running them under `Ξ` leaves the `A-NATIVE-DECIDE` disclosure
+exactly as `Ctor` and Wave-1 state it.
+
+This does **not** discharge `A-PINNED-SOURCE`. It links `ctor.hex` to
+`main.hex` inside the pin; it observes nothing on chain. The residual
+open part is the deployed-address / deployed-codehash observation — see
+`audit/assumptions.yaml`.
+-/
+
+namespace Eip8282.Audit.Guarantees.PControl1.CtorXi
+
+open EvmYul
+open EvmYul.EVM
+open Eip8282.Audit.Bytecode
+open Eip8282.Audit.EvmRunner
+
+/-- The init images halt in far fewer steps than a runtime call: each
+preamble is a `CODECOPY` and a `RETURN`. -/
+def CTOR_FUEL : Nat := 20000
+
+/-- Account that deploys the predeploy. Its identity is irrelevant to the
+init programs — neither image reads `CALLER` before returning. -/
+def deployer : Nat := 0x1234
+
+/-- `Ξ` on an init image, with the account being created holding no code.
+
+`Ξ` is entered with `executionEnv.code := initCode`, which is what
+`CODESIZE` / `CODECOPY` read during creation, while the account being
+created still has none. `EvmRunner.run` would additionally install
+`initCode` as that account's code; the pinned preambles never read their
+own account code, but leaving it empty is the faithful creation world. -/
+def runInit (fuel : Nat) (target : AccountAddress) (initCode : ByteArray)
+    : RunResult :=
+  let σ : AccountMap .EVM :=
+    (default : AccountMap .EVM)
+      |>.insert target (mkAccount ByteArray.empty)
+      |>.insert (toAddress deployer) (mkAccount ByteArray.empty oneEth)
+  Ξ fuel default default default σ σ defaultGas default
+    (callEnv target initCode (toAddress deployer) ZERO_U256 ByteArray.empty)
+
+/-- Return buffer of a successful `Ξ`; empty on revert or interpreter error. -/
+def returnBuffer (r : RunResult) : ByteArray :=
+  match r with
+  | .ok (.success _ o) => o
+  | _ => ByteArray.empty
+
+/-- The code-deposit step (115) of `Λ`, on bytes: running `initCode`
+succeeds, and the buffer it returns is exactly `runtime` — the value
+`Λ` would install as the new account's `code`. -/
+def initDeploys (target : AccountAddress) (initCode runtime : ByteArray) : Bool :=
+  let r := runInit CTOR_FUEL target initCode
+  isSuccess r && bytesEq (returnBuffer r) runtime
+
+/-- Deposit ctor: deploys `depositRuntime` and writes no storage. -/
+def depositCtorFact (initCode : ByteArray) : Bool :=
+  initDeploys depositAddr initCode depositRuntime
+    && slots0to3Are (runInit CTOR_FUEL depositAddr initCode) depositAddr 0 0 0 0
+
+/-- Exit ctor: deploys `exitRuntime` and leaves slot 0 = `INHIBITOR` with
+slots 1–3 untouched. -/
+def exitCtorFact (initCode : ByteArray) : Bool :=
+  initDeploys exitAddr initCode exitRuntime
+    && slots0to3Are (runInit CTOR_FUEL exitAddr initCode) exitAddr
+        ((2 ^ 256) - 1) 0 0 0
+
+/-- Both ctor facts, parameterised by the two init images so that a
+one-byte init mutant can be fed to exactly the statement the parent is
+registered against. -/
+def ctorXiFacts (depInit exitInit : ByteArray) : Bool :=
+  depositCtorFact depInit && exitCtorFact exitInit
+
+/--
+**C4 code-deposit trace, on pinned init bytecode.**
+
+`Ξ` on the full pinned 638-byte deposit init and 503-byte exit init
+images. Each returned buffer is the pinned `depositRuntime` /
+`exitRuntime` byte for byte — the `code` that `Λ`'s step (115) would
+install. The exit ctor additionally leaves slot 0 at `INHIBITOR` with
+slots 1–3 zero; the deposit ctor writes nothing.
+
+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.
+
+Kill-line: `Eip8282.Tests.PControl1Mutant.ctor_mutant_refutes_parent`
+flips one byte of each init image — the deposit `CODECOPY` source offset
+at 5 (`0x0a` → `0x0b`) and the exit `SSTORE` at 34 (`0x55` → `0x50`,
+`POP`) — and shows `ctorXiFacts` is `false` on each.
+
+Discharged by `native_decide` for cost, on the same terms as the Wave-1
+traces: each image executes only its preamble before `RETURN`, and
+neither preamble contains a `SHA3`, `CREATE`, call or precompile-dispatch
+opcode, so no `opaque @[extern]` FFI constant and no `partial` RLP
+decoder is reached. See `A-NATIVE-DECIDE`.
+-/
+theorem pcontrol1_ctor_xi_parent :
+    ctorXiFacts depositInit exitInit = true := by
+  native_decide
+
+end Eip8282.Audit.Guarantees.PControl1.CtorXi
diff --git a/Eip8282/Audit/Trust.lean b/Eip8282/Audit/Trust.lean
index 31d96c4..77258d5 100644
--- a/Eip8282/Audit/Trust.lean
+++ b/Eip8282/Audit/Trust.lean
@@ -231,6 +231,14 @@ open at HIGH.
 #print axioms Eip8282.Tests.PControl1Mutant.wave5_mutants_leave_psubmit1_intact
 #print axioms Eip8282.Tests.PControl1Mutant.nonempty_is_not_empty
 
+-- C4 code-deposit half: Ξ on the full pinned init images (Node 4).
+#print axioms Eip8282.Audit.Guarantees.PControl1.CtorXi.pcontrol1_ctor_xi_parent
+#print axioms Eip8282.Tests.PControl1Mutant.pinned_ctor_bytes
+#print axioms Eip8282.Tests.PControl1Mutant.ctor_mutants_differ_in_one_byte
+#print axioms Eip8282.Tests.PControl1Mutant.ctor_mutant_refutes_parent
+#print axioms Eip8282.Tests.PControl1Mutant.ctor_mutants_are_independent
+#print axioms Eip8282.Tests.PControl1Mutant.ctor_mutants_leave_runtime_guarantees_intact
+
 -- R4: unconditional `X` → `Ξ` layer. Three foundational axioms only.
 #print axioms Eip8282.Audit.XiTransport.observe_Xi_eq_observe_X
 #print axioms Eip8282.Audit.XiTransport.observe_Xi_zero
diff --git a/Eip8282/Tests/PControl1Mutant.lean b/Eip8282/Tests/PControl1Mutant.lean
index 09c901f..ab07232 100644
--- a/Eip8282/Tests/PControl1Mutant.lean
+++ b/Eip8282/Tests/PControl1Mutant.lean
@@ -270,4 +270,73 @@ theorem fold_equating_mutants_leave_psubmit1_intact :
     ∧ Eip8282.Audit.Guarantees.PSubmit1.submitFacts depositRuntime foldEquatingExit = true := by
   native_decide
 
+/-! ## Kill-line for the C4 code-deposit conjunct
+
+`CtorXi.ctorXiFacts` is cut on the **init** images, one byte each. These
+are bytes no runtime trace can reach: the init code is not the deployed
+code, so neither `controlFacts` nor `submitFacts` nor `drainFacts`
+constrains them. Before `pcontrol1_ctor_xi_parent` nothing in this
+repository did.
+-/
+
+open Eip8282.Audit.Guarantees.PControl1.CtorXi
+
+/-- Source offset of the runtime copy in the deposit ctor
+(`PUSH2 0x0274; DUP1; PUSH1 0x0a; PUSH0; CODECOPY`): the `0x0a` operand. -/
+def depositCtorSrcIdx : Nat := 5
+
+/-- The `SSTORE` of the exit ctor's `PUSH32 INHIBITOR; PUSH0; SSTORE`. -/
+def exitCtorSstoreIdx : Nat := 34
+
+/-- Sanity: the pinned init bytes really are what the mutations claim to cut. -/
+theorem pinned_ctor_bytes :
+    depositInit.size = 638
+    ∧ exitInit.size = 503
+    ∧ depositInit.get! depositCtorSrcIdx = 0x0a
+    ∧ exitInit.get! exitCtorSstoreIdx = 0x55 := by
+  native_decide
+
+/-- `CODECOPY` source `10` → `11`. The ctor still returns 628 bytes and
+still succeeds, but the buffer is the runtime shifted one byte, so the
+code deposited is not the code every other guarantee is proved about. -/
+def ctorSrcMutatedDeposit : ByteArray := depositInit.set! depositCtorSrcIdx 0x0b
+
+/-- `SSTORE` → `POP`. The exit ctor still deploys the right runtime, but
+slot 0 is left at 0 instead of `INHIBITOR`, so the exit contract starts
+un-inhibited — the exact failure C4 exists to exclude. -/
+def sstoreMutatedExit : ByteArray := exitInit.set! exitCtorSstoreIdx 0x50
+
+theorem ctor_mutants_differ_in_one_byte :
+    ctorSrcMutatedDeposit.size = depositInit.size
+    ∧ ctorSrcMutatedDeposit.get! depositCtorSrcIdx = 0x0b
+    ∧ sstoreMutatedExit.size = exitInit.size
+    ∧ sstoreMutatedExit.get! exitCtorSstoreIdx = 0x50 := by
+  native_decide
+
+/-- **The C4 code-deposit kill-line.** `ctorXiFacts` is the conjunct
+`pcontrol1_c4_ctor_forall` carries, so each cut also makes the registered
+`pcontrol1_forall_parent` false of the mutated init image. -/
+theorem ctor_mutant_refutes_parent :
+    ctorXiFacts ctorSrcMutatedDeposit exitInit = false
+    ∧ ctorXiFacts depositInit sstoreMutatedExit = false := by
+  native_decide
+
+/-- The two cuts are independent: the shifted-copy mutant leaves the exit
+ctor alone and the lost-`SSTORE` mutant leaves the deposit ctor alone. -/
+theorem ctor_mutants_are_independent :
+    depositCtorFact ctorSrcMutatedDeposit = false
+    ∧ exitCtorFact exitInit = true
+    ∧ depositCtorFact depositInit = true
+    ∧ exitCtorFact sstoreMutatedExit = false := by
+  native_decide
+
+/-- The init cuts leave every runtime guarantee intact: the deployed code
+is a different byte string from the init code, so no runtime trace can
+see these bytes. This is what makes the C4 code-deposit conjunct
+load-bearing rather than a restatement. -/
+theorem ctor_mutants_leave_runtime_guarantees_intact :
+    controlFacts depositRuntime exitRuntime = true
+    ∧ Eip8282.Audit.Guarantees.PSubmit1.submitFacts depositRuntime exitRuntime = true := by
+  native_decide
+
 end Eip8282.Tests.PControl1Mutant
diff --git a/README.md b/README.md
index f0179cd..6db08e5 100644
--- a/README.md
+++ b/README.md
@@ -162,8 +162,22 @@ Two disclosed costs, both in `audit/assumptions.yaml`:
   parents are under `WellFormed` / `CallHyp`. `A-ABSTRACT-TX` stays: F4
   did not prove `Ξ ↔ Model`.
 
-Deployment provenance is out of the current claim. P-CONTROL-1's C4 lemmas
-are CFG prefixes of the pinned init bytecode, not `Ξ` CREATE traces.
+Deployment provenance is still out of the current claim, but C4 no longer
+stops at a CFG prefix. `PControl1.CtorXi.pcontrol1_ctor_xi_parent` runs the
+full pinned 638-byte deposit and 503-byte exit init images under
+`EvmYul.EVM.Ξ` and pins the buffer each returns to be `depositRuntime` /
+`exitRuntime` byte for byte — the `code` that `Λ`'s step (115) installs —
+with the exit ctor leaving slot 0 at `INHIBITOR`. That is what ties
+`pinned/bytecode/*/ctor.hex` to `pinned/bytecode/*/main.hex`;
+`audit/artifacts.lock.json` hashes the two files independently.
+
+It is deliberately not `Λ` itself. `Λ` derives its address as
+`KEC(RLP(sender, nonce))`, and the EIP-8282 contracts are genesis
+predeploys, not `CREATE` outputs — so driving `Λ` would pin an address
+that is provably not the predeploy address. No address derivation is
+claimed, and `A-PINNED-SOURCE` stays **open**: nothing here observes chain
+state. What remains is a single observation — the live codehash at
+`0x0000bFF4…` / `0x000064D6…` against keccak of the pinned `main.hex`.
 
 The three IDs are the smallest coherent audit surface:
 
diff --git a/audit/assumptions.yaml b/audit/assumptions.yaml
index dfb6b1f..d848e85 100644
--- a/audit/assumptions.yaml
+++ b/audit/assumptions.yaml
@@ -60,12 +60,12 @@
     {
       "id": "A-PINNED-SOURCE",
       "accepted": true,
-      "risk": "Assembly and EIP text are pinned snapshots, not live-deployed bytecode.",
-      "justification": "sys-asm@83f9801 and EIPs PR #12120 head b759aae8 are the working references.",
+      "risk": "Assembly and EIP text are pinned snapshots, not live-deployed bytecode. STILL OPEN. Node 4 closed the ctor-to-runtime half only: nothing here observes chain state, and no deployed codehash is claimed.",
+      "justification": "sys-asm@83f9801 and EIPs PR #12120 head b759aae8 are the working references. Within the pin, the two bytecode files are no longer independent: Eip8282.Audit.Guarantees.PControl1.CtorXi.pcontrol1_ctor_xi_parent runs the full pinned ctor.hex images under EvmYul.EVM.Ξ and shows each returns main.hex byte for byte, which is the code Λ step (115) installs. So keccak(deployed code) is determined by ctor.hex given the pin. What remains assumed is that these files are the images actually at 0x0000bFF46984e3725691FA540a8C7589300D8282 and 0x000064D678505ad48F8cCb093BC65613800E8282.",
       "severity": "HIGH",
-      "violation_impact": "A later sys-asm or EIP revision can invalidate the model.",
-      "validation": "audit/artifacts.lock.json sha256 of pinned files.",
-      "removal_path": "Add deployed-bytecode observation and keccak identity."
+      "violation_impact": "A later sys-asm or EIP revision can invalidate the model. Because the predeploys are genesis-installed rather than CREATE outputs, no address derivation is proved either: Λ's KEC(RLP(sender,nonce)) address is not the predeploy address, so CtorXi deliberately does not invoke Lambda and the deployed-address binding is untouched.",
+      "validation": "audit/artifacts.lock.json sha256 of pinned files, plus PControl1.CtorXi.pcontrol1_ctor_xi_parent tying ctor.hex to main.hex inside the pin. Kill-line: Eip8282.Tests.PControl1Mutant.ctor_mutant_refutes_parent.",
+      "removal_path": "Observe the live codehash at the two predeploy addresses and check it against keccak of the pinned main.hex. The ctor-to-runtime link is now proved, so that single observation would close this assumption."
     }
   ]
 }
diff --git a/audit/guarantees.yaml b/audit/guarantees.yaml
index 3a9d81d..3b9b66b 100644
--- a/audit/guarantees.yaml
+++ b/audit/guarantees.yaml
@@ -144,7 +144,7 @@
     {
       "id": "P-CONTROL-1",
       "parent": "Eip8282.Audit.Guarantees.PControl1.pcontrol1_forall_parent",
-      "parent_note": "The registered parent is the CFG-level ∀ theorem under WellFormed/CallHyp (gas ≥ 30M, caller class), conjoined with the Wave-1 pcontrol1_bytecode_parent, Wave-5 pcontrol1_nonempty_bytecode_parent, and fold-discrimination traces that the kill-line still refutes. The fold-discrimination conjunct (pcontrol1_fold_discriminate_parent) asserts that the user-path bump_excess fold (excess + max(0, count−TARGET)) and the system-path update_excess fold (max(0, excess+count−TARGET)) produce different values on both runtimes. R4 (Eip8282.Audit.XiTransport.pcontrol1_xi_forall_parent) carries this same theorem as a conjunct alongside a complete-Ξ observational transport that still takes EndpointAgrees / A-ABSTRACT-TX as an explicit OPEN hypothesis. The YAML parent ID is unchanged. The abstract-model theorem below is supporting evidence, not a substitute: per audit/WAVE0.md, abstract CHECKED does not stand in for bytecode CHECKED. This parent is not Ξ ↔ Model.",
+      "parent_note": "The registered parent is the CFG-level ∀ theorem under WellFormed/CallHyp (gas ≥ 30M, caller class), conjoined with the Wave-1 pcontrol1_bytecode_parent, Wave-5 pcontrol1_nonempty_bytecode_parent, and fold-discrimination traces that the kill-line still refutes. The fold-discrimination conjunct (pcontrol1_fold_discriminate_parent) asserts that the user-path bump_excess fold (excess + max(0, count−TARGET)) and the system-path update_excess fold (max(0, excess+count−TARGET)) produce different values on both runtimes. R4 (Eip8282.Audit.XiTransport.pcontrol1_xi_forall_parent) carries this same theorem as a conjunct alongside a complete-Ξ observational transport that still takes EndpointAgrees / A-ABSTRACT-TX as an explicit OPEN hypothesis. The YAML parent ID is unchanged. The abstract-model theorem below is supporting evidence, not a substitute: per audit/WAVE0.md, abstract CHECKED does not stand in for bytecode CHECKED. This parent is not Ξ ↔ Model. C4 now also carries a code-deposit conjunct: Eip8282.Audit.Guarantees.PControl1.CtorXi.pcontrol1_ctor_xi_parent runs the full pinned ctor.hex images under EvmYul.EVM.Xi and pins the buffer each returns to be the pinned main.hex byte for byte, which is the code Lambda step (115) installs. It is not Lambda itself: the predeploys are genesis-installed, so Lambda's KEC(RLP(sender,nonce)) address is not the predeploy address and no address derivation or Reachable claim is made.",
       "assumptions": [
         "A-ABSTRACT-TX",
         "A-REACHABLE",
@@ -154,11 +154,11 @@
         "A-PINNED-SOURCE"
       ],
       "reproduction": {
-        "command": "lake build EvmYul.FFI.ffi:dynlib && lake build Eip8282.Audit.Guarantees.PControl1 Eip8282.Tests.PControl1Mutant Eip8282.Audit.Trust",
-        "expected": "pcontrol1_forall_parent, pcontrol1_bytecode_parent, pcontrol1_nonempty_bytecode_parent, pcontrol1_fold_discriminate_parent, and the bytecode kill-lines build; Trust prints propext, Classical.choice, Quot.sound for the ∀ conjuncts and for the four D_J jumpdest tables and their validJumps bridges, plus one <theorem>._native.native_decide.ax_1_1 for each kept bytecode trace theorem (empty-queue parent, nonempty-queue parent, fold discrimination, Wave-1 mutants, Wave-5 mutants, fold-equating mutants, and independence)",
+        "command": "lake build EvmYul.FFI.ffi:dynlib && lake build Eip8282.Audit.Guarantees.PControl1 Eip8282.Audit.Guarantees.PControl1.CtorXi Eip8282.Tests.PControl1Mutant Eip8282.Audit.Trust",
+        "expected": "pcontrol1_forall_parent, pcontrol1_bytecode_parent, pcontrol1_nonempty_bytecode_parent, pcontrol1_fold_discriminate_parent, and the bytecode kill-lines build; Trust prints propext, Classical.choice, Quot.sound for the ∀ conjuncts and for the four D_J jumpdest tables and their validJumps bridges, plus one <theorem>._native.native_decide.ax_1_1 for each kept bytecode trace theorem (empty-queue parent, nonempty-queue parent, fold discrimination, Wave-1 mutants, Wave-5 mutants, fold-equating mutants, and independence), plus pcontrol1_ctor_xi_parent and the C4 code-deposit kill-lines (ctor_mutant_refutes_parent, ctor_mutants_are_independent, ctor_mutants_leave_runtime_guarantees_intact)",
         "prerequisite": "The first target builds EVMYulLean's keccak/sha2 FFI shared objects. native_decide runs the compiled interpreter, which needs them; lakefile.lean passes both via --load-dynlib, libleanffi.so first."
       },
-      "summary": "The control plane of both predeploys: msg.sender alone decides the fee-quote vs system subroutine; a paid user wraps SLOT_COUNT += 1 and leaves excess; every system call resets SLOT_COUNT and rewrites SLOT_EXCESS to INHIBITOR on nonempty calldata, 0 if already inhibited, else max(0, excess+count-TARGET) for TARGET 8 (deposits) and 2 (exits). The user-path bump_excess fold (excess + max(0, count−TARGET)) and the system-path update_excess fold (max(0, excess+count−TARGET)) are distinct computations: at (100, 5, 8) they give 100 vs 97, at (100, 1, 2) they give 100 vs 99. Queue length is unused. Exit init stores INHIBITOR at slot 0 then returns runtime; deposit init does not SSTORE. Under CallHyp (WellFormed storage, gas ≥ 30M, caller class) this is a CFG-level ∀ (C1 gate, C2 excess, C3 count, C4 ctor). The Wave-1 controlFacts, Wave-5 nonemptyControlFacts, and fold-discrimination traces remain as the kill-line witness.",
+      "summary": "The control plane of both predeploys: msg.sender alone decides the fee-quote vs system subroutine; a paid user wraps SLOT_COUNT += 1 and leaves excess; every system call resets SLOT_COUNT and rewrites SLOT_EXCESS to INHIBITOR on nonempty calldata, 0 if already inhibited, else max(0, excess+count-TARGET) for TARGET 8 (deposits) and 2 (exits). The user-path bump_excess fold (excess + max(0, count−TARGET)) and the system-path update_excess fold (max(0, excess+count−TARGET)) are distinct computations: at (100, 5, 8) they give 100 vs 97, at (100, 1, 2) they give 100 vs 99. Queue length is unused. Exit init stores INHIBITOR at slot 0 then returns runtime; deposit init does not SSTORE. Under CallHyp (WellFormed storage, gas ≥ 30M, caller class) this is a CFG-level ∀ (C1 gate, C2 excess, C3 count, C4 ctor). The Wave-1 controlFacts, Wave-5 nonemptyControlFacts, and fold-discrimination traces remain as the kill-line witness. Beyond the init CFG preamble, the full pinned init images are executed under Xi and shown to return exactly the pinned runtime images, tying ctor.hex to main.hex inside the pin (A-PINNED-SOURCE stays OPEN: no chain observation is made).",
       "abstract": {
         "status": "CHECKED",
         "theorem": "Eip8282.Audit.Guarantees.PControl1.empty_updates_excess"
@@ -167,14 +167,14 @@
         "status": "CHECKED",
         "scope": "CFG_FORALL",
         "theorem": "Eip8282.Audit.Guarantees.PControl1.pcontrol1_forall_parent",
-        "executes": "CFG stepper on the pinned opening CALLER/EQ/JUMPI gate (C1), the system update_excess … SLOT_EXCESS SSTORE block (C2), the paid-user SLOT_COUNT increment and system store_excess count reset (C3), and the deposit/exit init preambles (C4) of pinned/bytecode/builder_{deposits,exits}/{ctor,main}.hex. Kill-line traces still run EvmYul.EVM.Xi (EVMYulLean 0ff72b2db35302305fccb1d4f42b480434b77bfe) via Eip8282.Audit.EvmRunner. Not a proof that Ξ agrees with Model.userCall/systemCall.",
-        "world": "CallHyp: WellFormed packed queue (slots 0–3, head ≤ tail), gas ≥ 30000000, caller class (SYSTEM_ADDR vs not). C2 additionally needs the UInt256 sum-no-wrap hypothesis on the empty non-inhibited fold. Ctor CFG is the init preamble under campaign gas, not CREATE. Kill-line traces keep the two-account synthetic world: empty-queue control (excess in {0,5,100,112,120,250,300,2^256-1}, count in {0,1,2,3,4,5,7,8,9,17,20,30,40}, HEAD=TAIL=0) plus nonempty-queue control (excess 100 count 5 HEAD 0 TAIL 2/17/65) and inhibited variants.",
+        "executes": "CFG stepper on the pinned opening CALLER/EQ/JUMPI gate (C1), the system update_excess … SLOT_EXCESS SSTORE block (C2), the paid-user SLOT_COUNT increment and system store_excess count reset (C3), and the deposit/exit init preambles (C4) of pinned/bytecode/builder_{deposits,exits}/{ctor,main}.hex. Kill-line traces still run EvmYul.EVM.Xi (EVMYulLean 0ff72b2db35302305fccb1d4f42b480434b77bfe) via Eip8282.Audit.EvmRunner. Not a proof that Ξ agrees with Model.userCall/systemCall. C4 additionally executes the complete 638-byte deposit and 503-byte exit init images under EvmYul.EVM.Xi and compares the returned code-deposit buffer against the pinned runtime images byte for byte (CtorXi.pcontrol1_ctor_xi_parent).",
+        "world": "CallHyp: WellFormed packed queue (slots 0–3, head ≤ tail), gas ≥ 30000000, caller class (SYSTEM_ADDR vs not). C2 additionally needs the UInt256 sum-no-wrap hypothesis on the empty non-inhibited fold. Ctor CFG is the init preamble under campaign gas, not CREATE. Kill-line traces keep the two-account synthetic world: empty-queue control (excess in {0,5,100,112,120,250,300,2^256-1}, count in {0,1,2,3,4,5,7,8,9,17,20,30,40}, HEAD=TAIL=0) plus nonempty-queue control (excess 100 count 5 HEAD 0 TAIL 2/17/65) and inhibited variants. The C4 code-deposit trace uses a creation world: the account being created holds no code, Xi is entered with executionEnv.code = the init image, empty calldata, zero value.",
         "kill_line": {
           "module": "Eip8282.Tests.PControl1Mutant",
           "theorem": "Eip8282.Tests.PControl1Mutant.wave5_mutant_refutes_nonempty_parent",
-          "mutation": "three standard single-byte cuts plus two fold-equating cuts, each fed to the same controlFacts / nonemptyControlFacts / fold-discrimination facts the ∀ parent still contains: builder_deposits runtime byte 22, EQ (0x14) -> LT (0x10), the CALLER vs SYSTEM_ADDR gate (CFG: gateEqPc); builder_deposits runtime byte 571, PUSH1 operand 8 -> 9, the system compute_excess TARGET (CFG: update_excess local 70 / blockBase+71); builder_exits runtime byte 401, PUSH1 operand 2 -> 3, the exit system TARGET (Wave 5). Fold-equating cuts: builder_deposits byte 571 PUSH1 operand 8 -> 5 (equates bump_excess and update_excess at (100,5,8): both give 100); builder_exits byte 401 PUSH1 operand 2 -> 1 (equates at (100,1,2): both give 100). mutant_refutes_parent covers EQ@22 and TARGET 8@571 against controlFacts; wave5_mutant_refutes_nonempty_parent covers TARGET 8@571, TARGET 2@401, and EQ@22 against nonemptyControlFacts; fold_equating_mutant_refutes_discrimination covers 571: 8→5 and 401: 2→1 against the fold-discrimination facts; existing_kill_line_refutes_fold_discrimination covers 571: 8→9 and 401: 2→3. The user-side bump_excess at 83/82, the LOG0 sizes, and the drain-only caps are left alone.",
-          "effect": "controlFacts gateMutatedDeposit exitRuntime = false, controlFacts depositRuntime gateMutatedExit = false, and controlFacts targetMutatedDeposit exitRuntime = false. nonemptyControlFacts wave5TargetMutatedDeposit exitRuntime = false, nonemptyControlFacts depositRuntime wave5TargetMutatedExit = false, and nonemptyControlFacts gateMutatedDeposit exitRuntime = false. depositFoldDiscriminateFact foldEquatingDeposit = false and exitFoldDiscriminateFact foldEquatingExit = false: the equating cuts make the system store the bump_excess value (100) instead of the update_excess value (97/99), merging the two folds. depositFoldDiscriminateFact targetMutatedDeposit = false and exitFoldDiscriminateFact wave5TargetMutatedExit = false: the standard kill-line also refutes the fold discrimination. Concretely the gate cut answers SYSTEM_ADDR as a user (32-byte quote, count stays 5); the deposit TARGET cut stores excess 96 not 97 on empty and nonempty images; the exit TARGET cut stores 102 not 103; the fold-equating deposit cut stores 100 not 97; the fold-equating exit cut stores 100 not 99. Because pcontrol1_forall_parent includes the bytecode parents and the fold discrimination, each mutant makes the registered parent false of that bytecode. The mutations are to bytecode bytes, not to any model function.",
-          "independence": "Eip8282.Tests.PControl1Mutant.control_mutants_leave_psubmit1_intact, wave5_mutants_leave_psubmit1_intact, and fold_equating_mutants_leave_psubmit1_intact prove the EQ@22, TARGET 8/2, and fold-equating cuts leave Eip8282.Audit.Guarantees.PSubmit1.submitFacts true. P-SUBMIT-1 never calls as SYSTEM_ADDR and never reaches compute_excess. P-DRAIN-1's FIFO and amount recoding are separate and remain true on the pinned bytes; the P-CONTROL-1 parent is not a restatement of a sibling. P-SUBMIT-1 / P-DRAIN-1 registered parents are not changed."
+          "mutation": "three standard single-byte cuts plus two fold-equating cuts, each fed to the same controlFacts / nonemptyControlFacts / fold-discrimination facts the ∀ parent still contains: builder_deposits runtime byte 22, EQ (0x14) -> LT (0x10), the CALLER vs SYSTEM_ADDR gate (CFG: gateEqPc); builder_deposits runtime byte 571, PUSH1 operand 8 -> 9, the system compute_excess TARGET (CFG: update_excess local 70 / blockBase+71); builder_exits runtime byte 401, PUSH1 operand 2 -> 3, the exit system TARGET (Wave 5). Fold-equating cuts: builder_deposits byte 571 PUSH1 operand 8 -> 5 (equates bump_excess and update_excess at (100,5,8): both give 100); builder_exits byte 401 PUSH1 operand 2 -> 1 (equates at (100,1,2): both give 100). mutant_refutes_parent covers EQ@22 and TARGET 8@571 against controlFacts; wave5_mutant_refutes_nonempty_parent covers TARGET 8@571, TARGET 2@401, and EQ@22 against nonemptyControlFacts; fold_equating_mutant_refutes_discrimination covers 571: 8→5 and 401: 2→1 against the fold-discrimination facts; existing_kill_line_refutes_fold_discrimination covers 571: 8→9 and 401: 2→3. The user-side bump_excess at 83/82, the LOG0 sizes, and the drain-only caps are left alone. C4 code-deposit cuts, on the init images rather than the runtimes: builder_deposits ctor byte 5, CODECOPY source operand 0x0a -> 0x0b, shifting the deployed copy by one byte; builder_exits ctor byte 34, SSTORE (0x55) -> POP (0x50), so slot 0 is left at 0 instead of INHIBITOR. ctor_mutant_refutes_parent feeds each to the same ctorXiFacts the parent contains.",
+          "effect": "controlFacts gateMutatedDeposit exitRuntime = false, controlFacts depositRuntime gateMutatedExit = false, and controlFacts targetMutatedDeposit exitRuntime = false. nonemptyControlFacts wave5TargetMutatedDeposit exitRuntime = false, nonemptyControlFacts depositRuntime wave5TargetMutatedExit = false, and nonemptyControlFacts gateMutatedDeposit exitRuntime = false. depositFoldDiscriminateFact foldEquatingDeposit = false and exitFoldDiscriminateFact foldEquatingExit = false: the equating cuts make the system store the bump_excess value (100) instead of the update_excess value (97/99), merging the two folds. depositFoldDiscriminateFact targetMutatedDeposit = false and exitFoldDiscriminateFact wave5TargetMutatedExit = false: the standard kill-line also refutes the fold discrimination. Concretely the gate cut answers SYSTEM_ADDR as a user (32-byte quote, count stays 5); the deposit TARGET cut stores excess 96 not 97 on empty and nonempty images; the exit TARGET cut stores 102 not 103; the fold-equating deposit cut stores 100 not 97; the fold-equating exit cut stores 100 not 99. Because pcontrol1_forall_parent includes the bytecode parents and the fold discrimination, each mutant makes the registered parent false of that bytecode. The mutations are to bytecode bytes, not to any model function. ctorXiFacts ctorSrcMutatedDeposit exitInit = false and ctorXiFacts depositInit sstoreMutatedExit = false: the shifted copy deploys a byte string that is not depositRuntime, and the lost SSTORE leaves the exit contract un-inhibited at genesis. ctor_mutants_are_independent shows each cut refutes only its own half.",
+          "independence": "Eip8282.Tests.PControl1Mutant.control_mutants_leave_psubmit1_intact, wave5_mutants_leave_psubmit1_intact, and fold_equating_mutants_leave_psubmit1_intact prove the EQ@22, TARGET 8/2, and fold-equating cuts leave Eip8282.Audit.Guarantees.PSubmit1.submitFacts true. P-SUBMIT-1 never calls as SYSTEM_ADDR and never reaches compute_excess. P-DRAIN-1's FIFO and amount recoding are separate and remain true on the pinned bytes; the P-CONTROL-1 parent is not a restatement of a sibling. P-SUBMIT-1 / P-DRAIN-1 registered parents are not changed. Eip8282.Tests.PControl1Mutant.ctor_mutants_leave_runtime_guarantees_intact shows the two init cuts leave controlFacts and PSubmit1.submitFacts true on the pinned runtimes: the init images are not the deployed code, so no runtime trace constrains those bytes and the C4 code-deposit conjunct is load-bearing rather than a restatement."
         }
       },
       "fidelity": {