diff --git a/Infoductor/Foundation/Meta.lean b/Infoductor/Foundation/Meta.lean
index 770071f..2bf3cd5 100644
--- a/Infoductor/Foundation/Meta.lean
+++ b/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`.
diff --git a/Infoductor/Foundation/Restructure.lean b/Infoductor/Foundation/Restructure.lean
index e7995ec..89ecde1 100644
--- a/Infoductor/Foundation/Restructure.lean
+++ b/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
diff --git a/Infoductor/Test.lean b/Infoductor/Test.lean
index 6f8a6cf..a7e8bbf 100644
--- a/Infoductor/Test.lean
+++ b/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`