Doubling rectifiable curves with no finite-dimensional bi-Lipschitz embedding

Using the fixed doubling Hilbert-space nonembedding theorem of OpenAI at revision fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb as an explicit external premise, we construct in every infinite-dimensional real Banach space one Lipschitz image of [0,1] which is uniformly doubling in its restricted ambient norm metric and has no finite-distortion bi-Lipschitz embedding into any finite-dimensional real normed space. One finite universal doubling constant works for every ambient Banach space. A finite height-separated net thickening retains original witness distances and controls ambient balls at every edge scale. Whole-span Dvoretzky placement and summable tree tours yield a single compact path-connected set of finite one-dimensional Hausdorff measure, fixed before the target dimension or distortion. The accompanying Lean package formalizes selected cover and scalar interfaces, not the full geometric, compactness or nonembedding proof. No injective curve, optimal constant or worldwide priority claim is made.