diff --git a/ToMathlib/Data/IndexedBinaryTree/Basic.lean b/ToMathlib/Data/IndexedBinaryTree/Basic.lean
index 91d3d41c..583caca5 100644
--- a/ToMathlib/Data/IndexedBinaryTree/Basic.lean
+++ b/ToMathlib/Data/IndexedBinaryTree/Basic.lean
@@ -87,6 +87,7 @@ inductive SkeletonInternalIndex : Skeleton → Type
       SkeletonInternalIndex (Skeleton.internal left right)
   | ofRight {left right : Skeleton} (idxRight : SkeletonInternalIndex right) :
       SkeletonInternalIndex (Skeleton.internal left right)
+  deriving DecidableEq
 
 /-- Type of indices of any node of a skeleton -/
 inductive SkeletonNodeIndex : Skeleton → Type
@@ -583,6 +584,14 @@ def SkeletonInternalIndex.depth {s : Skeleton} : SkeletonInternalIndex s → Nat
   | SkeletonInternalIndex.ofLeft idxLeft => idxLeft.depth + 1
   | SkeletonInternalIndex.ofRight idxRight => idxRight.depth + 1
 
+/-- The height of the subtree rooted at an internal-node index. -/
+@[simp]
+def SkeletonInternalIndex.subtreeDepth :
+    {s : Skeleton} → SkeletonInternalIndex s → Nat
+  | .internal left right, .ofInternal => (Skeleton.internal left right).depth
+  | _, .ofLeft idxLeft => idxLeft.subtreeDepth
+  | _, .ofRight idxRight => idxRight.subtreeDepth
+
 /-- Depth of a SkeletonNodeIndex -/
 def SkeletonNodeIndex.depth {s : Skeleton} : SkeletonNodeIndex s → Nat
   | SkeletonNodeIndex.ofLeaf => 0
diff --git a/VCVio.lean b/VCVio.lean
index 4bce7595..63eaffcc 100644
--- a/VCVio.lean
+++ b/VCVio.lean
@@ -52,6 +52,8 @@ public import VCVio.CryptoFoundations.KEMDEM
 public import VCVio.CryptoFoundations.KeyEncapMech
 public import VCVio.CryptoFoundations.MacAlg
 public import VCVio.CryptoFoundations.MacFromPRF
+public import VCVio.CryptoFoundations.MerkleTree.Addressed.Basic
+public import VCVio.CryptoFoundations.MerkleTree.Addressed.Level
 public import VCVio.CryptoFoundations.MerkleTree.Inductive.Batch.Completeness
 public import VCVio.CryptoFoundations.MerkleTree.Inductive.Batch.Defs
 public import VCVio.CryptoFoundations.MerkleTree.Inductive.Batch.ToSingle
diff --git a/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean b/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean
new file mode 100644
index 00000000..7f67b6c4
--- /dev/null
+++ b/VCVio/CryptoFoundations/MerkleTree/Addressed/Basic.lean
@@ -0,0 +1,536 @@
+/-
+Copyright (c) 2026 Richard Goodman. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Goodman
+-/
+
+module
+public import VCVio.CryptoFoundations.MerkleTree.Inductive.Binding
+public import VCVio.CryptoFoundations.TweakableHash
+
+/-! # Node-Addressed Merkle Trees
+
+Merkle trees whose node hash may depend on the **full address** of the node being
+hashed — the typed root-path position `SkeletonInternalIndex s` — via
+`nodeHash : SkeletonInternalIndex s → α → α → α`.
+
+Tree building, putative-root recomputation, completeness, and constructive collision
+tracing are defined and proven **once here**, for an arbitrary `nodeHash`. Every hash
+discipline expressible as a `nodeHash` — the ordinary tree (constant), the
+level-separated tree (`nodeHash` through the depth of the addressed subtree), and
+XMSS/SLH-DSA-style fully-addressed trees (`nodeHash` through an arbitrary
+address-to-tweak map) — inherits all of it by specialization.
+
+**Scope note (staged, deliberately).** The pre-existing unaddressed API in
+`MerkleTree.Inductive` is *not* re-expressed as a wrapper around this engine: its
+definitions (`getPutativeRootWithHash`, `populateUp`, `findCollision`) stand
+unchanged, and this module is added alongside them. What the `Instances` section
+below establishes instead is that the unaddressed API is **propositionally
+subsumed** at the constant instance — its build and putative-root computations are
+recovered (`populateUpAddressed_const`, `getPutativeRootAddressed_const`), its
+completeness theorem is *re-derived* from this engine's rather than reproved
+(`functional_completeness_of_addressed`), and its constructive collision walk is
+literally this engine's walk with the address tag erased
+(`findCollisionAddressed_const`). Turning that propositional subsumption into a
+definitional one — redefining the unaddressed entry points as constant
+specializations — would change a load-bearing upstream API consumed by
+`Inductive.Extractability`, `Inductive.Batch`, `Uniqueness` and `QueryBound`, so it
+is left as a follow-up for the maintainers rather than performed inside this
+contribution.
+
+Design: at each recursion step into a child, the engine passes the *reindexed* hash
+`fun a => nodeHash (.ofLeft a)` (resp. `.ofRight`) — the address is threaded by
+precomposition, so no explicit path accumulator or embedding parameter appears.
+
+Contents:
+
+* `SkeletonInternalIndex` — typed addresses of **internal** nodes (only internal nodes hash);
+  `SkeletonInternalIndex.subtreeDepth` recovers the height of the addressed subtree (the
+  level-separation data), and the full constructor path is the XMSS address.
+* `populateUpAddressed` / `buildMerkleTreeAddressedWithHash` — cache construction.
+* `getPutativeRootAddressedWithHash` — putative-root recomputation from a leaf, an
+  authentication path (`generateProof` is reused unchanged — proofs carry no
+  addresses), and a leaf index.
+* `addressed_functional_completeness` — honest paths verify, for **every** `nodeHash`.
+* `AddressedCollision`, `findCollisionAddressed`, `findCollisionAddressed_sound` —
+  the constructive collision kernel, returning the collision **as data, tagged with
+  the address** at which it occurs: two distinct pairs with equal hash *under that
+  address's hash function*.
+* `getPutativeRootAddressedWithHash_binding_collision` — the user-facing binding
+  statement: distinct leaf values verifying to the same root at the same index yield
+  an address-tagged collision.
+
+The symmetric collision statement here is deliberately **not** phrased as a
+target-collision-resistance win: TCR is directional (one endpoint fixed at
+target-registration time). The oriented reduction against a sampled-target game is
+the follow-up consumer of the address tag.
+-/
+
+@[expose] public section
+
+namespace AddressedMerkleTree
+
+open List OracleSpec OracleComp BinaryTree InductiveMerkleTree
+
+variable {α : Type _} [DecidableEq α]
+
+
+/-- Build the full cache of a Merkle tree under an address-dependent hash: each
+internal node stores `nodeHash addr leftRoot rightRoot` where `addr` is that node's
+address. The address is threaded by reindexing `nodeHash` along `.ofLeft` / `.ofRight`. -/
+@[simp, grind]
+def populateUpAddressed : {s : Skeleton} → (nodeHash : SkeletonInternalIndex s → α → α → α) →
+    LeafData α s → FullData α s
+  | .leaf, _, .leaf v => .leaf v
+  | .internal _ _, nh, .internal dl dr =>
+    let L := populateUpAddressed (fun a => nh (.ofLeft a)) dl
+    let R := populateUpAddressed (fun a => nh (.ofRight a)) dr
+    .internal (nh .ofInternal L.getRootValue R.getRootValue) L R
+
+/-- Alias matching the naming of the unaddressed engine. -/
+@[simp, grind]
+def buildMerkleTreeAddressedWithHash {s : Skeleton} (leaf_tree : LeafData α s)
+    (nodeHash : SkeletonInternalIndex s → α → α → α) : FullData α s :=
+  populateUpAddressed nodeHash leaf_tree
+
+/-- Recompute the putative root from a leaf value, its index, and an authentication
+path, hashing each step under the address of the node being reconstituted. The
+node reconstituted by the *last* step is the root (`.ofInternal`); descending into the
+index reindexes the hash along the path. -/
+@[simp, grind]
+def getPutativeRootAddressedWithHash :
+    {s : Skeleton} → (nodeHash : SkeletonInternalIndex s → α → α → α) →
+      (idx : SkeletonLeafIndex s) → (leafValue : α) → List.Vector α idx.depth → α
+  | _, _, .ofLeaf, leafValue, _ => leafValue
+  | _, nh, .ofLeft idxLeft, leafValue, proof =>
+    nh .ofInternal (getPutativeRootAddressedWithHash (fun a => nh (.ofLeft a)) idxLeft
+      leafValue proof.tail) proof.head
+  | _, nh, .ofRight idxRight, leafValue, proof =>
+    nh .ofInternal proof.head (getPutativeRootAddressedWithHash (fun a => nh (.ofRight a)) idxRight
+      leafValue proof.tail)
+
+omit [DecidableEq α] in
+/-- **Completeness of the engine**: an honestly generated authentication path
+recomputes the honest root, for every address-dependent hash. -/
+theorem addressed_functional_completeness {s : Skeleton}
+    (idx : SkeletonLeafIndex s) (leaf_data_tree : LeafData α s)
+    (nodeHash : SkeletonInternalIndex s → α → α → α) :
+    getPutativeRootAddressedWithHash nodeHash idx (leaf_data_tree.get idx)
+      (generateProof (buildMerkleTreeAddressedWithHash leaf_data_tree nodeHash) idx)
+    = (buildMerkleTreeAddressedWithHash leaf_data_tree nodeHash).getRootValue := by
+  induction idx with
+  | ofLeaf => cases leaf_data_tree; rfl
+  | ofLeft idxLeft ih =>
+    cases leaf_data_tree with
+    | internal dl dr =>
+      simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed,
+        getPutativeRootAddressedWithHash, InductiveMerkleTree.generateProof,
+        List.Vector.head_cons, BinaryTree.LeafData.get, BinaryTree.FullData.getRootValue]
+      exact congrArg (fun z => nodeHash .ofInternal z _) (ih dl (fun a => nodeHash (.ofLeft a)))
+  | ofRight idxRight ih =>
+    cases leaf_data_tree with
+    | internal dl dr =>
+      simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed,
+        getPutativeRootAddressedWithHash, InductiveMerkleTree.generateProof,
+        List.Vector.head_cons, BinaryTree.LeafData.get, BinaryTree.FullData.getRootValue]
+      exact congrArg (nodeHash .ofInternal _) (ih dr (fun a => nodeHash (.ofRight a)))
+
+/-- An address-tagged collision: two *distinct* input pairs with equal digest under
+the hash **at that address**. -/
+def AddressedCollision {s : Skeleton} (nodeHash : SkeletonInternalIndex s → α → α → α)
+    (w : SkeletonInternalIndex s × α × α × α × α) : Prop :=
+  (w.2.1, w.2.2.1) ≠ (w.2.2.2.1, w.2.2.2.2) ∧
+    nodeHash w.1 w.2.1 w.2.2.1 = nodeHash w.1 w.2.2.2.1 w.2.2.2.2
+
+/-- Walk two verifying branches at the same leaf index looking for the level at
+which they merge; return the collision **as data, tagged with its address**. -/
+def findCollisionAddressed : {s : Skeleton} → (nodeHash : SkeletonInternalIndex s → α → α → α) →
+    (idx : SkeletonLeafIndex s) → (proof₁ proof₂ : List.Vector α idx.depth) →
+    (x y : α) → Option (SkeletonInternalIndex s × α × α × α × α)
+  | _, _, .ofLeaf, _, _, _, _ => none
+  | _, nh, .ofLeft idxLeft, proof₁, proof₂, x, y =>
+    let subL1 := getPutativeRootAddressedWithHash (fun a => nh (.ofLeft a)) idxLeft x proof₁.tail
+    let subL2 := getPutativeRootAddressedWithHash (fun a => nh (.ofLeft a)) idxLeft y proof₂.tail
+    if (subL1, proof₁.head) = (subL2, proof₂.head) then
+      (findCollisionAddressed (fun a => nh (.ofLeft a)) idxLeft proof₁.tail proof₂.tail x y).map
+        (fun w => (.ofLeft w.1, w.2))
+    else if nh .ofInternal subL1 proof₁.head = nh .ofInternal subL2 proof₂.head then
+      some (.ofInternal, subL1, proof₁.head, subL2, proof₂.head)
+    else
+      none
+  | _, nh, .ofRight idxRight, proof₁, proof₂, x, y =>
+    let subR1 := getPutativeRootAddressedWithHash (fun a => nh (.ofRight a)) idxRight x proof₁.tail
+    let subR2 := getPutativeRootAddressedWithHash (fun a => nh (.ofRight a)) idxRight y proof₂.tail
+    if (proof₁.head, subR1) = (proof₂.head, subR2) then
+      (findCollisionAddressed (fun a => nh (.ofRight a)) idxRight proof₁.tail proof₂.tail x y).map
+        (fun w => (.ofRight w.1, w.2))
+    else if nh .ofInternal proof₁.head subR1 = nh .ofInternal proof₂.head subR2 then
+      some (.ofInternal, proof₁.head, subR1, proof₂.head, subR2)
+    else
+      none
+
+/-- **Soundness of the kernel**: anything returned is an address-tagged collision. -/
+theorem findCollisionAddressed_sound {s : Skeleton}
+    (nodeHash : SkeletonInternalIndex s → α → α → α) (idx : SkeletonLeafIndex s)
+    (proof₁ proof₂ : List.Vector α idx.depth) (x y : α)
+    (w : SkeletonInternalIndex s × α × α × α × α)
+    (hw : findCollisionAddressed nodeHash idx proof₁ proof₂ x y = some w) :
+    AddressedCollision nodeHash w := by
+  induction idx with
+  | ofLeaf => simp [findCollisionAddressed] at hw
+  | ofLeft idxLeft ih =>
+    rw [findCollisionAddressed] at hw
+    split at hw
+    · simp only [Option.map_eq_some_iff] at hw
+      obtain ⟨w', hw', rfl⟩ := hw
+      exact ih (fun a => nodeHash (.ofLeft a)) proof₁.tail proof₂.tail w' hw'
+    · rename_i hneq
+      split at hw
+      · rename_i heq
+        simp only [Option.some.injEq] at hw
+        subst hw
+        exact ⟨hneq, heq⟩
+      · simp at hw
+  | ofRight idxRight ih =>
+    rw [findCollisionAddressed] at hw
+    split at hw
+    · simp only [Option.map_eq_some_iff] at hw
+      obtain ⟨w', hw', rfl⟩ := hw
+      exact ih (fun a => nodeHash (.ofRight a)) proof₁.tail proof₂.tail w' hw'
+    · rename_i hneq
+      split at hw
+      · rename_i heq
+        simp only [Option.some.injEq] at hw
+        subst hw
+        exact ⟨hneq, heq⟩
+      · simp at hw
+
+/-- If two openings at the same index recompute the same root but the branches differ
+somewhere (in leaf value or path), `findCollisionAddressed` finds a collision: the
+walk only returns `none` when the two branches agree at every compared level, which
+forces the leaf values to agree. -/
+theorem findCollisionAddressed_isSome {s : Skeleton}
+    (nodeHash : SkeletonInternalIndex s → α → α → α) (idx : SkeletonLeafIndex s)
+    (proof₁ proof₂ : List.Vector α idx.depth) (x y : α)
+    (hroot : getPutativeRootAddressedWithHash nodeHash idx x proof₁
+      = getPutativeRootAddressedWithHash nodeHash idx y proof₂)
+    (hne : x ≠ y) :
+    (findCollisionAddressed nodeHash idx proof₁ proof₂ x y).isSome := by
+  induction idx with
+  | ofLeaf =>
+    simp only [vector_eq_nil] at hroot
+    exact absurd hroot hne
+  | ofLeft idxLeft ih =>
+    rw [findCollisionAddressed]
+    split
+    · rename_i hagree
+      simp only [Prod.mk.injEq] at hagree
+      simp only [Option.isSome_map]
+      exact ih (fun a => nodeHash (.ofLeft a)) proof₁.tail proof₂.tail hagree.1
+    · split
+      · simp
+      · rename_i hne'
+        exact absurd (by simpa [getPutativeRootAddressedWithHash] using hroot) hne'
+  | ofRight idxRight ih =>
+    rw [findCollisionAddressed]
+    split
+    · rename_i hagree
+      simp only [Prod.mk.injEq] at hagree
+      simp only [Option.isSome_map]
+      exact ih (fun a => nodeHash (.ofRight a)) proof₁.tail proof₂.tail hagree.2
+    · split
+      · simp
+      · rename_i hne'
+        exact absurd (by simpa [getPutativeRootAddressedWithHash] using hroot) hne'
+
+/-- **Binding, user-facing**: two openings of the same index recomputing the same
+root with distinct leaf values yield an address-tagged collision, as data. -/
+theorem getPutativeRootAddressedWithHash_binding_collision {s : Skeleton}
+    (nodeHash : SkeletonInternalIndex s → α → α → α) (idx : SkeletonLeafIndex s)
+    (proof₁ proof₂ : List.Vector α idx.depth) (x y : α)
+    (hroot : getPutativeRootAddressedWithHash nodeHash idx x proof₁
+      = getPutativeRootAddressedWithHash nodeHash idx y proof₂)
+    (hne : x ≠ y) :
+    ∃ w, findCollisionAddressed nodeHash idx proof₁ proof₂ x y = some w ∧
+      AddressedCollision nodeHash w := by
+  obtain ⟨w, hw⟩ := Option.isSome_iff_exists.mp
+    (findCollisionAddressed_isSome nodeHash idx proof₁ proof₂ x y hroot hne)
+  exact ⟨w, hw, findCollisionAddressed_sound nodeHash idx proof₁ proof₂ x y w hw⟩
+
+/-! ## Target orientation
+
+`findCollisionAddressed` is symmetric in its two openings. The theorems below break
+the symmetry for the honest-vs-adversarial configuration: when the first opening is
+the **honest** one (leaf and path generated from a built cache), the first endpoint
+of the returned collision is exactly the pair of child roots **stored in the cache at
+the returned address** — a value fixed by the (commitment-time) build, before any
+adversarial opening exists. This is the *directional* content a target-collision
+reduction needs, exposed as data; the probabilistic game packaging is deliberately
+kept separate. -/
+
+/-- The pair of child root values stored at an internal address of a cache. These
+are the honestly-precommitted hash inputs at that node. -/
+@[simp]
+def childPairAt : {s : Skeleton} → FullData α s → SkeletonInternalIndex s → α × α
+  | _, .internal _ L R, .ofInternal => (L.getRootValue, R.getRootValue)
+  | _, .internal _ L _, .ofLeft a => childPairAt L a
+  | _, .internal _ _ R, .ofRight a => childPairAt R a
+
+/-- **Orientation**: against an honest first opening, the collision's first endpoint
+is the precommitted child pair at the returned address. -/
+theorem findCollisionAddressed_oriented {s : Skeleton}
+    (nodeHash : SkeletonInternalIndex s → α → α → α) (ld : LeafData α s)
+    (idx : SkeletonLeafIndex s) (y : α) (proof₂ : List.Vector α idx.depth)
+    (hroot : getPutativeRootAddressedWithHash nodeHash idx y proof₂
+      = (buildMerkleTreeAddressedWithHash ld nodeHash).getRootValue)
+    (hne : ld.get idx ≠ y) :
+    ∃ (a : SkeletonInternalIndex s) (c : α × α),
+      findCollisionAddressed nodeHash idx
+        (InductiveMerkleTree.generateProof
+          (buildMerkleTreeAddressedWithHash ld nodeHash) idx) proof₂
+        (ld.get idx) y
+      = some (a, (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a).1,
+          (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a).2,
+          c.1, c.2) := by
+  induction idx with
+  | ofLeaf =>
+    cases ld with
+    | leaf v =>
+      simp only [getPutativeRootAddressedWithHash, buildMerkleTreeAddressedWithHash,
+        populateUpAddressed, FullData.getRootValue_leaf] at hroot
+      exact absurd hroot.symm (by simpa using hne)
+  | ofLeft idxLeft ih =>
+    cases ld with
+    | internal dl dr =>
+      have hsub : getPutativeRootAddressedWithHash (fun a => nodeHash (.ofLeft a)) idxLeft
+          (dl.get idxLeft)
+          (InductiveMerkleTree.generateProof
+            (populateUpAddressed (fun a => nodeHash (.ofLeft a)) dl) idxLeft)
+        = (populateUpAddressed (fun a => nodeHash (.ofLeft a)) dl).getRootValue :=
+        addressed_functional_completeness idxLeft dl (fun a => nodeHash (.ofLeft a))
+      have hroot' : nodeHash .ofInternal
+          (getPutativeRootAddressedWithHash (fun a => nodeHash (.ofLeft a)) idxLeft y
+            proof₂.tail) proof₂.head
+        = nodeHash .ofInternal
+            (populateUpAddressed (fun a => nodeHash (.ofLeft a)) dl).getRootValue
+            (populateUpAddressed (fun a => nodeHash (.ofRight a)) dr).getRootValue := by
+        simpa only [getPutativeRootAddressedWithHash, buildMerkleTreeAddressedWithHash,
+          populateUpAddressed, FullData.internal_getRootValue] using hroot
+      rw [findCollisionAddressed]
+      split
+      · rename_i hagree
+        simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed,
+          InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree,
+          SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons,
+          BinaryTree.LeafData.get, hsub, Prod.mk.injEq] at hagree
+        obtain ⟨a', c, hwalk⟩ := ih (fun a => nodeHash (.ofLeft a)) dl proof₂.tail
+          (show getPutativeRootAddressedWithHash (fun a => nodeHash (.ofLeft a)) idxLeft y
+              proof₂.tail
+            = (buildMerkleTreeAddressedWithHash dl (fun a => nodeHash (.ofLeft a))).getRootValue
+            from hagree.1.symm)
+          (by simpa using hne)
+        refine ⟨.ofLeft a', c, ?_⟩
+        simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed,
+          InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree,
+          SkeletonLeafIndex.depth, List.Vector.tail_cons,
+          BinaryTree.LeafData.get] at hwalk ⊢
+        rw [hwalk]
+        simp [childPairAt]
+      · split
+        · refine ⟨.ofInternal, (getPutativeRootAddressedWithHash (fun a => nodeHash (.ofLeft a))
+            idxLeft y proof₂.tail, proof₂.head), ?_⟩
+          simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed,
+            InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree,
+            SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons,
+            BinaryTree.LeafData.get, hsub, childPairAt]
+        · rename_i hne2
+          refine absurd ?_ hne2
+          simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed,
+            InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree,
+            SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons,
+            BinaryTree.LeafData.get, hsub]
+          exact hroot'.symm
+  | ofRight idxRight ih =>
+    cases ld with
+    | internal dl dr =>
+      have hsub : getPutativeRootAddressedWithHash (fun a => nodeHash (.ofRight a)) idxRight
+          (dr.get idxRight)
+          (InductiveMerkleTree.generateProof
+            (populateUpAddressed (fun a => nodeHash (.ofRight a)) dr) idxRight)
+        = (populateUpAddressed (fun a => nodeHash (.ofRight a)) dr).getRootValue :=
+        addressed_functional_completeness idxRight dr (fun a => nodeHash (.ofRight a))
+      have hroot' : nodeHash .ofInternal proof₂.head
+          (getPutativeRootAddressedWithHash (fun a => nodeHash (.ofRight a)) idxRight y
+            proof₂.tail)
+        = nodeHash .ofInternal
+            (populateUpAddressed (fun a => nodeHash (.ofLeft a)) dl).getRootValue
+            (populateUpAddressed (fun a => nodeHash (.ofRight a)) dr).getRootValue := by
+        simpa only [getPutativeRootAddressedWithHash, buildMerkleTreeAddressedWithHash,
+          populateUpAddressed, FullData.internal_getRootValue] using hroot
+      rw [findCollisionAddressed]
+      split
+      · rename_i hagree
+        simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed,
+          InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree,
+          SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons,
+          BinaryTree.LeafData.get, hsub, Prod.mk.injEq] at hagree
+        obtain ⟨a', c, hwalk⟩ := ih (fun a => nodeHash (.ofRight a)) dr proof₂.tail
+          (show getPutativeRootAddressedWithHash (fun a => nodeHash (.ofRight a)) idxRight y
+              proof₂.tail
+            = (buildMerkleTreeAddressedWithHash dr (fun a => nodeHash (.ofRight a))).getRootValue
+            from hagree.2.symm)
+          (by simpa using hne)
+        refine ⟨.ofRight a', c, ?_⟩
+        simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed,
+          InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree,
+          SkeletonLeafIndex.depth, List.Vector.tail_cons,
+          BinaryTree.LeafData.get] at hwalk ⊢
+        rw [hwalk]
+        simp [childPairAt]
+      · split
+        · refine ⟨.ofInternal, (proof₂.head, getPutativeRootAddressedWithHash
+            (fun a => nodeHash (.ofRight a)) idxRight y proof₂.tail), ?_⟩
+          simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed,
+            InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree,
+            SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons,
+            BinaryTree.LeafData.get, hsub, childPairAt]
+        · rename_i hne2
+          refine absurd ?_ hne2
+          simp only [buildMerkleTreeAddressedWithHash, populateUpAddressed,
+            InductiveMerkleTree.generateProof, FullData.leftSubtree, FullData.rightSubtree,
+            SkeletonLeafIndex.depth, List.Vector.tail_cons, List.Vector.head_cons,
+            BinaryTree.LeafData.get, hsub]
+          exact hroot'.symm
+
+omit [DecidableEq α] in
+/-- **Oriented binding, user-facing**: an adversarial opening that verifies against an
+honestly built root with a different leaf value yields a collision whose first
+endpoint is the honestly-precommitted child pair at the tagged address — the
+directional configuration a target-collision reduction consumes. -/
+theorem addressed_oriented_binding {s : Skeleton}
+    (nodeHash : SkeletonInternalIndex s → α → α → α) (ld : LeafData α s)
+    (idx : SkeletonLeafIndex s) (y : α) (proof₂ : List.Vector α idx.depth)
+    (hroot : getPutativeRootAddressedWithHash nodeHash idx y proof₂
+      = (buildMerkleTreeAddressedWithHash ld nodeHash).getRootValue)
+    (hne : ld.get idx ≠ y) :
+    ∃ (a : SkeletonInternalIndex s) (c : α × α),
+      (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a) ≠ c ∧
+      nodeHash a (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a).1
+          (childPairAt (buildMerkleTreeAddressedWithHash ld nodeHash) a).2
+        = nodeHash a c.1 c.2 := by
+  letI : DecidableEq α := Classical.decEq α
+  obtain ⟨a, c, hwalk⟩ :=
+    findCollisionAddressed_oriented nodeHash ld idx y proof₂ hroot hne
+  have hcol := findCollisionAddressed_sound nodeHash idx _ proof₂ (ld.get idx) y _ hwalk
+  exact ⟨a, c, by simpa [AddressedCollision, Prod.ext_iff] using hcol.1,
+    by simpa [AddressedCollision] using hcol.2⟩
+
+/-! ## Instances: three hash disciplines, one engine
+
+The three hash disciplines are specializations of `nodeHash`; the theorems above
+specialize with them. The theorems below are the **subsumption certificates** for the
+constant instance: they exhibit the unaddressed `MerkleTree.Inductive` API as this
+engine specialized, at the level of its computations
+(`populateUpAddressed_const`, `getPutativeRootAddressed_const`,
+`buildMerkleTreeAddressed_const`), its completeness theorem
+(`functional_completeness_of_addressed`, derived here rather than reproved) and its
+constructive collision kernel (`findCollisionAddressed_const`: address erasure sends
+one to the other on the nose). The subsumption is propositional, not definitional —
+see the scope note in the module header. The level-separated (`Tweaked`) development
+factors through `SkeletonInternalIndex.subtreeDepth` and is *definitionally* an instance
+(`levelNodeHash_eq_addressed` is `rfl`). -/
+
+section Instances
+
+omit [DecidableEq α] in
+/-- **Ordinary instance**: a constant `nodeHash` recovers the unaddressed
+putative-root computation. -/
+theorem getPutativeRootAddressed_const (h : α → α → α) {s : Skeleton}
+    (idx : SkeletonLeafIndex s) (x : α) (proof : List.Vector α idx.depth) :
+    getPutativeRootAddressedWithHash (s := s) (fun _ => h) idx x proof
+      = InductiveMerkleTree.getPutativeRootWithHash idx x proof h := by
+  induction idx with
+  | ofLeaf => rfl
+  | ofLeft idxLeft ih => simp [getPutativeRootAddressedWithHash, ih]
+  | ofRight idxRight ih => simp [getPutativeRootAddressedWithHash, ih]
+
+omit [DecidableEq α] in
+/-- **Ordinary instance**: a constant `nodeHash` recovers the unaddressed cache
+construction. -/
+theorem populateUpAddressed_const (h : α → α → α) {s : Skeleton}
+    (ld : LeafData α s) :
+    populateUpAddressed (fun _ => h) ld = BinaryTree.populateUp ld h := by
+  induction ld with
+  | leaf v => rfl
+  | internal dl dr ihl ihr => simp [populateUpAddressed, BinaryTree.populateUp, ihl, ihr]
+
+omit [DecidableEq α] in
+/-- **Ordinary instance**: a constant `nodeHash` recovers the unaddressed build. -/
+theorem buildMerkleTreeAddressed_const (h : α → α → α) {s : Skeleton}
+    (ld : LeafData α s) :
+    buildMerkleTreeAddressedWithHash ld (fun _ => h)
+      = InductiveMerkleTree.buildMerkleTreeWithHash ld h :=
+  populateUpAddressed_const h ld
+
+omit [DecidableEq α] in
+/-- **Subsumption certificate (completeness)**: the unaddressed completeness theorem
+is a consequence of the engine's, at the constant instance. This is not a second
+proof of completeness — it is the first one, specialized. -/
+theorem functional_completeness_of_addressed (h : α → α → α) {s : Skeleton}
+    (idx : SkeletonLeafIndex s) (ld : LeafData α s) :
+    InductiveMerkleTree.getPutativeRootWithHash idx (ld.get idx)
+        (InductiveMerkleTree.generateProof
+          (InductiveMerkleTree.buildMerkleTreeWithHash ld h) idx) h
+      = (InductiveMerkleTree.buildMerkleTreeWithHash ld h).getRootValue := by
+  rw [← buildMerkleTreeAddressed_const h ld, ← getPutativeRootAddressed_const h]
+  exact addressed_functional_completeness idx ld (fun _ => h)
+
+/-- **Subsumption certificate (collision kernel)**: erasing the address tag from the
+engine's constructive collision walk yields *exactly* the unaddressed `findCollision`.
+So the two collision kernels are not parallel implementations that happen to agree on
+their statements — they are one function, up to the address decoration. -/
+theorem findCollisionAddressed_const (h : α → α → α) {s : Skeleton}
+    (idx : SkeletonLeafIndex s) (proof₁ proof₂ : List.Vector α idx.depth) (x y : α) :
+    (findCollisionAddressed (fun _ => h) idx proof₁ proof₂ x y).map (fun w => w.2)
+      = InductiveMerkleTree.findCollision h idx proof₁ proof₂ x y := by
+  induction idx with
+  | ofLeaf => rfl
+  | ofLeft idxLeft ih =>
+    rw [findCollisionAddressed, InductiveMerkleTree.findCollision]
+    simp only [getPutativeRootAddressed_const, dite_eq_ite]
+    split
+    · rw [Option.map_map]; exact ih proof₁.tail proof₂.tail
+    · split <;> rfl
+  | ofRight idxRight ih =>
+    rw [findCollisionAddressed, InductiveMerkleTree.findCollision]
+    simp only [getPutativeRootAddressed_const, dite_eq_ite]
+    split
+    · rw [Option.map_map]; exact ih proof₁.tail proof₂.tail
+    · split <;> rfl
+
+/-- **Level-separated instance**: hash through the depth of the addressed subtree.
+This is the discipline of the `Tweaked` development: per-level domain separation. -/
+def levelNodeHash {PkSeed Tweak Y : Type} (th : TweakableHash PkSeed Tweak (Y × Y) Y)
+    (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton} : SkeletonInternalIndex s → Y → Y → Y :=
+  fun a l r => th.eval pk (tweakAt a.subtreeDepth) (l, r)
+
+/-- **Fully-addressed (XMSS-style) instance**: hash through an arbitrary map out of
+the full typed address — per-node domain separation. Any concrete addressing scheme
+(layer, horizontal index, domain tag) factors through `tweakOf`; nothing about the
+address is discarded before the user's map is applied. -/
+def addressedNodeHash {PkSeed Tweak Y : Type} (th : TweakableHash PkSeed Tweak (Y × Y) Y)
+    (pk : PkSeed) {s : Skeleton} (tweakOf : SkeletonInternalIndex s → Tweak) :
+    SkeletonInternalIndex s → Y → Y → Y :=
+  fun a l r => th.eval pk (tweakOf a) (l, r)
+
+/-- The level instance factors through the fully-addressed one — level separation is
+the special case `tweakOf = tweakAt ∘ subtreeDepth`. -/
+theorem levelNodeHash_eq_addressed {PkSeed Tweak Y : Type}
+    (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed) (tweakAt : ℕ → Tweak)
+    {s : Skeleton} :
+    levelNodeHash th pk tweakAt (s := s)
+      = addressedNodeHash th pk (fun a => tweakAt a.subtreeDepth) := rfl
+
+end Instances
+
+end AddressedMerkleTree
diff --git a/VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean b/VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean
new file mode 100644
index 00000000..c26d7e61
--- /dev/null
+++ b/VCVio/CryptoFoundations/MerkleTree/Addressed/Level.lean
@@ -0,0 +1,76 @@
+/-
+Copyright (c) 2026 Richard Goodman. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Richard Goodman
+-/
+
+module
+public import VCVio.CryptoFoundations.MerkleTree.Addressed.Basic
+
+/-! # Level-Separated Merkle Trees, as an instance of the addressed engine
+
+Per-**level** domain separation — every node at the same subtree depth hashes under
+the same tweak — obtained by specializing the node-addressed engine's `nodeHash`
+through `SkeletonInternalIndex.subtreeDepth`. Nothing here is proven from scratch: building,
+completeness, and the (oriented) collision kernel are the engine's theorems at
+`levelNodeHash`.
+
+This is deliberately **not** the XMSS / SLH-DSA layout, which separates by full node
+address; that is the engine itself (`addressedNodeHash`), of which this file is the
+depth-collapsed special case (`levelNodeHash_eq_addressed`).
+-/
+
+@[expose] public section
+
+namespace AddressedMerkleTree
+
+open BinaryTree InductiveMerkleTree
+
+variable {PkSeed Tweak Y : Type} [DecidableEq Y]
+
+/-- Build a level-separated Merkle tree: node at subtree-depth `d` hashes under
+`tweakAt d`. -/
+def buildMerkleTreeLevel (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed)
+    (tweakAt : ℕ → Tweak) {s : Skeleton} (ld : LeafData Y s) : FullData Y s :=
+  buildMerkleTreeAddressedWithHash ld (levelNodeHash th pk tweakAt)
+
+/-- Putative-root recomputation for the level-separated tree. -/
+def getPutativeRootLevel (th : TweakableHash PkSeed Tweak (Y × Y) Y) (pk : PkSeed)
+    (tweakAt : ℕ → Tweak) {s : Skeleton} (idx : SkeletonLeafIndex s) (leafValue : Y)
+    (proof : List.Vector Y idx.depth) : Y :=
+  getPutativeRootAddressedWithHash (levelNodeHash th pk tweakAt) idx leafValue proof
+
+omit [DecidableEq Y] in
+/-- Completeness for the level-separated tree — the engine's completeness at
+`levelNodeHash`. -/
+theorem level_functional_completeness (th : TweakableHash PkSeed Tweak (Y × Y) Y)
+    (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton}
+    (idx : SkeletonLeafIndex s) (ld : LeafData Y s) :
+    getPutativeRootLevel th pk tweakAt idx (ld.get idx)
+      (generateProof (buildMerkleTreeLevel th pk tweakAt ld) idx)
+    = (buildMerkleTreeLevel th pk tweakAt ld).getRootValue := by
+  letI : DecidableEq Y := Classical.decEq Y
+  exact addressed_functional_completeness idx ld (levelNodeHash th pk tweakAt)
+
+omit [DecidableEq Y] in
+/-- **Oriented binding** for the level-separated tree — the engine's oriented
+binding at `levelNodeHash`: an adversarial opening verifying against an honestly
+built root with a different leaf yields two distinct pairs with equal digest under
+the tweak of the collision's level, the first pair being the honestly-precommitted
+one at the tagged address. -/
+theorem level_oriented_binding (th : TweakableHash PkSeed Tweak (Y × Y) Y)
+    (pk : PkSeed) (tweakAt : ℕ → Tweak) {s : Skeleton} (ld : LeafData Y s)
+    (idx : SkeletonLeafIndex s) (y : Y) (proof₂ : List.Vector Y idx.depth)
+    (hroot : getPutativeRootLevel th pk tweakAt idx y proof₂
+      = (buildMerkleTreeLevel th pk tweakAt ld).getRootValue)
+    (hne : ld.get idx ≠ y) :
+    ∃ (a : SkeletonInternalIndex s) (c : Y × Y),
+      (childPairAt (buildMerkleTreeLevel th pk tweakAt ld) a) ≠ c ∧
+      th.eval pk (tweakAt a.subtreeDepth)
+          ((childPairAt (buildMerkleTreeLevel th pk tweakAt ld) a).1,
+           (childPairAt (buildMerkleTreeLevel th pk tweakAt ld) a).2)
+        = th.eval pk (tweakAt a.subtreeDepth) (c.1, c.2) := by
+  letI : DecidableEq Y := Classical.decEq Y
+  exact addressed_oriented_binding (levelNodeHash th pk tweakAt) ld idx y proof₂ hroot hne
+
+end AddressedMerkleTree