diff --git a/CubicalTransport.lean b/CubicalTransport.lean
index d0db845..4bc4c2b 100644
--- a/CubicalTransport.lean
+++ b/CubicalTransport.lean
@@ -29,5 +29,6 @@ import CubicalTransport.Algebra.Restructure
 import CubicalTransport.Algebra.MacroAlias
 import CubicalTransport.Algebra.MetaPath
 import CubicalTransport.Algebra.Methodology
+import CubicalTransport.Algebra.EngineMethodologies
 import CubicalTransport.Algebra.Test
 import CubicalTransport.PropertyTest
diff --git a/CubicalTransport/Algebra/EngineMethodologies.lean b/CubicalTransport/Algebra/EngineMethodologies.lean
new file mode 100644
index 0000000..6191a39
--- /dev/null
+++ b/CubicalTransport/Algebra/EngineMethodologies.lean
@@ -0,0 +1,98 @@
+/-
+  CubicalTransport.Algebra.EngineMethodologies
+  ============================================
+  Engine-bound methodology registrations.  Per ALGEBRA_PLAN.md §9:
+
+  > Every existing `eval_*` / `vTransp_*` / `vCompValue_*` / Glue /
+  > Soundness theorem has at least one corresponding `@[methodology]`
+  > registration that closes its representative question via
+  > `cubical_search`.
+
+  Each registration here is a *closing form* — a theorem that closes
+  a concrete-shape question goal directly, with its classifier
+  hypothesis discharged automatically (typically by `rfl` after
+  struct projection).  This turns a hypothesis-bearing simp lemma
+  (`ask_of_full_face`) into a `cubical_search`-applicable closer
+  (`compq_top_concrete`).
+
+  Goals targeted:
+    - Full-face / empty-face / interval-line questions (all three
+      question shapes: CompQ, TranspQ, HCompQ).
+    - hcomp on `.pi` and on `.top` — closing forms with concrete body.
+
+  Out of scope here:
+    - Methodologies requiring non-trivial classifier discharge
+      (e.g., `ask_of_const_line` wants `¬IsFullFace ∧ ¬IsEmptyFace ∧
+      IsConstLine`).  These would need a richer dispatch tactic; for
+      now `cubical_simp` covers them via the simp-routing path.
+    - Methodologies depending on Glue / Path body shape.  The Glue
+      transport axioms have ~10 face-disjoint cases that each need
+      their own concrete closers; they land in a follow-up.
+-/
+
+import CubicalTransport.Algebra.Methodology
+import CubicalTransport.Question
+
+namespace CubicalTransport.Algebra.EngineMethodologies
+
+open CubicalTransport.Algebra
+open Question
+
+-- ── CompQ closers ───────────────────────────────────────────────────────────
+
+/-- C1 closer: literal `.top` face on a CompQ → `eval env (u.substDim
+    binder .one)`.  Classifier discharged by struct-projection rfl. -/
+@[methodology IsCompQTopFace]
+theorem compQ_top_face (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
+    (CompQ.mk env i A .top u t).ask = eval env (u.substDim i .one) :=
+  CompQ.ask_of_full_face _ rfl
+
+/-- C2 closer: literal `.bot` face on a CompQ → `eval env (.transp
+    binder body .bot t)`. -/
+@[methodology IsCompQBotFace]
+theorem compQ_bot_face (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
+    (CompQ.mk env i A .bot u t).ask = eval env (.transp i A .bot t) :=
+  CompQ.ask_of_empty_face _ rfl
+
+-- ── TranspQ closers ─────────────────────────────────────────────────────────
+
+/-- T1 closer: literal `.top` face on a TranspQ → identity. -/
+@[methodology IsTranspQTopFace]
+theorem transpQ_top_face (env : CEnv) (i : DimVar) (A : CType) (t : CTerm) :
+    (TranspQ.mk env i A .top t).ask = eval env t :=
+  TranspQ.ask_of_full_face _ rfl
+
+/-- T2 specialisation: any face on `.interval` → identity. -/
+@[methodology IsTranspQIntervalLine]
+theorem transpQ_interval_line (env : CEnv) (i : DimVar)
+    (φ : FaceFormula) (t : CTerm) :
+    (TranspQ.mk env i .interval φ t).ask = eval env t :=
+  TranspQ.ask_of_interval_line _ rfl
+
+-- ── HCompQ closers ──────────────────────────────────────────────────────────
+
+/-- HCompQ full-face closer: `vPApp tube .one`. -/
+@[methodology IsHCompQTopFace]
+theorem hcompQ_top_face (A : CType) (tube base : CVal) :
+    (HCompQ.mk A .top tube base).ask = vPApp tube .one :=
+  HCompQ.ask_of_full_face _ rfl
+
+end CubicalTransport.Algebra.EngineMethodologies
+
+-- ── `cubical_close` — simp + search composition ────────────────────────────
+-- Lives here because this is the first module that imports both
+-- `Question` (for `cubical_simp`) and `Methodology` (for
+-- `cubical_search`).
+
+/-- `cubical_close` — the composite closer.  Tries `cubical_simp`
+    first (Level-3-light `@[simp]` routing); then attempts to
+    finish via `rfl` (handles trivially equal residues); then
+    falls through to `cubical_search` (methodology dispatch +
+    metaPath transport).
+
+    Use as the default tactic for question-form goals when you don't
+    know whether they need rewriting, dispatch, or both.  A goal
+    that resists `cubical_close` is genuinely outside the current
+    methodology library and metaPath registry. -/
+macro "cubical_close" : tactic =>
+  `(tactic| first | (cubical_simp; first | rfl | cubical_search) | cubical_search | rfl)
diff --git a/CubicalTransport/Algebra/Test.lean b/CubicalTransport/Algebra/Test.lean
index a2fb962..c1087ea 100644
--- a/CubicalTransport/Algebra/Test.lean
+++ b/CubicalTransport/Algebra/Test.lean
@@ -18,6 +18,7 @@
 
 import CubicalTransport.Algebra.Methodology
 import CubicalTransport.Algebra.MetaPath
+import CubicalTransport.Algebra.EngineMethodologies
 import CubicalTransport.Question
 
 namespace CubicalTransport.Algebra.Test
@@ -187,4 +188,19 @@ example (env : CEnv) (i : DimVar) (t : CTerm) :
     (TranspQ.mk env i .interval .top t).ask = eval env t := by
   cubical_search
 
+-- ── cubical_close: composite closer ─────────────────────────────────────────
+
+/-- `cubical_close` succeeds on a CompQ goal that needs reduction. -/
+example (env : CEnv) (i : DimVar) (A : CType) (u t : CTerm) :
+    (CompQ.mk env i A .top u t).ask = eval env (u.substDim i .one) := by
+  cubical_close
+
+/-- `cubical_close` succeeds on a goal that's already trivial. -/
+example : True := by cubical_close
+
+/-- `cubical_close` succeeds on a TranspQ goal via simp routing. -/
+example (env : CEnv) (i : DimVar) (A : CType) (t : CTerm) :
+    (TranspQ.mk env i A .top t).ask = eval env t := by
+  cubical_close
+
 end CubicalTransport.Algebra.Test