diff --git a/Infoductor/Foundation/MetaParse.lean b/Infoductor/Foundation/MetaParse.lean
index 171fdce..576a55e 100644
--- a/Infoductor/Foundation/MetaParse.lean
+++ b/Infoductor/Foundation/MetaParse.lean
@@ -821,21 +821,28 @@ theorem tokenize_render_artifact_empty :
       MetaArtifact.toTokens MetaArtifact.empty := by
   decide
 
--- The recursive arms (`.str`, `.app`, `.lam`, etc.) require the
--- four substantial lemmas sketched below — multi-page Lean
--- reasoning about `readIdent` / `readStrLit` distribution.
--- Documented as future work; the token-level universal above
--- plus `decide` on closed instances cover the round-trip
--- operationally in the meantime.
+-- ── Phase 3 distribution lemmas — open question ────────────────────────────
+-- Proving `tokenize ∘ render = toTokens` requires four substantial
+-- distribution lemmas:
 --
---   readIdent_app    : readIdent on (ident-chars ++ rest) where
---                      rest starts cleanly returns (acc ++ ident, rest).
---   readStrLit_app   : readStrLit on (escapeStrLit body ++ '\"' ++ rest)
---                      returns (body, rest).
+--   readIdent_app : reading an ident sequence followed by a clean
+--                   boundary returns the accumulated ident.
+--   readStrLit_app: reading an escapeStrLit-encoded body returns
+--                   the original String.
 --   tokenize_app_clean: tokenize distributes over a concatenation
---                      where the prefix ends "cleanly".
---   tokenize_render_X: induction over each meta-mirror type using
---                      the above plus IH on sub-values.
+--                   where the prefix ends "cleanly".
+--   tokenize_render_X: induction over each meta-mirror type.
+--
+-- Each requires reasoning about Lean 4.30's `String` API (UTF-8
+-- ByteArray-backed) — specifically the equation
+-- `s.push c ++ xs.asString = s ++ (c :: xs).asString`, which is
+-- *not* definitionally true and needs a String-internals lemma.
+--
+-- Cleaner paths forward: (a) refactor `readIdent`/`readStrLit` to
+-- accumulate into a `List Char` rather than a `String`, then build
+-- the String at the end via `List.asString` — decouples the proof
+-- from String internals; or (b) import Mathlib's richer String
+-- API which provides the needed lemmas.
 
 -- ── Round-trip — atomic kernel-reducible witnesses ─────────────────────────
 -- For non-recursive shapes the round-trip is closed by `rfl` (or