listings literate replacements not applied correctly

### Description

In the HTML rendering of this paper, Lean 4 code blocks in Section 4 do not correctly apply the LaTeX `listings` package `literate=` replacements from the TeX source.

Paper URL:

https://arxiv.org/html/2305.00594v3

The raw TeX defines a `leanpretty` listings style with `literate=` mappings for Lean/math tokens such as:

```tex
literate=
{\\Real}{{$\mathbb{R}$}}1
{\\root}{{$\sqrt{\phantom{x}}$}}1
{\\nhdsSym}{{$\mathcal{N}$}}1
{\\Infinity}{{$\infty$}}1
{\\eqF}{{$=^{\mathcal{F}}$}}1
```

However, the HTML output shows the raw replacement keys inside the Lean code instead of the intended rendered symbols/substitutions. For example, the HTML currently contains code like:

```lean
def PPV (TP FP : \Real) : \Real := TP / (TP + FP)
def FM (TP FP FN : \Real) : \Real := \root (PPV TP FP * TPR TP FN)
Tendsto (fun x : \Real => c / x) atTop (\nhdsSym 0)
(fun TN : \Real => MCC TP TN FP FN) \eqF[atTop] post_step3 := by
```

Expected behavior: the rendered listing should follow the `literate=` substitutions from the source, matching the PDF/source intent.

Actual behavior: the `literate=` replacement keys remain visible in the HTML listing.

Note: the do not modify sections required me to populate them before I could submit.

### (Optional:) Please add any files, screenshots, or other information here.

Tex link: https://github.com/Erotemic/paper-g1-and-mcc/blob/51dbc49b42a6fddb994b1a39de25562f0bb72aa2/main.tex

Relevant raw latex snippet:

```latex
\newcommand{\surdSym}{\ensuremath{\raisebox{0.3ex}{\scalebox{0.8}{$\surd$}}}}

\lstdefinestyle{leanpretty}{%
language=lean,
columns=fullflexible,
backgroundcolor=\color{backcolour},
commentstyle=\color{codegreen},
keywordstyle=\color{keywordcolor},
numberstyle=\tiny\color{codegray},
stringstyle=\color{codepurple},
basicstyle=\ttfamily\footnotesize,
breakatwhitespace=false,
breaklines=true,
captionpos=b,
keepspaces=true,
numbers=left,
numbersep=5pt,
showspaces=false,
showstringspaces=false,
showtabs=false,
tabsize=2,
literate=
{`}{\textasciigrave}1
{\\Real}{$\mathbb{R}$}5
{\\le}{$\le$}3
{\\ge}{$\ge$}3
{\\ne}{$\ne$}3
{\\to}{$\to$}3
{\\in}{$\in$}3
{\\nhdsSym}{\ensuremath{\mathcal{N}}}8
{\\Infinity}{\ensuremath{\infty}}9
{\\root}{\surdSym}5
{\\eqF}{\ensuremath{=\raisebox{-0.3ex}{$^{\mathrm{f}}$}}}4
}

\lstset{style=leanpretty}

\begin{lstlisting}[language=lean]
import Mathlib.Tactic
open Filter Topology

noncomputable section

/-- Precision (positive predictive value) -/
def PPV (TP FP : \Real) : \Real := TP / (TP + FP)

/-- Recall (true positive rate) -/
def TPR (TP FN : \Real) : \Real := TP / (TP + FN)

/-- Fowlkes-Mallows index -/
def FM (TP FP FN : \Real) : \Real := \root (PPV TP FP * TPR TP FN)

/-- Matthews correlation coefficient -/
def MCC (TP TN FP FN : \Real) : \Real :=
(TP * TN - FP * FN) / \root ((TP + FP) * (TP + FN) * (TN + FP) * (TN + FN))
\end{lstlisting}
```

PDF Render:

HTML Render:

### (Required) What is this issue most closely related to? Select one.

Other

### Internal issue ID

not automatically populated

### Paper URL

https://arxiv.org/html/2305.00594v3

### Browser

Chrome on Linux

### Device Type

Desktop

Start by comparing the generated listing at https://arxiv.org/html/2305.00594v3 with the listings definitions and Lean examples in main.tex. Trace the HTML rendering path that handles the `literate=` mappings, then verify that the rendered output replaces keys such as `\Real` and `\root` instead of displaying them literally.

Written by the indexing model from the issue text.