diff --git a/formal/SilverSight/GCCL.lean b/formal/SilverSight/GCCL.lean
index fc8695ab..410da33d 100644
--- a/formal/SilverSight/GCCL.lean
+++ b/formal/SilverSight/GCCL.lean
@@ -249,6 +249,181 @@ theorem lawful_all_pass (t : Transition) :
     t.decision = Decision.accept := by
   simp [isLawful]
 
+/-! §8b The Five Control Filters (Admit Pipeline)
+
+  The GCCL gate decomposes into eight sub-checks, organized as the
+  five canonical control filters plus three bookkeeping gates.
+
+  These began as meme-named handles on real mathematical machinery
+  (see "Meme Math That Pays Rent"). The jokes got parking passes;
+  they pay rent as formal admission gates.
+
+  Timeline of the COUCH family:
+
+  COUCH — "Super Freak" / Rick James / moving sofa problem
+    The original. A continuous oscillator with a joke name, formalized
+    as a Lean witness with 5 regimes and 28 theorems. Measures pressure
+    and hysteresis stability. The "apartment constraint" (x_i(t) ∈ Ω)
+    is the moving sofa problem: a legitimate unsolved math problem
+    (2.2195 ≤ S ≤ 2.8284). Rick James said "I'm in the apartment, not
+    touching the walls." That IS the constrained-manifold traversal.
+
+  Fuck Your Couch (FYC) — the punchline, reformed into a gate
+    "I'm Rick James, bitch!" → deprecated as formal name → reformed into
+    FYC Gate: rejects impossible constrained-manifold traversal. A
+    candidate route that claims it can navigate a topology that's
+    actually impossible gets rejected.
+
+  LoC/NES Monster — "Loch Ness Monster"
+    Locality-of-change check. Detects entropy smuggling via recurrence.
+    Wraps the set with a creature-feature theme.
+
+  Tree Fiddy — "I need about tree fiddy"
+    Cost bound. The budget beyond which the Loch Ness Monster takes your
+    money. Checks that the AngrySphinx cost (2^depth) is within budget.
+
+  BHOCS — "Big Hash of Certified Stuff"
+    Receipt/audit trail verification. The SHA-256 hash chain is intact.
+
+  Philosophy: "A joke can get a parking pass. It does not get tenure.
+  If it wants to stay in the stack, it has to pay rent."
+
+  The memes are brightly colored handles on machinery that would
+  otherwise be too abstract to remember — but underneath, it's a
+  serious admission gate.
+
+  Connection to GCCL law axes:
+    replay_valid     → Compression (round-trip)
+    byte_gain > 0    → Compression (actual reduction)
+    residual_declared → Residual (explicit loss)
+    LoC_NES_pass     → Cognitive (locality, no smuggling)
+    FYC_pass         → Geometric (traversable manifold)
+    COUCH_stable     → Geometric (pressure stability)
+    TreeFiddy_bounded → Cost (budget)
+    BHOCS_verified   → Receipt (audit trail)
+-/
+
+/-- A candidate transition X entering the admission pipeline. -/
+structure CandidateX where
+  /-- Replay produces identical output (determinism) -/
+  replayValid : Bool
+  /-- Net byte reduction > 0 (actual compression) -/
+  byteGain : Q16_16  -- positive means compression achieved
+  /-- Residual (loss) is explicitly declared, not hidden -/
+  residualDeclared : Bool
+  /-- Locality-of-change: no entropy smuggling via recurrence -/
+  locNesPass : Bool
+  /-- FYC: constrained-manifold traversal is geometrically possible -/
+  fycPass : Bool
+  /-- COUCH: pressure/hysteresis stability (the original gate) -/
+  couchStable : Bool
+  /-- Tree Fiddy: cost within budget (AngrySphinx 2^depth ≤ limit) -/
+  treeFiddyBounded : Bool
+  /-- BHOCS: receipt/audit trail (SHA-256 hash chain) verified -/
+  bhocsVerified : Bool
+  deriving Repr, DecidableEq, Inhabited
+
+/-- byteGain > 0 check: actual compression was achieved. -/
+def byteGainPositive (x : CandidateX) : Bool :=
+  x.byteGain > Q16_16.zero
+
+/-- The full Admit predicate — all eight gates must pass.
+
+    Admit(X) = replay_valid(X)
+             ∧ byte_gain(X) > 0
+             ∧ residual_declared(X)
+             ∧ LoC_NES_pass(X)
+             ∧ FYC_pass(X)
+             ∧ COUCH_stable(X)
+             ∧ TreeFiddy_bounded(X)
+             ∧ BHOCS_verified(X)
+
+    A candidate is admitted only if it survives all five control filters
+    plus the three bookkeeping gates. Each gate checks a different aspect
+    of lawfulness:
+
+    - replay_valid: the encoding is deterministic and reproducible
+    - byte_gain > 0: the candidate actually compresses (fewer collisions)
+    - residual_declared: the quantization loss is explicit (Q16_16 floor)
+    - LoC_NES_pass: locality of change (no rewriting the entire tree)
+    - FYC_pass: the braid structure is geometrically traversable
+    - COUCH_stable: the candidate's Omega is in the stable range
+    - TreeFiddy_bounded: AngrySphinx cost 2^depth ≤ budget
+    - BHOCS_verified: the SHA-256 hash chain is intact -/
+def Admit (x : CandidateX) : Bool :=
+  x.replayValid &&
+  byteGainPositive x &&
+  x.residualDeclared &&
+  x.locNesPass &&
+  x.fycPass &&
+  x.couchStable &&
+  x.treeFiddyBounded &&
+  x.bhocsVerified
+
+/-- Admit requires ALL eight gates to pass. -/
+theorem admit_all_pass (x : CandidateX) :
+    Admit x ↔
+    x.replayValid ∧
+    byteGainPositive x ∧
+    x.residualDeclared ∧
+    x.locNesPass ∧
+    x.fycPass ∧
+    x.couchStable ∧
+    x.treeFiddyBounded ∧
+    x.bhocsVerified := by
+  simp [Admit]
+
+/-- A candidate with any gate failing is NOT admitted. -/
+theorem admit_fails_on_any_failure (x : CandidateX) :
+    (¬ x.replayValid ∨ ¬ byteGainPositive x ∨ ¬ x.residualDeclared ∨
+     ¬ x.locNesPass ∨ ¬ x.fycPass ∨ ¬ x.couchStable ∨
+     ¬ x.treeFiddyBounded ∨ ¬ x.bhocsVerified) →
+    ¬ Admit x := by
+  intro h
+  by_contra hAdmit
+  rw [admit_all_pass] at hAdmit
+  obtain ⟨h1, h2, h3, h4, h5, h6, h7, h8⟩ := hAdmit
+  rcases h with h1' | h2' | h3' | h4' | h5' | h6' | h7' | h8'
+  · exact h1' h1
+  · exact h2' h2
+  · exact h3' h3
+  · exact h4' h4
+  · exact h5' h5
+  · exact h6' h6
+  · exact h7' h7
+  · exact h8' h8
+
+/-- FYC rejects impossible constrained-manifold traversal.
+
+    If FYC_pass is false, the candidate is rejected regardless of
+    other gates. A route that claims to navigate an impossible
+    topology cannot be admitted. -/
+theorem fyc_rejection_blocks_admit (x : CandidateX) (h : ¬ x.fycPass) :
+    ¬ Admit x := by
+  intro hAdmit
+  rw [admit_all_pass] at hAdmit
+  exact h hAdmit.2.2.2.1
+
+/-- Tree Fiddy bounds the AngrySphinx cost.
+
+    If the cost exceeds the Tree Fiddy budget, the candidate is rejected.
+    The Loch Ness Monster takes your money. -/
+theorem treeFiddy_rejection_blocks_admit (x : CandidateX) (h : ¬ x.treeFiddyBounded) :
+    ¬ Admit x := by
+  intro hAdmit
+  rw [admit_all_pass] at hAdmit
+  exact h hAdmit.2.2.2.2.1
+
+/-- A fully-passing candidate IS admitted. -/
+theorem all_pass_implies_admit (x : CandidateX)
+    (h1 : x.replayValid) (h2 : byteGainPositive x)
+    (h3 : x.residualDeclared) (h4 : x.locNesPass)
+    (h5 : x.fycPass) (h6 : x.couchStable)
+    (h7 : x.treeFiddyBounded) (h8 : x.bhocsVerified) :
+    Admit x := by
+  rw [admit_all_pass]
+  exact ⟨h1, h2, h3, h4, h5, h6, h7, h8⟩
+
 /-! §9 GCCL Swap Gate (Q16_16) -/
 
 /-- GCCL swap decision result. -/