S6: Proposition 1 (pin-store safety) — the last theorem, Merkle-layer share

The consumer pin store (§5.4) as a transition predicate; the paper's
Prop 1(1) fully mechanized:
- pinAccept: same-size ⇒ root match; smaller ⇒ reject (rollback); larger
  ⇒ consistency proof verifies. Mirrors sthstore.py.
- pinAccept_monotone: an accepted step never shrinks the pin (definitional).
- pin_prefix_correct: an honest advance where D is NOT the prefix of D'
  makes pinExtract output a genuine collision — same-size routes to
  extractMTH (whole-tree Lemma 2), grow routes to extractCons (Theorem 3).
  Explicit named-extractor form ⇒ non-vacuous (pin_prefix_nonvacuous
  pinned).
- fork_distinct: the Merkle share of Prop 1(2) — different roots at equal
  size commit to different content. EUF-CMA transferable-evidence is
  signature-layer, OUT OF SCOPE and documented in the file header (not
  smuggled).

Cones: single hash axiom (pin_prefix_correct adds Classical.choice via
functional induction downstream). 33 certs green. Fable statement-audit:
matches paper Prop 1(1); Prop 1(2) scope-bounded honestly. LTL untouched.

Every §6 statement is now kernel-checked: Lemma 1, Theorems 1-3,
whole-tree Lemma 2, Proposition 1. Remaining: S7 fidelity, S8 freeze.

Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>

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

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

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}}'