diff --git a/AGENTS.md b/AGENTS.md
index 1317427e..2c2055e2 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -124,6 +124,7 @@ Target: `formal/SilverSight/HachimojiN8.lean` — provable by `native_decide` on
 | PIST/YangBaxter.lean | Complete (Layer 2d) | 0 |
 | PIST/Tdoku16D.lean | Complete (reflexive convergence 336) | 0 |
 | PIST/CrossDomainSynthesis.lean | Complete (Rydberg defect & SC band) | 0 |
+| PIST/MultiSurfacePacker.lean | Complete (Lagrangian decision logic) | 0 |
 | PIST/UnifiedCovariant.lean | Complete (L1 + L2c: 0 sorries; L3: 7 sorries) | 7† |
 | CoreFormalism/ChentsovFinite.lean | Complete (3 axioms) | 0 |
 | AVMIsa/Types.lean | Complete | 0 |
diff --git a/formal/SilverSight/PIST/MultiSurfacePacker.lean b/formal/SilverSight/PIST/MultiSurfacePacker.lean
new file mode 100644
index 00000000..3eb856d3
--- /dev/null
+++ b/formal/SilverSight/PIST/MultiSurfacePacker.lean
@@ -0,0 +1,204 @@
+-- MultiSurfacePacker.lean — Lean decision logic for ΔΦΓΛ Lagrangian
+--
+-- Formalizes the Multi-Surface Packing Lagrangian optimization and coherence gating
+-- using pure, definitionally-reducible Q16_16 fixed-point arithmetic.
+
+import SilverSight.FixedPoint
+import Mathlib.Tactic
+
+namespace SilverSight.PIST.MultiSurfacePacker
+
+open SilverSight.FixedPoint
+open SilverSight.FixedPoint.Q16_16
+
+-- ============================================================
+-- §1  COST & LAGRANGIAN STRUCTURES
+-- ============================================================
+
+structure DeltaSurfaceCost where
+  deltaL1 : Q16_16
+  blockCount : Nat
+  avgCompressibility : Q16_16
+  deriving Repr, Inhabited, DecidableEq
+
+structure SpectralSurfaceCost where
+  sampleCount : Q16_16
+  coherence : Q16_16
+  spectralEnergy : Q16_16
+  deriving Repr, Inhabited, DecidableEq
+
+structure ProgramSurfaceCost where
+  descriptionLength : Q16_16
+  complexity : Q16_16
+  codonCount : Nat
+  deriving Repr, Inhabited, DecidableEq
+
+structure MultiSurfaceLagrangian where
+  deltaCost : Q16_16
+  spectralCost : Q16_16
+  programCost : Q16_16
+  alpha : Q16_16
+  beta : Q16_16
+  total : Q16_16
+  deriving Repr, Inhabited, DecidableEq
+
+/-- Compute the Lagrangian: L = deltaL1 + alpha * sampleCount + beta * descriptionLength. -/
+def computeLagrangian (delta : DeltaSurfaceCost) (spectral : SpectralSurfaceCost)
+    (program : ProgramSurfaceCost) (alpha beta : Q16_16) : MultiSurfaceLagrangian :=
+  let spectralWeighted := mul alpha spectral.sampleCount
+  let programWeighted := mul beta program.descriptionLength
+  let total := add delta.deltaL1 (add spectralWeighted programWeighted)
+  { deltaCost := delta.deltaL1
+    spectralCost := spectralWeighted
+    programCost := programWeighted
+    alpha := alpha
+    beta := beta
+    total := total }
+
+-- ============================================================
+-- §2  COHERENCE OVERLAP & GATING
+-- ============================================================
+
+/-- Custom definitionally-reducible index lookup for List. -/
+def get? {α : Type} : List α → Nat → Option α
+  | [], _ => none
+  | x :: _, 0 => some x
+  | _ :: xs, n + 1 => get? xs n
+
+/-- Safely get element from list with default value. -/
+def getD (l : List Q16_16) (i : Nat) (default : Q16_16) : Q16_16 :=
+  match get? l i with
+  | some x => x
+  | none => default
+
+/-- Custom definitionally-reducible foldl with index for List. -/
+def foldlIdx {α β : Type} (f : β → Nat → α → β) (init : β) (l : List α) : β :=
+  let rec loop (i : Nat) (acc : β) : List α → β
+    | [] => acc
+    | x :: xs => loop (i + 1) (f acc i x) xs
+  loop 0 init l
+
+/-- Compute coherence overlap squared between two sample series. -/
+def coherenceOverlap (samplesA samplesB : List Q16_16) : Q16_16 :=
+  if samplesA.isEmpty ∨ samplesB.isEmpty then
+    zero
+  else
+    let m := min samplesA.length samplesB.length
+    let commonA := samplesA.take m
+    let commonB := samplesB.take m
+    if m = 0 then
+      zero
+    else
+      let sumA := commonA.foldl add zero
+      let sumB := commonB.foldl add zero
+      let meanA := div sumA (ofNat m)
+      let meanB := div sumB (ofNat m)
+      let dot := foldlIdx (fun acc i a =>
+        let aCentered := sub a meanA
+        let bCentered := sub (getD commonB i zero) meanB
+        add acc (mul aCentered bCentered)) zero commonA
+      let normA := commonA.foldl (fun acc a =>
+        let aC := sub a meanA
+        add acc (mul aC aC)) zero
+      let normB := commonB.foldl (fun acc b =>
+        let bC := sub b meanB
+        add acc (mul bC bC)) zero
+      if normA.toInt = 0 ∧ normB.toInt = 0 then
+        one
+      else
+        let denom := mul normA normB
+        if denom.toInt = 0 then
+          zero
+        else
+          div (mul dot dot) denom
+
+/-- Coherence gate: accepts if overlapSq >= 1 - epsilon. -/
+def coherenceGate (overlapSq : Q16_16) (epsilon : Q16_16) : Bool :=
+  let threshold := sub one epsilon
+  overlapSq ≥ threshold
+
+-- ============================================================
+-- §3  GCCL SWAP GATE & DECISIONS
+-- ============================================================
+
+structure GCDecision where
+  accept : Bool
+  reject : Bool
+  hold : Bool
+  quarantine : Bool
+  deriving Repr, Inhabited, DecidableEq
+
+/-- GCCL swap decision logic. -/
+def gcclSwapGate (oldCost newCost reconRisk : Q16_16) : GCDecision :=
+  let improvement := if oldCost > newCost then
+    sub oldCost newCost
+  else
+    zero
+  let admissible := improvement ≥ reconRisk
+  { accept := admissible
+    reject := ¬admissible
+    hold := ¬admissible
+    quarantine := false }
+
+-- ============================================================
+-- §4  RECEIPT STRUCTURE
+-- ============================================================
+
+structure MultiSurfaceReceipt where
+  schema : String := "multi_surface_packing_v1"
+  inputSize : Nat
+  deltaCost : Q16_16
+  spectralCost : Q16_16
+  programCost : Q16_16
+  totalLagrangian : Q16_16
+  coherencePassed : Bool
+  gcclPassed : Bool
+  decision : String
+  compressedSize : Nat
+  compressionRatio : Q16_16
+  claimBoundary : String := "multi-surface-packing-lean-core"
+  deriving Repr, Inhabited, DecidableEq
+
+def finalizeReceipt (receipt : MultiSurfaceReceipt) : MultiSurfaceReceipt :=
+  receipt
+
+-- ============================================================
+-- §5  THEOREMS
+-- ============================================================
+
+theorem coherenceGateAcceptsIdentical :
+    coherenceGate one (ofRawInt 3277) = true := by
+  decide
+
+theorem coherenceGateRejectsOrthogonal :
+    coherenceGate zero (ofRawInt 3277) = false := by
+  decide
+
+theorem gcclRejectsExpansion :
+    gcclSwapGate (ofNat 100) (ofNat 200) (ofNat 500) =
+    { accept := false, reject := true, hold := true, quarantine := false } := by
+  decide
+
+-- ============================================================
+-- §6  EXAMPLES
+-- ============================================================
+
+def exampleDelta : DeltaSurfaceCost := {
+  deltaL1 := ofNat 12800
+  blockCount := 4
+  avgCompressibility := ofNat 32768
+}
+
+def exampleSpectral : SpectralSurfaceCost := {
+  sampleCount := ofNat 256
+  coherence := ofNat 55705
+  spectralEnergy := ofNat 65536
+}
+
+def exampleProgram : ProgramSurfaceCost := {
+  descriptionLength := ofNat 500
+  complexity := ofNat 29491
+  codonCount := 150
+}
+
+end SilverSight.PIST.MultiSurfacePacker
diff --git a/lakefile.lean b/lakefile.lean
index 3ab1f01c..2c923659 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -67,6 +67,7 @@ lean_lib «SilverSightRRC» where
     `SilverSight.PIST.YangBaxter,
     `SilverSight.PIST.Tdoku16D,
     `SilverSight.PIST.CrossDomainSynthesis,
+    `SilverSight.PIST.MultiSurfacePacker,
     `SilverSight.RRCLogogramProjection,
     `SilverSight.ReceiptCore,
     `SilverSight.RRC.Emit,