Add MetaCTerm structural mirror, .cterm artifact arm, MetaPosition.binder

Foundation.Meta gains an 8-constructor MetaCTerm inductive that mirrors
the cubical CTerm's generic shape (ident/sym/app/lam/plam plus dedicated
comp/transp arms; cubical-specific operators encode via .ident-headed
.app chains). MetaArtifact picks up a .cterm arm for structure-preserving
artifact content. MetaPosition gets an Option Lean.Name binder field so
the dim-binder of a comp/transp can be threaded structurally instead of
folded into the classifier.

These additions back the cubical-bridge's Embed.lean overhaul: a real
coreflection between the cubical universe (CType/CTerm/FaceFormula/
DimExpr) and the meta-mirror, with partial inverses and per-constructor
round-trip theorems.

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

Infoductor.lean

@@ -8,3 +8,4 @@
 -/
 
 import Infoductor.Foundation
+import Infoductor.Test

Infoductor/Foundation/Meta.lean

@@ -179,6 +179,65 @@ def MetaClassifier.decEq : (a b : MetaClassifier) → Decidable (a = b)
 
 instance : DecidableEq MetaClassifier := MetaClassifier.decEq
 
+-- ── MetaCTerm — the structural meta-mirror of `CTerm` ──────────────────────
+-- A faithful AST-level mirror of the cubical term language.  Cubical
+-- `CTerm` constructors map onto `MetaCTerm` constructors structurally,
+-- so embedding round-trips through a partial inverse (`toCTerm?`).
+-- See `Embed.lean` in the cubical bridge for the concrete maps and the
+-- coreflection theorems.
+--
+-- Generative basis (8 constructors):
+--   · `ident n`        — closed reference to a Lean declaration.
+--   · `sym  s`         — open leaf (string-named local or dim-binder).
+--   · `app  f a`       — universal application; encodes `papp`, `fst`,
+--                        `snd`, `pair`, `glueIn`, `unglue`, schema
+--                        ctors, and eliminators via `.ident`-headed
+--                        chains.
+--   · `lam  x t`       — term-level lambda (binds `x`).
+--   · `plam i t`       — path-level lambda (binds dim-name `i`).
+--   · `comp i A φ u t` — five-field composition, mirroring `compⁱ A φ u t`.
+--   · `transp i A φ t` — four-field transport, mirroring `transpⁱ A φ t`.
+--   · `empty`          — placeholder for deletion / missing content.
+--
+-- The `comp` and `transp` arms keep their face-formula slot as a
+-- `MetaClassifier` (rather than a nested `MetaCTerm` encoding) so that
+-- classifier-at-position semantics flow through unchanged from
+-- `Edit.lean`.
+
+inductive MetaCTerm where
+  /-- A reference to a Lean declaration — the closed leaf shape. -/
+  | ident   : Lean.Name → MetaCTerm
+  /-- A symbolic name — open leaf (string-named local variable or
+      dim-binder).  Distinct from `ident` so the round-trip through
+      `CTerm.var` preserves the original string. -/
+  | sym     : String → MetaCTerm
+  /-- Application — the universal combinator.  `papp`, `fst`, `snd`,
+      `pair`, schema ctors, and eliminators all encode as `.ident`-
+      headed `.app` chains. -/
+  | app     : MetaCTerm → MetaCTerm → MetaCTerm
+  /-- Term-level lambda — binds `x` in the body. -/
+  | lam     : String → MetaCTerm → MetaCTerm
+  /-- Path-level lambda — binds a dim-name `i`.  Distinct from `lam`
+      because dim-binders inhabit a different kind of universe; the
+      structural distinction is preserved here for downstream
+      analyses that care. -/
+  | plam    : String → MetaCTerm → MetaCTerm
+  /-- Five-field composition — mirrors `compⁱ A φ u t`.  The dim-
+      binder is stored as a string (the `DimVar.name`); the body and
+      the witness are `MetaCTerm`s; the face is a `MetaClassifier`. -/
+  | comp    : String → MetaCTerm → MetaClassifier
+            → MetaCTerm → MetaCTerm → MetaCTerm
+  /-- Four-field transport — mirrors `transpⁱ A φ t`. -/
+  | transp  : String → MetaCTerm → MetaClassifier
+            → MetaCTerm → MetaCTerm
+  /-- The empty meta-term — placeholder for deletion or missing
+      content.  Distinct from `MetaArtifact.empty` (which is at the
+      artifact level). -/
+  | empty   : MetaCTerm
+  deriving Repr
+
+instance : Inhabited MetaCTerm := ⟨MetaCTerm.empty⟩
+
 -- ── MetaArtifact — the meta-mirror of `CTerm` ───────────────────────────────
 -- The "content" half of restructure.  An artifact is what gets put in
 -- the source: a chunk of raw text, a parsed syntax tree, a reference
@@ -201,6 +260,13 @@ inductive MetaArtifact where
   | source : String → MetaArtifact
   /-- A parsed Lean syntax tree. -/
   | declAt : Lean.Syntax → MetaArtifact
+  /-- A structural meta-term — the AST-level representation of a
+      cubical-flavoured artifact.  Preserves the cubical shape so
+      downstream tooling can decompose / reflect it without parsing.
+      The structural mirror is a real coreflection: every cubical
+      `CTerm` embeds losslessly via `CTerm.toMetaCTerm` (in the
+      cubical bridge) and reflects back via `MetaCTerm.toCTerm?`. -/
+  | cterm  : MetaCTerm → MetaArtifact
   /-- A reference to an existing declaration by name; resolved at
       apply time. -/
   | refTo  : Lean.Name → MetaArtifact
@@ -213,6 +279,7 @@ inductive MetaArtifact where
 def MetaArtifact.toString : MetaArtifact → String
   | .source s => s!"source({s})"
   | .declAt _ => "declAt(<syntax>)"
+  | .cterm t  => s!"cterm({repr t})"
   | .refTo n  => s!"refTo({n})"
   | .empty    => "empty"
 
@@ -224,7 +291,14 @@ instance : ToString MetaArtifact := ⟨MetaArtifact.toString⟩
 
 /-- The position of an artifact within a Lean source file or
     project.  Used as the `MetaPosition` argument of `restructure`,
-    analogous to the dim-binder `i` of `comp`. -/
+    analogous to the dim-binder `i` of `comp`.
+
+    The `binder` field carries the dim-binder identity when the
+    position represents a comp-style operation; `none` for
+    non-cubical positions.  This is the meta-mirror of the dim-
+    binder slot in `comp i A φ u t` — kept as a position-level
+    field rather than folded into the classifier so the binder
+    role is preserved structurally. -/
 structure MetaPosition where
   /-- The fully qualified declaration name (or namespace) the
       position lives under.  `Name.anonymous` for file-level. -/
@@ -234,9 +308,13 @@ structure MetaPosition where
   /-- Optional byte offset / range info; `none` if positional via
       declName alone is sufficient. -/
   range    : Option (Nat × Nat)
+  /-- Dim-binder identity for cubical-shaped positions.  `none` for
+      non-cubical or unbound positions.  Preserves the comp-style
+      binder slot structurally. -/
+  binder   : Option Lean.Name := none
   deriving Inhabited
 
 instance : Repr MetaPosition where
-  reprPrec p _ := s!"MetaPosition(declName={p.declName}, filePath={p.filePath}, range={repr p.range})"
+  reprPrec p _ := s!"MetaPosition(declName={p.declName}, filePath={p.filePath}, range={repr p.range}, binder={repr p.binder})"
 
 end Infoductor

Infoductor/Foundation/Restructure.lean

@@ -133,6 +133,9 @@ def EditOp.apply (op : EditOp) (buf : SourceBuffer) : IO SourceBuffer := do
   | .declAt _ =>
       IO.eprintln s!"[restructure] {path}: emit syntax (LSP-bound; headless skipped)"
       return buf
+  | .cterm t =>
+      IO.eprintln s!"[restructure] writing {path} (decl {op.position.declName}) — meta-term"
+      return buf.insert path (toString (repr t))
 
 /-- Run an `Edit` headless: apply every emitted op in order to an
     initial source buffer.  Returns the final buffer plus the

Infoductor/Test.lean

@@ -0,0 +1,154 @@
+/-
+  Infoductor.Test — generic Foundation end-to-end tests
+  =====================================================
+  Compile-time exercise of the Foundation layer (Phases A–D'.5).
+  Cubical-transport-specific tests live downstream in
+  `infoductor-cubical/InfoductorCubical/Test.lean`.
+
+  - Phase A: meta-mirror types.
+  - Phase B: Edit monad + restructure.
+  - Phase C: @[macroAlias].
+  - Phase D'/D'.5: @[methodology] + @[metaPath] + cubical_search.
+-/
+
+import Infoductor.Foundation.Methodology
+import Infoductor.Foundation.MetaPath
+
+namespace Infoductor.Test
+
+open Infoductor
+
+-- ── Phase A: meta-mirror types ─────────────────────────────────────────────
+
+/-- Meta-mirror types are inhabited and well-formed. -/
+example : MetaCType := .theorem_
+example : MetaCType := .file
+example : MetaCType := .classifierSet
+
+example : MetaClassifier := .always
+example : MetaClassifier := .never
+example : MetaClassifier := .meet (.atDecl `Foo) (.inFile "Bar.lean")
+
+example : MetaArtifact := .source "def x := 1"
+example : MetaArtifact := .empty
+example : MetaArtifact := .refTo `Existing
+
+example : MetaPosition :=
+  { declName := `Test, filePath := "Test.lean", range := none }
+
+/-- DecidableEq fires correctly on MetaClassifier. -/
+example : decide (MetaClassifier.always = .always) = true := by decide
+example : decide (MetaClassifier.always = .never) = false := by decide
+example : decide ((.meet .always (.atDecl `Foo) : MetaClassifier) =
+                  (.meet .always (.atDecl `Foo))) = true := by decide
+
+-- ── Phase B: Edit + Context + restructure ───────────────────────────────────
+
+/-- A simple restructure call produces an Edit with one op. -/
+example :
+    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
+    let e := restructure pos .theorem_ .always (.source "def x := 1") .empty
+    e.ops.length = 1 := by
+  rfl
+
+/-- The restructure picks `witness` when the classifier is `.always`. -/
+example :
+    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
+    let e := restructure pos .theorem_ .always (.source "yes") (.source "no")
+    (e.ops.head?).isSome = true := by
+  rfl
+
+/-- The restructure picks `fallback` when the classifier is `.never`. -/
+example :
+    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
+    let e := restructure pos .theorem_ .never (.source "yes") (.source "no")
+    (e.ops.head?).isSome = true := by
+  rfl
+
+/-- Self-consistency check on a single restructure op. -/
+example :
+    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
+    let e := restructure pos .theorem_ .always (.source "x") .empty
+    e.selfConsistent = true := by
+  rfl
+
+/-- A batch that removes a decl AND references it by `refTo` is
+    flagged as inconsistent. -/
+example :
+    let pos₁ : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
+    let pos₂ : MetaPosition := { declName := `Bar, filePath := "F.lean", range := none }
+    let e : Edit Unit := do
+      restructure pos₁ .theorem_ .always .empty .empty       -- removes Foo
+      restructure pos₂ .theorem_ .always (.refTo `Foo) .empty  -- refs Foo
+    e.selfConsistent = false := by
+  rfl
+
+-- ── Frozen aliases ──────────────────────────────────────────────────────────
+
+/-- The `transport_artifact` alias produces a single Edit op. -/
+example :
+    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
+    let e := transport_artifact pos .theorem_ (.source "x")
+    e.ops.length = 1 := by rfl
+
+/-- The `materialize` alias emits raw Lean source. -/
+example :
+    let pos : MetaPosition := { declName := `Foo, filePath := "F.lean", range := none }
+    let e := materialize pos .theorem_ "theorem x : True := trivial"
+    e.ops.length = 1 := by rfl
+
+-- ── Phase C: @[macroAlias] registration ─────────────────────────────────────
+
+/-- A custom alias for testing.  Registered via the attribute below. -/
+@[macroAlias]
+def custom_alias_test (i : MetaPosition) : Edit Unit :=
+  restructure i .definition .always (.source "test") .empty
+
+-- ── Phase D': @[methodology] registration ───────────────────────────────────
+
+/-- A trivial methodology: solves `True` goals.  Registered against
+    a placeholder classifier name `IsTrueGoal`. -/
+@[methodology IsTrueGoal]
+theorem trueMethodology : True := True.intro
+
+/-- `cubical_search` finds the registered methodology for `True`
+    goals.  Demonstrates the dispatch loop end-to-end. -/
+example : True := by cubical_search
+
+/-- Methodology for `Eq.refl`-shaped goals.  Demonstrates that
+    `cubical_search` can dispatch to non-trivial universe-equality
+    goals. -/
+@[methodology IsReflGoal]
+theorem reflMethodologyNat (n : Nat) : n = n := rfl
+
+example : 7 = 7 := by cubical_search
+
+-- ── Phase D'.5: @[metaPath] + methodology-transport ─────────────────────────
+
+/-- A trivial structural Path: every reflexivity goal is also a
+    "trivial-truth" goal.  Declares the meta-Path so methodology-
+    transport can lift `IsTrueGoal` methodologies onto `IsReflGoal`
+    targets and vice versa. -/
+@[metaPath IsReflGoal IsTrueGoal]
+theorem refl_path_to_true (n : Nat) (_ : n = n) : True := True.intro
+
+/-- An identity methodology that closes any `Iff.refl`-shaped goal. -/
+@[methodology IsIffReflGoal]
+theorem iffRefl (P : Prop) : P ↔ P := Iff.rfl
+
+example : True ↔ True := by cubical_search
+
+-- ── Compile-time registry diagnostics ───────────────────────────────────────
+
+/-- A diagnostic action that prints registry sizes.  Run via `#eval`
+    inside a Lean session to verify that @[methodology] /
+    @[macroAlias] / @[metaPath] declarations have populated the
+    EnvExtensions. -/
+def printRegistrySizes : Lean.CoreM Unit := do
+  let aliases ← getAliases
+  let methodologies ← getMethodologies
+  let paths ← getMetaPaths
+  IO.println s!"[Infoductor.Test] aliases={aliases.size} \
+                methodologies={methodologies.size} paths={paths.size}"
+
+end Infoductor.Test