EngineMethodologies + cubical_close: ALGEBRA §9 closer set

Phase D'.6 — closes the "every existing theorem has a methodology"
criterion from ALGEBRA_PLAN.md §9 for the auto-discharging set
(@[simp]-tagged closers whose classifier hypotheses reduce to
struct-projection rfl).

CubicalTransport/Algebra/EngineMethodologies.lean (NEW):
- @[methodology IsCompQTopFace]    compQ_top_face
- @[methodology IsCompQBotFace]    compQ_bot_face
- @[methodology IsTranspQTopFace]  transpQ_top_face
- @[methodology IsTranspQIntervalLine] transpQ_interval_line
- @[methodology IsHCompQTopFace]   hcompQ_top_face

Each registration is a closing-form theorem: it takes the relevant
field tuple of the question and asserts equality to the expected
reduced form, with the classifier hypothesis discharged inline by
`rfl`.  Together with the methodologies in `Algebra/Test.lean`
(`trueMethodology`, `reflMethodologyNat`, `iffRefl`,
`compq_top_concrete`, `transpq_top_concrete`,
`transpq_interval_concrete`), the registry now covers the
auto-discharging core engine theorems.

`cubical_close` macro (in EngineMethodologies.lean):
  cubical_simp; (rfl | cubical_search) — fall-through composition.
  First reduces the goal via @[simp] routing; then closes any
  trivial residue via rfl; then dispatches via the methodology
  library.  The "default tactic" for question-form goals.

Three new end-to-end tests in Algebra/Test.lean exercising
cubical_close on full-face CompQ, trivial True, and full-face
TranspQ goals.

Methodologies still pending @[methodology] tagging (need richer
dispatch for non-trivial classifier conjunctions or Glue/Path
specialisations, scheduled REL2.6+):
- ask_of_const_line (needs ¬IsFullFace ∧ ¬IsEmptyFace ∧ IsConstLine
  conjunction; currently covered by cubical_simp's simp-routing).
- ask_of_pi_line, ask_of_path_line, ask_of_stuck.
- The 9 Glue-transport face-disjoint variants.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

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

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)

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