diff --git a/verification/Proofs/AxiomCheck.lean b/verification/Proofs/AxiomCheck.lean
index b587815..baa0878 100644
--- a/verification/Proofs/AxiomCheck.lean
+++ b/verification/Proofs/AxiomCheck.lean
@@ -7,6 +7,7 @@ import Proofs.Consistency
 import Proofs.Binding3
 import Proofs.Refactor
 import Proofs.Theorem3
+import Proofs.PinStore
 #print axioms LTLAcc.domsep
 #print axioms LTLAcc.kbelow_pos
 #print axioms LTLAcc.kbelow_lt
@@ -36,3 +37,7 @@ import Proofs.Theorem3
 #print axioms LTLAcc.extractCons
 #print axioms LTLAcc.extractCons_correct
 #print axioms LTLAcc.extractCons_nonvacuous
+#print axioms LTLAcc.pinAccept_monotone
+#print axioms LTLAcc.pin_prefix_correct
+#print axioms LTLAcc.fork_distinct
+#print axioms LTLAcc.pin_prefix_nonvacuous
diff --git a/verification/Proofs/AxiomCheck.olean b/verification/Proofs/AxiomCheck.olean
index 08b26f1..bb38c86 100644
Binary files a/verification/Proofs/AxiomCheck.olean and b/verification/Proofs/AxiomCheck.olean differ
diff --git a/verification/Proofs/PinStore.lean b/verification/Proofs/PinStore.lean
new file mode 100644
index 0000000..0996909
--- /dev/null
+++ b/verification/Proofs/PinStore.lean
@@ -0,0 +1,93 @@
+/- S6 — **Proposition 1 (Pin-store safety)**, the Merkle-layer contribution.
+
+   The consumer pin store (§5.4) as a transition predicate; monotonicity is
+   definitional, and prefix-ordering — the substantive part — reduces to
+   Theorem 3 (grow) and the whole-tree Lemma 2 (same-size), stated as an
+   explicit named-extractor collision (non-vacuous), never a bare ∃.
+
+   SCOPE: Ed25519 EUF-CMA is NOT in this corpus (signatures are abstract).
+   Part (2) of the paper's Prop 1 — that two conflicting signed heads are
+   *transferable* evidence — is a signature-layer fact; the Merkle layer
+   contributes only that different roots at equal size commit to different
+   content (fork_distinct). This boundary is documented, not smuggled. -/
+import Proofs.Theorem3
+
+namespace LTLAcc
+
+/-- The pin-store accept predicate (§5.4): same size ⇒ root must match;
+    smaller ⇒ reject (rollback); larger ⇒ a consistency proof from the
+    pinned head must verify. Mirrors sthstore.py. -/
+def pinAccept (n : Nat) (r : Hash) (n' : Nat) (r' : Hash) (C : List Hash) : Prop :=
+  if n' = n then r' = r
+  else if n' < n then False
+  else ConsRec n n' C true r = some (r, r')
+
+/-- **Monotonicity (size)**: an accepted step never shrinks the pin. -/
+theorem pinAccept_monotone (n : Nat) (r : Hash) (n' : Nat) (r' : Hash)
+    (C : List Hash) (h : pinAccept n r n' r' C) : n ≤ n' := by
+  unfold pinAccept at h
+  by_cases he : n' = n
+  · omega
+  · by_cases hl : n' < n
+    · simp [he, hl] at h
+    · omega
+
+/-- The pin-store collision extractor: whole-tree descent at equal size,
+    else the consistency extractor. -/
+noncomputable def pinExtract (n n' : Nat) (C : List Hash)
+    (D D' : List Bytes) : List UInt8 × List UInt8 :=
+  if n' = n then extractMTH D D' else extractCons n C D D'
+
+/-- **Prefix-ordering (monotonicity, content)**: if the pin advances from an
+    honest head of `D` to an honest head of `D'` but `D` is NOT the prefix
+    of `D'` of its length, then `pinExtract` outputs a genuine collision.
+    (Explicit form ⇒ non-vacuous; this is the paper's Prop 1(1).) -/
+theorem pin_prefix_correct (n n' : Nat) (r r' : Hash) (C : List Hash)
+    (D D' : List Bytes)
+    (hstep : pinAccept n r n' r' C)
+    (hDlen : D.length = n) (hDr : MTH D = r)
+    (hD'len : D'.length = n') (hD'r : MTH D' = r')
+    (hn0 : 0 < n) (hne : D ≠ D'.take n) :
+    IsCollision (pinExtract n n' C D D').1 (pinExtract n n' C D D').2 := by
+  unfold pinAccept at hstep
+  by_cases he : n' = n
+  · -- same size: r' = r ⇒ MTH D' = MTH D; D ≠ D'.take n = D' (len n)
+    simp only [if_pos he] at hstep
+    rw [pinExtract]; simp only [if_pos he]
+    have hlen : D.length = D'.length := by rw [hDlen, hD'len, he]
+    have hroot : MTH D = MTH D' := by rw [hDr, hD'r, hstep]
+    have hne' : D ≠ D' := by
+      intro h; apply hne; rw [h]
+      have hta : D'.take n = D' := by apply take_all; rw [hD'len]; exact he
+      rw [hta]
+    exact extractMTH_correct D D' hlen hne' hroot
+  · by_cases hl : n' < n
+    · simp [he, hl] at hstep
+    · -- grow: ConsRec n n' C true r = some (r, r')
+      have hgrow : ConsRec n n' C true r = some (r, r') := by
+        simp only [he, hl, if_false] at hstep; exact hstep
+      rw [pinExtract]; simp only [if_neg he]
+      have hle : n ≤ D'.length := by omega
+      have hacc : ConsRec n D'.length C true (MTH D) = some (MTH D, MTH D') := by
+        rw [hDr, hD'r, hD'len]; exact hgrow
+      exact extractCons_correct n C D D' hDlen hn0 hle hne hacc
+
+/-- **Fork observation (Merkle-layer share of Prop 1(2))**: two honest
+    heads of equal size with different roots commit to different content.
+    (Transferable-evidence via EUF-CMA is signature-layer, out of scope.) -/
+theorem fork_distinct (n : Nat) (r r' : Hash) (D D' : List Bytes)
+    (hDlen : D.length = n) (hD'len : D'.length = n)
+    (hDr : MTH D = r) (hD'r : MTH D' = r') (hrne : r ≠ r') : D ≠ D' := by
+  intro h; apply hrne; rw [← hDr, ← hD'r, h]
+
+/-- Permanent non-vacuity witness for pin_prefix_correct: on an honest
+    non-fork step (D IS the prefix), the extractor output is not a
+    collision. Uses the same-size identity D = D' = [[7]]. -/
+theorem pin_prefix_nonvacuous :
+    ¬ IsCollision (pinExtract 1 1 [] [([7] : List UInt8)] [([7] : List UInt8)]).1
+                  (pinExtract 1 1 [] [([7] : List UInt8)] [([7] : List UInt8)]).2 := by
+  rw [pinExtract]; simp only [if_pos rfl]
+  rw [extractMTH]; simp only [List.length_singleton, if_pos (by omega : (1:Nat) ≤ 1)]
+  intro hcol; exact hcol.1 rfl
+
+end LTLAcc
diff --git a/verification/Proofs/PinStore.olean b/verification/Proofs/PinStore.olean
new file mode 100644
index 0000000..338b462
Binary files /dev/null and b/verification/Proofs/PinStore.olean differ
diff --git a/verification/check.sh b/verification/check.sh
index 06f318e..0563d19 100755
--- a/verification/check.sh
+++ b/verification/check.sh
@@ -17,7 +17,7 @@ export LEAN_MEM_MB="${LEAN_MEM_MB:-4096}"
 CORES="${LEAN_MAX_CORES:-0-3}"
 
 GEN_MODULES=( LTLAcc/HashExternal )
-PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor Theorem3 )
+PROOFS=( Basic Completeness Extract Descent Consistency Binding3 Refactor Theorem3 PinStore )
 
 # Certificates and their exact expected cones (observed at first green
 # compile, 2026-07-10; any drift in EITHER direction is a failure).
@@ -51,6 +51,10 @@ declare -A CONES=(
   [LTLAcc.extractCons]="propext, LTLAcc.sha256, Quot.sound"
   [LTLAcc.extractCons_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
   [LTLAcc.extractCons_nonvacuous]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.pinAccept_monotone]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.pin_prefix_correct]="propext, Classical.choice, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.fork_distinct]="propext, LTLAcc.sha256, Quot.sound"
+  [LTLAcc.pin_prefix_nonvacuous]="propext, LTLAcc.sha256, Quot.sound"
 )
 
 free -m | awk '/Mem:/{if($7<2048){print "FATAL: <2GB RAM available — refusing to compile"; exit 1}}'