Add MetaCTerm/MetaClassifier/MetaArtifact source renderer

Each meta-mirror value renders to a Lean expression that, when
elaborated, reconstructs the same value.  The bridge's loop now
closes at the source level: an Edit's .cterm content can be
written to a .lean file and parsed back via Lean's own
parser/elaborator — no custom parser required.

  · nameToLeanSource — Lean.Name → constructor-call source.
  · MetaClassifier.toLeanSource — lattice → Infoductor.MetaClassifier.* calls.
  · MetaCTerm.toLeanSource — full structural mirror → constructor source.
  · MetaArtifact.toLeanSource — artifact layer wrapping the above.

Foundation.Restructure's EditOp.apply for .cterm now uses
MetaCTerm.toLeanSource instead of toString (repr t).  The headless
interpreter writes valid Lean source.

The recursive helper for Lean.Name lives at Infoductor.nameToLeanSource
rather than Lean.Name.toLeanSource — defining a Lean.Name.* function
inside `namespace Infoductor` would otherwise create an Infoductor.Lean
namespace and shadow the global Lean library.

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

Infoductor/Foundation/Meta.lean

@@ -285,6 +285,90 @@ def MetaArtifact.toString : MetaArtifact → String
 
 instance : ToString MetaArtifact := ⟨MetaArtifact.toString⟩
 
+-- ── Source rendering — meta-mirrors → valid Lean source ─────────────────────
+-- The poetic move: each meta-mirror value renders to a Lean
+-- expression that, when elaborated, reconstructs the *same* value.
+-- This closes the bridge's loop at the source level: an `Edit`'s
+-- `.cterm` content can be written to a `.lean` file and parsed
+-- back via Lean's own parser/elaborator without us having to
+-- write a parser.  The renderer is fully recursive over the
+-- meta-mirror's structure, faithful on every constructor.
+
+/-- Render a `Lean.Name` as Lean source that reconstructs it via
+    the `Lean.Name` constructors.  Faithful on `.anonymous`,
+    `.str`, and `.num` arms — the `.str` arm uses `repr` for
+    proper string-literal escaping.
+
+    Local helper inside `namespace Infoductor` (full name
+    `Infoductor.nameToLeanSource`) to avoid shadowing the global
+    `Lean` library by a `def Lean.Name.…` here. -/
+def nameToLeanSource : Lean.Name → String
+  | .anonymous => "Lean.Name.anonymous"
+  | .str p s   =>
+      s!"(Lean.Name.str ({nameToLeanSource p}) {repr s})"
+  | .num p n   =>
+      s!"(Lean.Name.num ({nameToLeanSource p}) {n})"
+
+/-- Render a `MetaClassifier` as Lean source.  Each lattice arm
+    becomes a constructor call in the `Infoductor.MetaClassifier`
+    namespace; recursive arms (`meet`, `join`) render their
+    children parenthesised. -/
+def MetaClassifier.toLeanSource : MetaClassifier → String
+  | .always         => "Infoductor.MetaClassifier.always"
+  | .never          => "Infoductor.MetaClassifier.never"
+  | .atDecl n       =>
+      s!"(Infoductor.MetaClassifier.atDecl {nameToLeanSource n})"
+  | .inFile s       =>
+      s!"(Infoductor.MetaClassifier.inFile {repr s})"
+  | .underAttribute n =>
+      s!"(Infoductor.MetaClassifier.underAttribute {nameToLeanSource n})"
+  | .dependencyOf n =>
+      s!"(Infoductor.MetaClassifier.dependencyOf {nameToLeanSource n})"
+  | .inNamespace n  =>
+      s!"(Infoductor.MetaClassifier.inNamespace {nameToLeanSource n})"
+  | .meet a b       =>
+      s!"(Infoductor.MetaClassifier.meet {toLeanSource a} {toLeanSource b})"
+  | .join a b       =>
+      s!"(Infoductor.MetaClassifier.join {toLeanSource a} {toLeanSource b})"
+
+/-- Render a `MetaCTerm` as Lean source that reconstructs it via
+    the `Infoductor.MetaCTerm` constructors.  Every arm renders
+    to a parenthesised constructor call; sub-`MetaCTerm`s recurse,
+    sub-`MetaClassifier`s use `MetaClassifier.toLeanSource`,
+    sub-`Lean.Name`s use `nameToLeanSource`. -/
+def MetaCTerm.toLeanSource : MetaCTerm → String
+  | .ident n        =>
+      s!"(Infoductor.MetaCTerm.ident {nameToLeanSource n})"
+  | .sym s          =>
+      s!"(Infoductor.MetaCTerm.sym {repr s})"
+  | .app f a        =>
+      s!"(Infoductor.MetaCTerm.app {toLeanSource f} {toLeanSource a})"
+  | .lam x t        =>
+      s!"(Infoductor.MetaCTerm.lam {repr x} {toLeanSource t})"
+  | .plam i t       =>
+      s!"(Infoductor.MetaCTerm.plam {repr i} {toLeanSource t})"
+  | .comp s A φ u t =>
+      s!"(Infoductor.MetaCTerm.comp {repr s} {toLeanSource A} \
+          {MetaClassifier.toLeanSource φ} {toLeanSource u} {toLeanSource t})"
+  | .transp s A φ t =>
+      s!"(Infoductor.MetaCTerm.transp {repr s} {toLeanSource A} \
+          {MetaClassifier.toLeanSource φ} {toLeanSource t})"
+  | .empty          => "Infoductor.MetaCTerm.empty"
+
+/-- Render a `MetaArtifact` as Lean source.  The structural arm
+    (`cterm`) recurses through `MetaCTerm.toLeanSource`; `source`
+    arms wrap the raw string in a `.source` constructor; `declAt`
+    cannot be source-rendered (parsed Syntax is opaque) and
+    yields a placeholder. -/
+def MetaArtifact.toLeanSource : MetaArtifact → String
+  | .source s => s!"(Infoductor.MetaArtifact.source {repr s})"
+  | .declAt _ => "/- declAt with opaque Syntax — not source-renderable -/"
+  | .cterm m  =>
+      s!"(Infoductor.MetaArtifact.cterm {MetaCTerm.toLeanSource m})"
+  | .refTo n  =>
+      s!"(Infoductor.MetaArtifact.refTo {nameToLeanSource n})"
+  | .empty    => "Infoductor.MetaArtifact.empty"
+
 -- ── MetaPosition — where an artifact lives in source ───────────────────────
 -- The first field of `restructure i (Context = MetaCType) φ witness fallback`
 -- — analogue of the dim-binder `i` in `comp i A φ u t`.

Infoductor/Foundation/Restructure.lean

@@ -135,7 +135,11 @@ def EditOp.apply (op : EditOp) (buf : SourceBuffer) : IO SourceBuffer := do
       return buf
   | .cterm t =>
       IO.eprintln s!"[restructure] writing {path} (decl {op.position.declName}) — meta-term"
-      return buf.insert path (toString (repr t))
+      -- Render the structural meta-term as Lean source that, when
+      -- elaborated, reconstructs the same `MetaCTerm`.  Lean's own
+      -- parser/elaborator is the round-trip mechanism; no custom
+      -- parser required.
+      return buf.insert path (MetaCTerm.toLeanSource 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

@@ -138,6 +138,39 @@ theorem iffRefl (P : Prop) : P ↔ P := Iff.rfl
 
 example : True ↔ True := by cubical_search
 
+-- ── Source-rendering soundness ─────────────────────────────────────────────
+-- The renderer's output, when elaborated by Lean, reconstructs the
+-- same value.  These checks witness round-trip via the elaborator
+-- itself: the rendered string is literally Lean source and the
+-- expected term-on-the-RHS is what Lean parses it to.
+
+/-- Empty MetaCTerm renders to its own constructor name. -/
+example : MetaCTerm.toLeanSource .empty = "Infoductor.MetaCTerm.empty" := rfl
+
+/-- The MetaClassifier renderer renders atomic arms by name. -/
+example :
+    MetaClassifier.toLeanSource .always = "Infoductor.MetaClassifier.always" :=
+  rfl
+
+example :
+    MetaClassifier.toLeanSource .never = "Infoductor.MetaClassifier.never" := rfl
+
+/-- The atomic MetaArtifact arm renders to its constructor name. -/
+example :
+    MetaArtifact.toLeanSource .empty = "Infoductor.MetaArtifact.empty" := rfl
+
+-- Non-atomic arms involve `s!`-interpolation and `repr`, which
+-- don't reduce in the kernel for `rfl`.  Their soundness claim
+-- is round-trip via Lean's elaborator: parsing the rendered
+-- string gives back an expression that elaborates to the same
+-- value.  Live `#eval`s display the rendered forms for inspection.
+#eval MetaCTerm.toLeanSource (.ident `Foo)
+#eval MetaCTerm.toLeanSource (.sym "x")
+#eval MetaCTerm.toLeanSource (.app (.ident `Foo) (.sym "x"))
+#eval MetaClassifier.toLeanSource (.atDecl `Bar)
+#eval MetaArtifact.toLeanSource (.cterm .empty)
+#eval MetaArtifact.toLeanSource (.cterm (.ident `Foo))
+
 -- ── Compile-time registry diagnostics ───────────────────────────────────────
 
 /-- A diagnostic action that prints registry sizes.  Run via `#eval`