# Reading roadmap: Effective version of Ratner's equidistribution theorem for SL(3,R) The proposed proof translates long unipotent orbit segments into expanding translates, imposes a two-sided diagonal thickness alternative, constructs transverse sets after a nondivergence step, and iterates dimension growth before a high-dimensional equidistribution input. Separate corollaries concern straight lines and nondegenerate planar curves. Source SHA-256: `e6f3ee5af078764b1750ea6a8cdbc8c1d9577ef6d14d0bc638830f385d839db8`. Indexed 211,793 characters. Edges point from prerequisite to consumer. Solid proof edges are attributed inferences, not formal certificates; references remain candidates. ## Statements and the exceptional alternative Read the vector-and-bivector thick part and the two equivalent formulations, keeping every quantifier and the diagonal exponents. Claims: thm:effective-U-orbit, thm:main-thm ## Nondivergence and initial transverse sets Follow the quantitative nondivergence input, the parameter list and the retained-set construction before dimension growth. Claims: prop:quantitative-nondivergence, def:initial-construction, prop:initial-bound-dimension ## Dimension growth and equidistribution Trace the multiscale transverse-set estimates into the high-dimensional equidistribution input and the main theorem. Claims: thm:main-thm ## Applications to curves Read each expanding-curve corollary separately, including changes of scale and Diophantine conditions. Claims: cor:straight-line, cor:curve ## Internal claim index ### Thm 1.1 — `thm:ratner` Source lines 383–393. Let $G$ be a Lie group and $\Gamma$ be a lattice in $G$, namely, the homogeneous space $X = G/\Gamma$ admits a $G$-invariant probability measure. Let $U = \{u(r): r\in \R\}$ be a one-parameter unipotent subgroup of $G$. For any $x \in X$, the closure of the $U$-orbit $U x$ of $x$ is a closed $L$-orbit $Lx$ for some Lie subgroup $L \subset G$. Moreover, $Ux$ is equidistributed in $Lx$ with respect to the unique $L$-invariant probability measure $\mu_L$, namely, for any $f \in C^\infty_c(X)$ (where $C^\infty_c(X)$ denotes the space of smooth func *Extractive statement; proof gist not independently reconstructed.* ### Thm 1.2 — `thm:effective-U-orbit` Source lines 480–488. There exist $\eta >0$ and $t_0 >1$ such that for any $t \ge t_0$ and any $x_0 \in X$, one of the following holds: \par (1) For any $f \in C^\infty_c(X)$, we have \[ \left| \int_{[1]} f(u(r e^t )x_0) \dd r - \int f \dd \mu_G \right| \ll e^{-\eta t } \|f\|_S,\] where $\|\cdot\|_S$ denotes a fixed Sobolev norm; \par (2) $a(-t) a_0( \ell) x_0 \not\in X_{e^{-|\ell|/3}}$ for some $ 0.99 t \le |\ell| \le 1.01 t$. *Extractive statement; proof gist not independently reconstructed.* - `thm:main-thm` (proof_dependency; curated_source_check): Proving Theorem \ref{thm:effective-U-orbit} is equivalent to proving the following theorem: ### Thm 1.3 — `thm:main-thm` Source lines 490–497. Let $\eta, t_0 >0$ be as above. For any $t \ge t_0$, and any $x_0 \in G/\Gamma$, one of the following holds: \par (1) For any $f \in C^\infty_c(X)$, we have \[ \left| \int_{[1]} f(a(t) u(r) x_0 ) \dd r - \int f \dd \mu_G \right| \ll e^{-\eta t} \|f\|_S;\] \par (2) $ a_0 (\ell )x_0 \not\in X_{e^{-|\ell|/3}}$ for some $ 0.99 t \le |\ell| \le 1.01 t$. *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par By Proposition \ref{prop:initial-bound-dimension}, we have that $\mu_{\cF_0}$ is $(d_0, s_0)$-good. By Proposition \ref{prop:dimension-improvement-random}, \ref{prop:dimension-improvement-strange-part}, and \ref{prop:dimension-improvement-structured-component} we get Proposition \ref{prop:improve-dimension}. By Proposition \ref{prop:reduction}, it implies that $\mu_{\cF_{i}}$ is $(d_i, s_i)$-good, where $d_i = d_0 + i \epsilon_2$ and $s_i = 2^{-i}s_0$(we remove an exponentially small proportion at each step). We can proceed with this inductive construction until $d_i \ge 4 - \theta$. By Proposition \ref{prop:high-dim-decomposition}, we have that \[ a(2s_i)_\ast \mu_{\cF_i} = \sum_{k} \n - `prop:initial-bound-dimension` (proof_dependency; curated_source_check): \par By Proposition \ref{prop:initial-bound-dimension}, we have that $\mu_{\cF_0}$ is $(d_0, s_0)$-good. By Proposition \ref{prop:dimension-improvement-random}, \ref{prop:dimension-improvement-strange-part}, and \ref{prop:dimension-improvement-structured-component} we get Proposition \ref{prop:improve-dimension}. By Proposition \ref{prop:reduction}, it implies that $\mu_{\cF_{i}}$ is $(d_i, s_i)$-good, where $d_i = d_0 + i \epsilon_2$ and $s_i = 2^{-i}s_0$(we remove an exponentially small proportion at each step). - `prop:reduction` (proof_dependency; curated_source_check): \par By Proposition \ref{prop:initial-bound-dimension}, we have that $\mu_{\cF_0}$ is $(d_0, s_0)$-good. By Proposition \ref{prop:dimension-improvement-random}, \ref{prop:dimension-improvement-strange-part}, and \ref{prop:dimension-improvement-structured-component} we get Proposition \ref{prop:improve-dimension}. By Proposition \ref{prop:reduction}, it implies that $\mu_{\cF_{i}}$ is $(d_i, s_i)$-good, where $d_i = d_0 + i \epsilon_2$ and $s_i = 2^{-i}s_0$(we remove an exponentially small proportion at each step). - `prop:improve-dimension` (proof_dependency; curated_source_check): \par By Proposition \ref{prop:initial-bound-dimension}, we have that $\mu_{\cF_0}$ is $(d_0, s_0)$-good. By Proposition \ref{prop:dimension-improvement-random}, \ref{prop:dimension-improvement-strange-part}, and \ref{prop:dimension-improvement-structured-component} we get Proposition \ref{prop:improve-dimension}. By Proposition \ref{prop:reduction}, it implies that $\mu_{\cF_{i}}$ is $(d_i, s_i)$-good, where $d_i = d_0 + i \epsilon_2$ and $s_i = 2^{-i}s_0$(we remove an exponentially small proportion at each step). - `prop:high-dim-decomposition` (proof_dependency; curated_source_check): We can proceed with this inductive construction until $d_i \ge 4 - \theta$. By Proposition \ref{prop:high-dim-decomposition}, we have that - `prop:high-dimension-to-equidistribution-a` (proof_dependency; curated_source_check): Then Proposition \ref{prop:high-dimension-to-equidistribution-a}, we have Candidate references: `cor:straight-line` (candidate_proof_dependency); `prop:initial-bound-dimension` (candidate_proof_dependency); `prop:dimension-improvement-random` (candidate_proof_dependency); `prop:dimension-improvement-strange-part` (candidate_proof_dependency); `prop:dimension-improvement-structured-component` (candidate_proof_dependency); `prop:improve-dimension` (candidate_proof_dependency); `prop:reduction` (candidate_proof_dependency); `prop:high-dim-decomposition` (candidate_proof_dependency); `prop:high-dimension-to-equidistribution-a` (candidate_proof_dependency); `external:Bernik-Kleinbock-Margulis` (external_reference). ### Cor 1.4 — `cor:straight-line` Source lines 504–526. Let us denote $$a_1 (t) := a(t) a_0(t) = e^{t/3} & & \\ & e^{t/3} & \\ & & e^{-2t/3} .$$ Let $ \vv w = (w_1, w_2) \in \R^2$ be a vector with Diophantine exponent $\omega(\vv w) = \kappa \le 0.6$, namely, for any positive integer $q \in \Z_+$, we have $$\max \{\langle q w_1 \rangle, \langle q w_2 \rangle\} \gg q^{-\kappa},$$ where $\langle \cdot \rangle$ denotes the distance to the nearest integer. For $\vv v =(v_1, v_2) \in \R^2$ let us denote \[ n(\vv v) := 1 & & v_2 \\ & 1 & v_1 \\ & & 1 . \] Let us define \[\varphi: [1] \to \R^2 \] by $\varp *Extractive statement; proof gist not independently reconstructed.* - `thm:main-thm` (proof_dependency; curated_source_check): Applying Theorem \ref{thm:main-thm} with $x_0 = a_0(t) n^\ast(-w_1, w_2)\Gamma$ and $f_{w_1}$, we have that ### Remark 1.5 — `rmk:expanding-line` Source lines 548–557. The qualitative version of Corollary \ref{cor:straight-line} was proved in \cite{KNSY} for $\omega(\vv w) \le 2$ using Ratner's theorem. The authors also proved that the equidistribution does not hold for $\omega(\vv w) > 2$. *Extractive statement; proof gist not independently reconstructed.* Candidate references: `cor:straight-line` (internal_reference); `external:KNSY` (external_reference). ### Cor 1.6 — `cor:curve` Source lines 558–565. Let us use the same notation as in Corollary \ref{cor:straight-line}. Let $\psi : [1] \to \R^2$ be a smooth non-degenerate curve in $\R^2$, namely, derivatives of $\psi$ span the whole space $\R^2$ at every $r \in [1]$. Then there exist $\eta, t_0>0$ such that for any $t \ge t_0$ and any $f \in C^\infty_c(X)$ we have \[ \left| \int_{[1]} f(a_1(t) n(\psi(r) )\Gamma) \dd r - \int f \dd \mu_G \right| \ll e^{-\eta t} \|f\|_S. \] *Extractive statement; proof gist not independently reconstructed.* - `thm:main-thm` (proof_dependency; curated_source_check): By Theorem \ref{thm:main-thm}, if we have that for any - `external:Bernik-Kleinbock-Margulis` (proof_dependency; curated_source_check): By \cite[Theorem 1.4]{Bernik-Kleinbock-Margulis}, we have that Candidate references: `cor:straight-line` (internal_reference). ### Remark 1.7 — `rmk:expanding-curve` Source lines 599–603. The ineffective version of Corollary \ref{cor:curve} was proved in \cite{Shah_2} using Ratner's theorem. *Extractive statement; proof gist not independently reconstructed.* Candidate references: `cor:curve` (internal_reference); `external:Shah_2` (external_reference). ### Lemma 2.1 — `lm:lie-bracket` Source lines 733–751. For $\vv w^+ \in \vv r^+$, and $\vv w^- \in \vv r^-$, \[ [\vv w^+, \vv w^-] \in \R \fa + \R \fa_0, \] \[ [\vv w^+, \fa] , [\vv w^+, \fa_0] \in \vv r^+, \] \[ [\vv w^-, \fa] , [\vv w^-, \fa_0] \in \vv r^-, \] \[ [\vv w^-, \fu] \in \vv r^+, [\vv w^-, \fu^\ast] =\vv 0, \] and \[ [\vv w^+, \fu^\ast] \in \vv r^-, [\vv w^+, \fu] = \vv 0. \] For $\vv w_1^+, \vv w_2^+ \in \vv r^+$, \[ [\vv w_1^+, \vv w_2^+] \in \R \fu. \] For $\vv w_1^-, \vv w_2^- \in \vv r^-$, \[ [\vv w_1^-, \vv w_2^-] \in \R \fu^\ast. \] For $\vv h \in \fh$, \[ [\fa_0, \vv h] = \vv 0 *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par The statements can be verified by direct calculation. ### Lemma 2.2 — `lm:product-lie-algebra-1` Source lines 755–772. \par Let $0 < \rho_1, \rho_2 < 10^{-10}$ be small constants. For $\vv w \in B_{\fr_1 + \fr_2}(\rho_1)$ and $\vv h \in B_{\R \fa_0 + \fh}(\rho_2)$, we have that \exp(\vv w) \exp(\vv h) = \exp(\tilde{\vv w} +\tilde{\vv h}), where $\tilde{\vv w} \in \fr_1 + \fr_2$ with $\|\vv w - \tilde{\vv w}\| \le 2\rho_2 \|\vv w\|$, and $\tilde{\vv h} \in \R \fa_0 + \fh$ with $$\|\vv h - \tilde{\vv h} \| \le 2\rho_1 \|\vv h\|.$$ \par Conversely, for $\tilde{\vv w} \in B_{\fr_1 + \fr_2}(\rho_1)$ and $\tilde{\vv h} \in B_{\R \fa_0 + \fh}(\rho_2)$, we have \exp(\t *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Let $\rho_0 = \max\left\{\rho_1, \rho_2\right\}$. By the Baker-Campbell-Hausdorff formula, we have \[ \exp(\vv w)\exp(\vv h) = \exp\left(\vv w + \vv h + P\left(\vv w, \vv h\right)\right), \] where P(\vv w , \vv h) =& \frac{1}{2} \left[ \vv w, \vv h \right] + \frac{1}{12} \left( \left[ \vv w, \left[\vv w, \vv h\right] \right] + \left[ \vv h, \left[\vv h, \vv w\right] \right]\right) + \cdots. By Lemma \ref{lm:lie-bracket} and the fact that for any $\vv w_1, \vv w_2 \in \fg$, $\|[\vv w_1, \vv w_2]\| \le \|\vv w_1\| \cdot \|\vv w_2\|$, we have that for any monomial $[\cdots \diamond \cdots]$ in $P(\vv w, \vv h)$ with $i$ Lie brackets, we have $[\cdots \diamond \cdots] \in \fr_1 + \fr_2$ or Candidate references: `lm:lie-bracket` (candidate_proof_dependency); `eq:product-w-h-1` (candidate_proof_dependency); `eq:product-w-h-2` (candidate_proof_dependency). ### Lemma 2.3 — `lm:product-w` Source lines 797–805. Let $0 < \rho < \rho_0 < 10^{-10}$ be two small constants. Let $\vv w, \vv w' \in B_{\fr_1 + \fr_2} (\rho_0)$ be such that \[ \|[\vv w, \vv w']\| \le \rho. \] Then \[ \exp(\vv w ) \exp( \vv w') = \exp(\tilde{\vv w}) \exp( \vv h), \] where $\tilde{\vv w} \in \fr_1 + \fr_2$ with $\| \tilde{\vv w} - \vv w - \vv w'\| \le 26\rho \rho_0$, and $\vv h \in B_{\R \fa_0 + \fh}(4\rho)$. *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par By the Baker-Campbell-Hausdorff formula, we have \[ \exp(\vv w)\exp(\vv w') = \exp\left(\vv w + \vv w' + P\left(\vv w, \vv w'\right)\right), \] where P(\vv w , \vv w') =& \frac{1}{2} \left[ \vv w, \vv w' \right] + \frac{1}{12} \left( \left[ \vv w, \left[\vv w, \vv w'\right] \right] + \left[ \vv w', \left[\vv w', \vv w\right] \right]\right) + \cdots. \par By Lemma \ref{lm:lie-bracket}, we have the following observations: \par For $i = 2j+1$, every monomial $[\cdots\diamond\cdots]$ in $P(\vv w, \vv w')$ with $i$ Lie brackets is in $\R \fa_0 + \fh$. For $i = 2j$, every monomial $[\cdots \diamond \cdots]$ in $P(\vv w, \vv w')$ with $i$ Lie brackets is in $\fr_1 + \fr_2$. \par Moreover, by t Candidate references: `lm:lie-bracket` (candidate_proof_dependency); `lm:product-lie-algebra-1` (candidate_proof_dependency); `eq:hatw-ww'` (candidate_proof_dependency); `eq:tildew-hatw` (candidate_proof_dependency). ### Prop 3.1 — `prop:high-dimension-to-equidistribution-a` Source lines 891–901. There exists $ \theta >0$ such that the following holds: For any $0 < \epsilon < 10^{-1000}$, there exist $ \eta >0$ and $s_0 \gg 1$ depending on $\epsilon >0$ such that for any $s' \ge s_0$, with $ e^{-\epsilon^2 s'} \le \beta \le 10^{-10}$, any Borel probability measure $\rho$ on $[\beta]^2$ with dimension larger than $2-2\theta$ at scale $s'$, that is, for any square $S \subset [\beta]^2$ of size $\beta e^{-s'}$, we have \[ \rho(S) \le \left(\beta e^{-s'}\right)^{2-2\theta},\] any function $f \in C_c^\infty(X)$, and any $x \in X_{\beta^{1/4} *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par The statement can be proved by following the proof of \cite[Proposition 4.2]{LM-preprint2021} step by step. - `external:LM-preprint2021` (proof_dependency; curated_source_check): The statement can be proved by following the proof of \cite[Proposition 4.2]{LM-preprint2021} step by step. - `external:Venkatesh2010` (proof_dependency; curated_source_check): It can be proved by following Venkatesh's argument (\cite[\S 3]{Venkatesh2010} and \cite[Proposition 4.2]{LM-preprint2021} for details). Candidate references: `external:LM-preprint2021` (external_reference). ### Prop 4.1 — `prop:quantitative-nondivergence` Source lines 918–925. There exists $ \alpha > 0$ such that the following holds: For any $\beta, s >0$, if $x \in X$ satisfies that $ a_0(-s)x , a_0(s)x \not\in X_{e^{- s/3 }}$, then, \[ \Leb\left(\left\{r \in [1]: a(s)u(r )x \not\in X_\beta \right\}\right) \ll \beta^{\alpha}. \] *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Let us denote $x = g \Gamma$. By the Kleinbock-Margulis quantitative non-divergence theorem (cf. \cite[Theorem 2.2]{kleinbock2008}, \cite[Theorem 5.2]{Klein_Mar}), if the statement does not hold then there exists a nonzero $\vv v \in \bigwedge^j \Z^3$ (where $j = 1$ or $2$), such that \[ \max_{r \in [1]}\| a(s) u(r) g \vv v\| \le 1. \] \par Case 1. $\vv v \in \Z^3$: Let us denote $ \vv v' = a(s) g \vv v = (v'_1, v'_2, v'_3)$. Then \[ a(s) u(r) g \vv v = u(r e^{s}) \vv v' = (v'_1 , v'_2 + r e^{s} v'_3, v'_3). \] Then $\|a(s) u(r ) g \vv v\| \le 1$ implies that $|v'_1| \le 1 $, $|v'_2 + r e^{s} v'_3| \le 1$ for any $r \in [1]$. The latter easily implies that $|v'_2| \le 1$ and $|v'_3| \le - `external:kleinbock2008` (proof_dependency; curated_source_check): By the Kleinbock-Margulis quantitative non-divergence theorem (cf. \cite[Theorem 2.2]{kleinbock2008}, \cite[Theorem 5.2]{Klein_Mar}), if the statement does not hold then there exists - `external:Klein_Mar` (proof_dependency; curated_source_check): By the Kleinbock-Margulis quantitative non-divergence theorem (cf. \cite[Theorem 2.2]{kleinbock2008}, \cite[Theorem 5.2]{Klein_Mar}), if the statement does not hold then there exists Candidate references: `external:kleinbock2008` (external_reference); `external:Klein_Mar` (external_reference). ### Lemma 4.2 — `lm:separation-lemma-a` Source lines 949–958. For any $\beta >0$, any $\ell \ge 1$, and any $x \in X$ with $a(-\ell)x \in X_{\beta^{1/4}}$, if \[ \exp( r_1 e^\ell \fu + r_2 e^{\ell/2} \vv v_1 + r_3 e^{\ell/2} \vv w_1) x = \exp(\vv v)x \] where $ r_1 , r_2, r_3 \in [\beta]$, $\|(r_1, r_2, r_3)\| \ge \beta/4$, and $\vv v \in B_\fg (\beta)$. Let us write \[ \vv v = u \fu + u^\ast \fu^\ast + a \fa + a_0 \fa_0 + \sum_{j=1}^2 w_j \vv w_j + v_j \vv v_j. \] if we have $|u^\ast| < \beta e^{-\ell}$, then $\|(v_2, w_2)\| \ge \beta e^{-\ell/2}$. *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par For a contradiction, let us assume that $|u^\ast|<\beta e^{-\ell}, |v_2, w_2| < \beta e^{-\ell/2}$. Let us denote $x = g\Gamma$. Then \[ \exp( r_1 e^\ell \fu + r_2 e^{\ell/2} \vv v_1 + r_3 e^{\ell/2} \vv w_1) g = \exp(\vv v)g \gamma, \] for some $\gamma \in \Gamma$. For $\ell >1$ large enough, we have $\gamma \neq e$. Then we have \[ \exp(-\vv v) \exp( r_1 e^\ell \fu + r_2 e^{\ell/2} \vv v_1 + r_3 e^{\ell/2} \vv w_1) = g \gamma g^{-1}. \] Then a(-\ell) g \gamma g^{-1} a(\ell) &= a(-\ell)\exp(-\vv v) \exp( r_1 e^\ell \fu + r_2 e^\ell \vv w_1) a(\ell) \\ &= \exp(- \Ad (a(-\ell))\vv v ) \exp (r_1 \fu + r_2 \vv v_1 + r_3 \vv w_1). Since $|u^\ast| < \beta e^{-\ell}, |v_2, w_2| < \beta e^{-\e ### Defn 6.1 — `def:initial-construction` Source lines 1032–1039. \par $\cF \subset \cE$ is defined by removing from $\cE$ points $y_0 = a ( s) u(r)x_{0} \in \cE$ satisfying $ a_0(\ell') a(-\ell) y_0 \not\in X_{\beta^{1/4}}$ for some $0 \le \ell \le 2\delta_2 t$ and $ - 2\delta_1 t \le \ell' \le 2\delta_1 t$. Let $\mu_{\cF}$ denote the normalized $U$-orbit measure on $\cF$. *Extractive statement; proof gist not independently reconstructed.* ### Prop 6.2 — `prop:initial-bound-dimension` Source lines 1053–1058. For any $\ell \in [\delta_3 t, \delta_1 t]$, and any $x \in \cF$, we have \[ \mu_{\cF} (Q_\ell(\beta) B^{A_0 H}(\beta) x) \le e^{- d_0 \ell}. \] *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Let $\eta_1 = 100 d_0$. Let us divide $a(s)u([1])x_0$ into pieces of length $e^{\eta_1 \ell}$. \par It suffices to show that for each piece $\tilde \cE$ from the above partition with $\tilde \cF := \tilde \cE \cap \cF \neq \emptyset$, and any $x \in \tilde \cF$, \[ |\tilde \cF \cap Q_\ell(\beta) B^{A_0 H}(\beta) x| \le e^{- d_0 \ell} e^{\eta_1 \ell}. \] \par For a contradiction, let us assume that the statement does not hold for some $x\in \tilde \cF$. Then we can find at least $e^{\eta_2 \ell}$ (where $\eta_2 = \eta_1/4$) many $\bar x \in \tilde \cF \cap Q_\ell(\beta) B^{A_0 H}(\beta) x$, $r_{\bar x} \in [1]$ such that \[ u(r_{\bar x} e^{2 d_0 \ell}) \bar x = \exp (\vv v_{\bar x}) a_0^ - `lm:separation-lemma-a` (proof_dependency; curated_source_check): by Lemma \ref{lm:separation-lemma-a}, if we write $h_{\bar x} = \exp(\vv h_{\bar x})$, and - `claim:retained-proportion` (proof_dependency; curated_source_check): \begin{prop} \label{prop:initial-bound-dimension} For any $\ell \in [\delta_3 t, \delta_1 t]$, and any $x \in \cF$, we have \[ \mu_{\cF} (Q_\ell(\beta) B^{A_0 H}(\beta) x) \le e^{- d_0 \ell}. \] \end{prop} - `external:einsiedler-margulis-venkatesh` (proof_dependency; curated_source_check): By repeating the same argument as in \cite{einsiedler-margulis-venkatesh}, Candidate references: `lm:separation-lemma-a` (candidate_proof_dependency); `eq:a0ge` (candidate_proof_dependency); `eq:bound-3` (candidate_proof_dependency); `eq:bound-2` (candidate_proof_dependency); `external:einsiedler-margulis-venkatesh` (external_reference). ### Prop 6.3 — `prop:sl2xr2-closing-lemma` Source lines 1170–1175. For any $x \in \cF$, $j = 1,2$, and any $\ell \in [2\delta_3 t, \delta_1 t]$ \[ \mu_{\cF}(Q(\fr_j, \ell, \beta)B^{A_0 H}(\beta)x) \le e^{- d_0 \ell/2}.\] *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Let us prove the statement for $j = 1$. The proof for $j=2$ is similar. \par For a contradiction, let us assume that there exists $x \in \cF$ such that \[ \mu_{\cF}\left(Q(\fr_1, \ell, \beta)B^{A_0 H}(\beta)x\right) > e^{- d_0 \ell/2}. \] Let us denote $\tilde x = a_0(\ell) x$ and $\hat \mu = a_0(\ell)_\ast \mu_{\cF}$. Noting that $$a_0(\ell) Q(\fr_1, \ell, \beta)B^{A_0 H}(\beta)x = Q_{\ell/2}(\beta) B^{A_0 H}(\beta)\tilde x,$$ we have that \[ \hat \mu \left(Q_{\tilde \ell}(\beta) B^{A_0 H}(\beta)\tilde x\right) > e^{- d_0 \tilde \ell}, \] where $\tilde \ell = \ell/2 \in [\delta_3 t, \delta_1 t]$. By repeating the argument in the proof of Proposition \ref{prop:initial-bound-dimension}, - `prop:initial-bound-dimension` (proof_dependency; curated_source_check): By repeating the argument in the proof of Proposition \ref{prop:initial-bound-dimension}, we can show that Candidate references: `prop:initial-bound-dimension` (candidate_proof_dependency). ### Defn 7.1 — `def:dimension-control` Source lines 1202–1209. Given a probability measure $\mu$ on $X$, we say that $\mu$ is $(d, \ell)$-good if for any $x_0 \in X$, \[\mu (Q_\ell(\beta) B^{A_0 H}(\beta) x_0) \le e^{- d \ell}.\] We say that $\mu$ is $(d, [\ell_1, \ell_2])$-good if it is $(d, \ell)$-good for any $\ell \in [\ell_1 , \ell_2]$. *Extractive statement; proof gist not independently reconstructed.* ### Prop 7.2 — `prop:reduction` Source lines 1237–1251. For $x \in X$, let us call a neighborhood of the form $\Pi(x) = \Pi_{s'} x$ a playground. A playground $\Pi(x)$ is called a full playground if \[ \mu(\Pi(x)) \ge \beta^{15}. \] For any full playground $\Pi(x)$, let us denote \[ \mu_{\Pi(x)} := \mu(\Pi(x))^{-1} \mu|_{\Pi(x)}. \] If for any full playground $\Pi(x)$, there exists \[ \cR_x \subset \Pi(x) \] such that $$\mu_{\Pi(x)} (\cR_x) \le \beta^{20},$$ and after removing $\cR_x$, $\mu_{\Pi(x)}$ is $(d_i+2\epsilon_2, s_{i+1})$-good. Then there exists $\cR_{\diamond} \subset X$ such that \[ \mu( *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Note that there exists a finite subset $\fQ \subset X$ with $|\fQ| \le \beta^{-9}$ and \[ X = \bigcup_{x \in \fQ} \Pi(x). \] Let $\fQ_1 \subset \fQ$ denote the set of $x \in \fQ$ such that $\Pi(x)$ is a full playground, and $\fQ_2 = \fQ \setminus \fQ_1$. Then \[ \mu \left( \bigcup_{x \in \fQ_2} \Pi(x) \right) \le \beta^{-9} \times \beta^{15} \le \beta^{6}. \] By the given condition, for every $x \in \fQ_1$, we get $\cR_x \subset \Pi(x)$ with \[ \mu_{\Pi(x)} (\cR_x) \le \beta^{20}, \] and after removing $\cR_x$, $\mu_{\Pi(x)}$ is $(d_i + 2 \epsilon_2, s_{i+1})$-good. Then \[ \mu\left( \bigcup_{x \in \fQ_1} \cR_x\right) \le \beta^{-9} \times \beta^{20} = \beta^{11}. \] Let \[ \cR_{\diamon ### Lemma 8.1 — `lm:two-theta` Source lines 1314–1321. \par Let us denote \[ \hat{\Theta}_{s'} := Q_{s'}(1.1\beta) Q^{A_0 H}(2s', 1.1\beta). \] Then \[ \Theta_{s'} \subset \hat{\Theta}_{s'}. \] *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Let us take $$g = a_0 a u^\ast (r^\ast) \exp(\vv w^-) \exp(\vv w^+) u(r) \in \Theta_{s'}.$$ By Lemma \ref{lm:product-w}, \[\exp(\vv w^-) \exp(\vv w^+) = \exp(\bar{\vv w} ) \exp( \bar{\vv h}), \] where $\bar{\vv w} \in B_{\fr_1 + \fr_2}(1.01\beta e^{-s'})$ and $\bar{\vv h} \in B_{\R \fa_0 + \fh} (0.01\beta e^{-2s'})$. Therefore, we have \[ g = a_0 a u^\ast (r^\ast) \exp(\bar{\vv w}) \exp(\bar{\vv h}) u(r).\] By rearranging the equation above, we have that $g \in \hat{\Theta}_{s'}$. Candidate references: `lm:product-w` (candidate_proof_dependency). ### Lemma 8.2 — `lm:product-theta` Source lines 1331–1338. \par Let us denote \[ \bar{\Theta}_{s'} := Q_{s'}(2.21\beta) Q^{A_0 H}(2s', 2.21\beta). \] Then for any $\epsilon_i \in \{\pm 1\}$ for $i=1,2$, \[ \Theta^{\epsilon_1}_{s'}\Theta^{\epsilon_2}_{s'} \subset \bar{\Theta}_{s'}. \] *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par We will only prove \[ \Theta_{s'}^{-1} \Theta_{s'} \subset \bar{\Theta}_{s'}. \] Other cases can be proved similarly. \par By Lemma \ref{lm:two-theta}, it suffices to show that \[ \hat{\Theta}_{s'}^{-1} \hat{\Theta}_{s'} \subset \bar{\Theta}_{s'},\] where $\hat{\Theta}_{s'}$ is defined as in Lemma \ref{lm:two-theta}. \par Let us take $g = \exp(\vv w) \exp(\vv h) \in \hat{\Theta}_{s'}$ and $g' = \exp(\vv w') \exp(\vv h') \in \hat{\Theta}_{s'}$. Then \[ g^{-1} g' = \exp(-\vv h) \exp(-\vv w) \exp(\vv w') \exp(\vv h'). \] By Lemma \ref{lm:product-w}, we have \[ \exp(-\vv w) \exp(\vv w') = \exp(\bar{\vv w}) \exp (\bar{\vv h}), \] where $\bar{\vv w} \in B_{\fr_1 + \fr_2}(2.201\beta e^{-s'})$, Candidate references: `lm:two-theta` (candidate_proof_dependency); `lm:product-w` (candidate_proof_dependency). ### Cor 8.3 — `cor:product-theta` Source lines 1355–1362. \par Let us denote \[ \tilde{\Theta}_{s'} := Q_{s'}(4.5\beta) Q^{A_0 H}(2s', 4.5\beta). \] Then for any $\epsilon_i \in \{\pm 1\}$ for $i=1,2,3,4$, \[ \Theta^{\epsilon_1}_{s'}\Theta^{\epsilon_2}_{s'} \Theta^{\epsilon_3}_{s'} \Theta^{\epsilon_4}_{s'} \subset \tilde{\Theta}_{s'}. \] *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par We will only prove \[\Theta_{s'}\Theta_{s'} \Theta_{s'} \Theta_{s'} \subset \tilde{\Theta}_{s'}. \] Other cases can be proved similarly. In fact, by Lemma \ref{lm:product-theta}, we have \[ \Theta_{s'}\Theta_{s'} \subset \bar{\Theta}_{s'}, \] where $\bar{\Theta}_{s'}$ is defined as in Lemma \ref{lm:product-theta}. By repeating the proof of Lemma \ref{lm:product-theta}, we get \[ \bar{\Theta}_{s'} \bar{\Theta}_{s'} \subset \tilde{\Theta}_{s'}. \] Combining the two inclusions above, we conclude that \[\Theta_{s'}\Theta_{s'} \Theta_{s'} \Theta_{s'} \subset \tilde{\Theta}_{s'}. \] Candidate references: `lm:product-theta` (candidate_proof_dependency). ### Lemma 8.4 — `lm:different-coordinate-1` Source lines 1373–1384. For $\vv w^+ \in \vv r^+$ and $ \vv w^- \in \vv r^-$ with $\|\vv w^+\|, \|\vv w^-\| \le 10 \beta e^{-\ell}$, we have that \[ \exp(\vv w^+ + \vv w^-) = a_0 a u^{\ast} (r^\ast) \exp(\bar{\vv w}^-) \exp(\bar{\vv w}^+) u(r), \] where $\bar{\vv w}^+ \in \vv r^+$ with $\|\bar{\vv w}^+ - \vv w^+\| \le 0.01\beta e^{-3\ell}$, $\bar{\vv w}^- \in \vv r^-$ with $\|\bar{\vv w}^- - \vv w^-\| \le 0.01\beta e^{-3\ell}$, $a_0 a \in B^{A_0 A}(0.01\beta e^{-2\ell})$, and $r^\ast, r \in [0.01\beta e^{-2\ell}]$. \par Similarly, we have \[ \exp(\vv w^+ + \vv w^-) = *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par We only prove the first statement. The second statement can be proved using the same argument. \par Let us write \[ \exp(\vv w^+ + \vv w^-) = a_0 a u^{\ast} (r^\ast) \exp(\bar{\vv w}^-) \exp(\bar{\vv w}^+) u(r), \] where $a_0 a \in B^{A_0A} (10\beta e^{-\ell})$, $r^\ast, r \in [10\beta e^{-\ell}]$, $\bar{\vv w}^- \in B_{\vv r^-}(10 \beta e^{-\ell})$, and $\bar{\vv w}^+ \in B_{\vv r^+}(10 \beta e^{-\ell})$. Noting that \[ \|[\bar{\vv w}^-, \bar{\vv w}^+]\| \le \|\bar{\vv w}^-\| \cdot \|\bar{\vv w}^+\| \le 0.001 \beta e^{-2\ell}, \] by Lemma \ref{lm:product-w}, we have \[ \exp(\bar{\vv w}^-) \exp(\bar{\vv w}^+) = \exp(\tilde{\vv w}^- + \tilde{\vv w}^+) \exp( \vv h), \] where $\tilde{\vv w Candidate references: `lm:product-w` (candidate_proof_dependency). ### Lemma 8.5 — `lm:cross-section` Source lines 1414–1421. For $y \in \Pi(x)$ and $r \in [\beta e^{2s'}]$, let \[J_r(y) :=\left\{r' \in \left[2\beta e^{2s'}\right]: u(r')y \in \Sigma^r\right\}. \] Then there exists intervals $J_1 \subset J_r(y) \subset J_2$ with size $ 0.5 \beta \le |J_1| \le |J_2| \le 4 \beta$. *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Without loss of generality, we can assume $r=0$. We first prove $J_0(y) \neq \emptyset$. For any $y \in \Pi(x)$, let us write \[ y = a_y a_{0, y} u^\ast(r^\ast_y) \exp(\vv w_y^-) \exp(\vv w_y^+) u(r_y) x \] where $a_y a_{0,y} \in B^{A A_0} (\beta)$, $r_y^\ast \in \left[\beta e^{-2s'}\right]$, $$\vv w_y^- = v_{2,y} \vv v_2 + w_{2,y} \vv w_2 \in B_{\vv r^-} \left(\beta e^{-s'}\right),$$ $$\vv w_y^+ = v_{1,y} \vv v_1 + w_{1,y} \vv w_1 \in B_{\vv r^+} \left(\beta e^{s'}\right),$$ and $r_y \in \left[\beta e^{2s'}\right]$. Then for any $r \in \left[\beta e^{2s'}\right]$, \[ u(r) y = a'_y a'_{0, y} u^{\ast} (\tilde r^\ast_y) u(\tilde r) \exp(\vv w_y^-) \exp(\vv w_y^+) u(r_y) x,\] where $a'_y a Candidate references: `eq:fy` (candidate_proof_dependency). ### Lemma 8.6 — `lm:initial-dimension-under-a-t` Source lines 1428–1433. For any $\delta_3 t \le \ell \le \delta_1 t$ and any $\bar x \in \Pi(x)$, we have \[ \tilde \mu(\Sigma_{s', \ell} (\bar x)) \le e^{-2s'} e^{-d_0 \ell}.\] *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Note that $\Sigma_{s', \ell} (\bar x)$ is a cross-section of $\Pi_{s', \ell}(\bar x)$ along the $U$-orbits, and $\tilde \mu$ is Lebesgue along the $U$-orbits. We have \[ \tilde \mu(\Sigma_{s', \ell} (\bar x) ) \ll e^{-2s'} \tilde \mu (\Pi_{s', \ell} (\bar x) ).\] Note that by the definition of $\tilde \mu$, we have \[ \tilde \mu (\Pi_{s', \ell} (\bar x)) \le \mu_{\cF_i} (a(-2s')\Pi_{s', \ell} (\bar x) ), \] and \[ a(-2s')\Pi_{s', \ell} (\bar x) = B^{A_0 A}(\beta) B^{U^\ast}(\beta) \exp\left( B_{\vv r^-}(\beta e^{-\ell}) \right) \exp\left( B_{\vv r^+}(\beta e^{-\ell}) \right) B^{U}(\beta) x' \] where $x' = a(-2s') \bar x$. By Lemma \ref{lm:different-coordinate-1}, we have that \[ B^{A_0 - `lm:different-coordinate-1` (proof_dependency; curated_source_check): By Lemma \ref{lm:different-coordinate-1}, we have that - `prop:initial-bound-dimension` (proof_dependency; curated_source_check): By repeating the proof of Proposition \ref{prop:initial-bound-dimension} to $\cF_i$ we have Candidate references: `lm:different-coordinate-1` (candidate_proof_dependency); `prop:initial-bound-dimension` (candidate_proof_dependency). ### Defn 8.7 — `def:kakeya-model` Source lines 1451–1538. \par Let $s'>0$ and $\tilde \mu$ be a probability measure on a playground $\Pi(x) \subset X$ defined by taking the normalized measure on a subset consisting of $U$-orbits of length $\beta e^{2s'}$. Let us fix a sequence of cross-sections $$\left\{\Sigma^r = \Sigma_{s'} u(r)x: r \in \left[\beta e^{2s'}\right]\cap\left(0.1\beta \Z\right) \right\} .$$ \par We first define the projection map \[ \bP: \Pi(x) \to \R^3 \] as follows: For $x' \in \Pi(x)$, we can write \[x' =a_{0, x'} a_{x'} u^\ast(r^\ast_{x'} ) \exp(\vv w^-_{x'}) \exp(\vv w^+_{x'}) u(r_ *Extractive statement; proof gist not independently reconstructed.* Candidate references: `eq:fy` (internal_reference). ### Lemma 8.8 — `lm:partition-1` Source lines 1612–1619. We have \[ \Pi(x) = \bigcup_{z \in \cI} \Theta'(z). \] Moreover, for any $z' \in \Pi(x)$, there are at most $N_2$ different $z \in \cI$ such that \[ \Theta(z') \cap \Theta(z) \neq \emptyset. \] *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par We first prove that for any $z' \in \Pi(x)$, there exists $z \in \cI$ such that $z' \in \Theta(z)$. In fact, let us write \[ z' = a_{z'} a_{0, z'} u^{\ast} (r^\ast_{z'}) \exp(\vv w^-_{z'}) \exp(v_{1, z'} \vv v_1 + w_{1, z'} \vv w_1) u(r_{z'}) x, \] where $a_{z'} \in B^A(\beta)$, $a_{0, z'} \in B^{A_0}(\beta)$, $r^\ast_{z'} \in \left[\beta e^{-2s'}\right]$, $\vv w^-_{z'} \in B_{\vv r^-}\left(\beta e^{-s'}\right)$, and $$(r_{z'} , v_{1, z'}, w_{1, z'}) \in \left[\beta e^{2s'}\right] \times \left[\beta e^{s'}\right]^2.$$ Let us choose $z \in \cI$ such that \[ z = \exp(v_1 \vv v_1 + w_1 \vv w_1 ) u(r_z) x \] such that $|r_z - r_{z'}| \le 0.2 \beta$, and \[ \max \{ |v_{1, z} - v_1|, |w_{1,z} Candidate references: `lm:product-theta` (candidate_proof_dependency); `lm:different-coordinate-1` (candidate_proof_dependency); `eq:z-z'` (candidate_proof_dependency). ### Lemma 8.9 — `lm:partition-2` Source lines 1660–1667. For any $z \in \cI$, \[ \Theta'(z) = \bigcup_{y \in \cI_z} \Omega'(y). \] Moreover, for any $y' \in \Theta(z)$, there are at most $N_2$ different $y \in \cI_z$ such that \[ \Omega(y) \cap \Omega(y') \neq \emptyset. \] *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par We first prove that for any $z' \in \Theta'(z)$, there exists $y \in \cI_z$ such that $z' \in \Omega(y)$. By Lemma \ref{lm:two-theta}, $\Theta_{s'} \subset \hat{\Theta}_{s'}$. Therefore, we can write \[ z' = a_0 a u(r) \exp(\vv w^+ + \vv w^-)u^\ast (r^\ast) z, \] where $a_0 a \in B^{A_0 A} (1.1 \beta)$, $r \in [1.1\beta]$, $r^\ast \in [1.1 \beta e^{-2s'}]$, $\vv w^+ \in B_{\vv r^+}(1.1 \beta e^{-s'})$ and $\vv w^- = v_2 \vv v_2 + w_2 \vv w_2 \in B_{\vv r^-}(1.1\beta e^{-s'})$. Let $y \in \cI_z$ such that \[ y = \exp(\bar{\vv w}^-) z, \] with $\| \bar{\vv w}^- - \vv w^- \|\le 0.2 \beta e^{-3s'}$. \par We will prove that $z' \in \Omega(y)$. In fact, we have z' = a_0 a u(r) \exp(\vv w^+ + Candidate references: `lm:two-theta` (candidate_proof_dependency); `lm:product-w` (candidate_proof_dependency); `eq:z'-y` (candidate_proof_dependency); `lm:different-coordinate-1` (candidate_proof_dependency). ### Defn 8.10 — `def:coordinate-theta` Source lines 1668–1675. \par Given $z \in \cI$ and $ y \in \Theta'(z)$, let us define the coordinate of $y$ in $\Theta'(z)$, denoted by $\fD_z(y) \in \R^2$ as follows: Let us write \[ y = a_0 a u(r_y) \exp(\vv w^+) \exp( \vv w^-)u^\ast (r^\ast_y) z, \] where $a_0 a \in A_0 A$, $\vv w^+ \in \vv r^+$ and $\vv w^- = v_2 \vv v_2 + w_2 \vv w_2 \in \vv r^-$. Then we define \[ \fD_z(y) := (v_2, w_2). \] *Extractive statement; proof gist not independently reconstructed.* ### Remark 8.11 — `rmk:partition-2` Source lines 1727–1736. \par Let us denote \fC := \left[1.2 \beta e^{-s'}\right]^2. From Lemma \ref{lm:partition-2}, we can see that for any $z' \in \Theta(z)$, \[ \fD_z(z') \in \fC. \] *Extractive statement; proof gist not independently reconstructed.* Candidate references: `lm:partition-2` (internal_reference). ### Lemma 8.12 — `lm:wv2r` Source lines 1736–1758. \par Suppose \[ y_2 = \exp(\vv w^-) \exp(\vv w^+) u(r_0) y_1,\] where $|r_0| \le \beta e^{2s'}$, $\vv w^- = v_2 \vv v_2 + w_2 \vv w_2 \in B_{\vv r^-} (\beta e^{-s'})$, and $\vv w^+ = v_1 \vv v_1 + w_1 \vv w_1 \in B_{\vv r^+} (\beta e^{s'})$. For $r \in [\beta e^{2s'}]$, let us write $u(r) y_2$ as \[ u(r) y_2 = a a_0 u^\ast \exp(\vv w^-(r)) \exp(\vv w^+(r)) u(f(r)) y_1, \] where $a \in A$, $a_0 \in A_0$, $u^\ast \in U^\ast$, $\vv w^+ (r) \in \vv r^+$, and \[ \vv w^-(r) = v_2(r) \vv v_2 + w_2 (r) \vv w_2 \in \vv r^-. \] Then v_2(r) = \frac{2 v_2} *Extractive statement; proof gist not independently reconstructed.* Proof opening: This can be verified by direct calculation. ### Lemma 8.13 — `lm:omega-u` Source lines 1763–1782. Let $\tilde \mu$ and $\Pi(x)$ be as in Definition \ref{def:kakeya-model}. Let us denote \hat{\Omega}_{s'} := Q^{s'}_{3s'}(2.1\beta) Q^{A_0 H} (2s', 2.1\beta). For $y \in \fJ$, let us denote U\Omega'(y) : = \left\{ u(r') y' : y' \in \Omega'(y), r' \in \fl(y') \right\}. For $r \in \fl(y)$, let us denote \Omega(y, r) := U\Omega'(y) \cap \Sigma^{\tilde{r}}, where $\tilde r$ satisfies that $u(r)y \in \Sigma^{\tilde{r}}$. Then \[ \Omega(y, r) \subset \hat{\Omega}(u(r)y) := \hat{\Omega}_{s'} u(r) y. \] In particular, we have \[ \tilde \mu(\Omega'(y)) *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par For $y' \in \Omega'(y)$, we have \[ y = \exp(\vv w^+ + \vv w^-) \exp(\vv h) y', \] where $\vv w^+ \in B_{\vv r^+}(2.01\beta e^{-s'})$, $\vv w^- \in B_{\vv r^-}(2.01\beta e^{-3s'})$, and $\vv h \in \fq^{A_0 H}(2s', 2\beta)$. Then u(r) y &= u(r) \exp(\vv w^+ + \vv w^-) \exp(\vv h) y' \\ &= \exp(\Ad_{u(r)} (\vv w^+ + \vv w^-)) u(r)\exp(\vv h) y' \\ &= \exp(\vv w^+ + \tilde{\vv w}^+ + \vv w^-) \exp(\tilde{\vv h}) u(r') y', where $\tilde{\vv w}^+ \in \vv r^+$ with $\|\tilde{\vv w}^+\| = |r| \|\vv w^-\|$, and $\tilde{\vv h} \in \fq^{A_0 H}(2s', 2.01\beta)$. Note that $|r| \le \beta e^{2s'}$, and $\|\vv w^-\| \le 2.01 \beta e^{-3s'}$. We have $\|\tilde{\vv w}^+\| \le 0.01 \beta e^{-s'}$. This Candidate references: `def:kakeya-model` (internal_reference); `lm:cross-section` (candidate_proof_dependency). ### Lemma 8.14 — `lm:time-leave` Source lines 1804–1822. \par Let $s' >0$ and $\Pi(x) $ be as in Definition \ref{def:kakeya-model}. Let us fix a cross-section $\Sigma^r \subset \Pi(x)$ defined as above. Then for any $y_1, y_2 \in \fJ \cap \Sigma^r$, suppose there exist $L_1, L_2$ and $z \in \cI$ such that \[ \Omega(y_i, L_i) \cap \Theta'(z) \neq \emptyset, \text{ for } i=1,2, \] where $\Omega(y_i, L_i)$ is defined as in \eqref{eq:omega-y-r}. \par Let us denote $\tilde{y}_i = u(L_i) y_i$ and write \[ \tilde{y}_1 = a_0 a u^\ast(r^\ast) \exp(\vv w^-) \exp(\vv w^+) u(r_0) \tilde{y}_2,\] where $a_0 a \in *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par By Lemma \ref{lm:omega-u}, we have $\Omega(y_i, L_i) \subset \hat{\Omega}(\tilde{y}_i)$. Therefore, we have $ \hat{\Omega}(\tilde{y}_1) \cap \Theta(z) \neq \emptyset$ which implies that \[ \tilde{y}_1 \in \hat{\Omega}_{s'}^{-1} \Theta_{s'} z \subset \Theta_{s'}^{-1} \Theta_{s'} z. \] Similarly, we have $ \hat{\Omega}(\tilde{y}_2) \cap \Theta(z) \neq \emptyset$ implies that \[ z \in \Theta_{s'}^{-1} \Omega_{s'} \tilde{y}_2 \subset \Theta_{s'}^{-1} \Theta_{s'} \tilde{y}_2. \] Therefore, \[ \tilde{y}_1 \in \Theta_{s'}^{-1} \Theta_{s'}\Theta_{s'}^{-1} \Theta_{s'} \tilde{y}_2. \] By Corollary \ref{cor:product-theta}, \[ \tilde{y}_1 \in \tilde{\Theta}_{s'} \tilde{y}_2.\] Then we have \[ \tild Candidate references: `def:kakeya-model` (internal_reference); `eq:omega-y-r` (internal_reference); `lm:omega-u` (candidate_proof_dependency); `cor:product-theta` (candidate_proof_dependency); `lm:different-coordinate-1` (candidate_proof_dependency); `eq:fvy` (candidate_proof_dependency); `eq:fwy` (candidate_proof_dependency); `eq:fy` (candidate_proof_dependency). ### Lemma 8.15 — `lm:concentrated-surface` Source lines 1862–1880. \par Recall that $I(y_1, y_2)$ is defined as in \eqref{eq:Iy1y2}. Let us fix a cross-section $\Sigma^r$. Let $z \in \cI\cap \Sigma^r, y \in \fJ\cap \Sigma^r$. Then the set of all coordinates $\fD_z (\bar z)$ of the elements $\bar z \in \cI_z$ such that $I(\bar z , y) \neq \emptyset$ and in addition there is some $r \in I(\bar z, y)$ with $|r| \ge \beta^{100} e^{2s'}$ is contained in the $ \beta^{-100} e^{-3s'}$ neighborhood of the hyperbola \left\{ (X, Y) \in \fC: (X - X_0)(Y-Y_0) + \frac{X - X_0}{v_1} + \frac{Y - Y_0}{w_1} = 0 \right\}, where *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par There exist $y' \in \Omega(y)$ and $z' \in \Theta(z)$ such that \[ z' = \exp(\vv w^+) u(r_{y'}) y',\] where $\vv w^+ = v_1 \vv v_1 + w_1 \vv w_1 $, and \[ z' = \exp(\vv w_0^-) z, \] where $\vv w_0^- = X_0 \vv v_2 + Y_0 \vv w_2$. We can also make sure that \[ \min\{|v_1|, |w_1|\} \ge \beta e^{-s'}. \] \par Without loss of generality, let us assume $|w_1| \ge |v_1|$. The opposite case can be handled similarly. \par Suppose $\bar z = \exp(\vv w^-) z' $ (where $\vv w^- = v_2 \vv v_2 + w_2 \vv w_2$) satisfies that $I(\bar z, y) \neq \emptyset$. Then by \eqref{eq:fvy}, \eqref{eq:fwy}, and \eqref{eq:fy}, we have that \[ u(r) \bar z = a_{0,r} a_r u^{\ast} (f^\ast(r)) \exp(\vv f_-(r)) \exp(\vv f Candidate references: `eq:Iy1y2` (internal_reference); `eq:fvy` (candidate_proof_dependency); `eq:fwy` (candidate_proof_dependency); `eq:fy` (candidate_proof_dependency); `lm:time-leave` (candidate_proof_dependency); `eq:1` (candidate_proof_dependency); `eq:2` (candidate_proof_dependency); `eq:3` (candidate_proof_dependency); `eq:hyperbola-box` (candidate_proof_dependency). ### Remark 8.16 — `rmk:concentrated-surface` Source lines 1934–1945. $\quad$ \item Note that $I(y_1, y_2)$ will change if we replace $y_1$ with $y'_1 \in \Omega(y_1)$. However, there exists a one-to-one map \[ P_{y_1, y'_1}: I(y_1, y_2) \to I(y'_1, y_2) \] such that $|P_{y_1, y'_1} (r') - r'| \le \beta |r'|$ for every $r' \in I(y_1,y_2)$. \item If $|v_1/w_1| \le e^{-s'}$ or $|w_1/v_1| \le e^{-s'}$, then the neighborhood described in~\eqref{eq:hyperbola} agrees with the $ \beta^{-100} e^{-3s'}$ neighborhood of the straight line \[ v_1^{-1}(X - X_0) + w_1^{-1}(Y - Y_0) = 0.\] *Extractive statement; proof gist not independently reconstructed.* Candidate references: `eq:hyperbola` (internal_reference). ### Prop 9.1 — `prop:improve-dimension` Source lines 1962–1971. \par Suppose that $\cF_i$ is $(d_i, s_i)$-good. Let $\mu = a(s_i)_\ast\mu_{\cF_i}$. Let us fix a full playground $\Pi(x)$ and denote $\tilde \mu = \mu_{\Pi(x)}$. Then $\tilde \mu$ admits the following decomposition: \[ \tilde \mu = \nu_{\cR_i} \tilde \mu_{\cR_i} + \nu_{i+1} \tilde \mu_{i+1}, \] such that $\nu_{\cR_i} \le \beta^{20}$, and $\mu_{i+1}$ is $(d_i+\epsilon_1, s_{i+1})$-good. Recall that $s_{i+1} = s_i/2$. *Extractive statement; proof gist not independently reconstructed.* - `prop:dimension-improvement-random` (proof_dependency; curated_source_check): By Proposition \ref{prop:dimension-improvement-random}, \ref{prop:dimension-improvement-strange-part}, and \ref{prop:dimension-improvement-structured-component} we get Proposition \ref{prop:improve-dimension}. - `prop:dimension-improvement-strange-part` (proof_dependency; curated_source_check): By Proposition \ref{prop:dimension-improvement-random}, \ref{prop:dimension-improvement-strange-part}, and \ref{prop:dimension-improvement-structured-component} we get Proposition \ref{prop:improve-dimension}. - `prop:dimension-improvement-structured-component` (proof_dependency; curated_source_check): By Proposition \ref{prop:dimension-improvement-random}, \ref{prop:dimension-improvement-strange-part}, and \ref{prop:dimension-improvement-structured-component} we get Proposition \ref{prop:improve-dimension}. ### Defn 9.2 — `def:heavy-part` Source lines 1978–1985. \par For $z \in \cI$, we call $\Theta'(z)$ a heavy neighborhood if \[ \tilde \mu (\Theta'(z)) > e^{-2s'} e^{- (d_i + \epsilon_1) s'}. \] $\Theta'(z)$ a extremely heavy if \[ \tilde \mu (\Theta'(z)) > e^{-2s'} e^{- (d_i -C_1 \epsilon_1) s'}. \] *Extractive statement; proof gist not independently reconstructed.* ### Defn 9.3 — `defn:line:1985` Source lines 1985–1988. \par Let $\cR_i \subset \Pi(x)$ denote the union of heavy neighborhoods. Then $\cR_i$ will be said to be the heavy part of $\Pi(x)$. *Extractive statement; proof gist not independently reconstructed.* ### Lemma 9.4 — `lm:omega-upper` Source lines 1998–2006. Let us denote $s' = s_{i+1}$. For any $\Omega(y) = \Omega_{s'} y$, we have \tilde \mu (\Omega'(y)) \le \beta^{-15}e^{-2 s'} e^{-2 d_i s'}. *Extractive statement; proof gist not independently reconstructed.* Proof opening: First note that \[ \mu(\Omega(y)) = \mu_{\cF_i}(a(-2s') \Omega(y)),\] and \[ a(-2s') \Omega(y) = Q_{2s'}(2\beta) R^{A_0 H}(2s', 2\beta) y' \] where $y' = a(-2s') y$. Noting that $\mu_{\cF_i}$ is a normalized measure on $U$-orbits, we have \[ \mu_{\cF_i} (Q_{2s'}(2\beta) R^{A_0 H}(2s', 2\beta) y') \le e^{-2s'} \mu_{\cF_i} (Q_{2s'}(2\beta) B^{A_0 H }(2\beta) y'). \] By our hypothesis that $\mu_{\cF_i}$ is $(d_i, 2s')$-good, we have \[ \mu_{\cF_i} (Q_{2s'}(2\beta) B^{A_0 H }(2\beta) y') \le e^{-2d_i s'}, \] which implies the claim. \par Since $\Pi(x)$ is a full playground, we have that for any $y \in \fJ$, \eqref{eq:upper-omega} holds. Candidate references: `eq:upper-omega` (candidate_proof_dependency). ### Defn 9.5 — `def:heavy-part-decomposition` Source lines 2020–2047. \par For integer $j \ge 1$, let us denote \[ \Xi_j(z') := \Xi_{s',j} z' \cap \Theta'(z'), \] where \[ \Xi_{s', j} := Q^{s'}_{s' + j}Q^{A_0 H}(2s', 1.1\beta).\] \par Given a heavy neighborhood $\Theta' (z)$, we call $\Theta'(z)$ strange if there exists $ \Xi_{C_1 \epsilon_1 s'}(z') \subset \Theta'(z)$ such that \[ \tilde \mu_{\fr}(\Xi_{C_1 \epsilon_1 s'}(z')) \ge (1-\beta) \tilde \mu_{\fr}(\Theta'(z)). \] Otherwise, we call it a normal neighborhood. Let $\bar \cR_i \subset \cR_i$ denote the union of all the heavy neighborhoods that are also norm *Extractive statement; proof gist not independently reconstructed.* Candidate references: `eq:upper-omega` (internal_reference); `eq:strange-nbhd-condition` (internal_reference). ### Defn 9.6 — `def:structure-randomness` Source lines 2050–2067. \par Let $s'>0$, $\Pi(x)$ and $\tilde \mu$ be as in Definition \ref{def:kakeya-model}. To fit our case, let us assume that for any $y \in \fJ$, $$\cW(y) = \tilde \mu(\Omega'(y)) \le e^{-2 d_i s' } e^{-2s'}.$$ By Lemma \ref{lm:concentrated-surface}, for every $y \in \fJ$ and $z \in \cI$ from the same cross-section $\Sigma^r$, there is a corresponding neighborhood $\cC(\cT(y), z) \subset \fC$. \par Let us consider the summation \[ \fS(\cT(y), z) := \sum_{\substack{ y' \in \cI_z \\ \fD_z(y') \in \cC(\cT(y), z)\cap \fB(\cT(y), z) }} \cW(y'). \] Let *Extractive statement; proof gist not independently reconstructed.* Candidate references: `def:kakeya-model` (internal_reference); `lm:concentrated-surface` (internal_reference); `eq:hyperbola-box` (internal_reference); `subsec-constants` (internal_reference). ### Remark 9.7 — `remark:line:2069` Source lines 2069–2076. Note that $\fS(\cT (y), z) $ is essentially the $\tilde\mu$-measure of a subset of $\Theta'(z)$ with $r$ so that $z,y \in \Sigma^r$ (in particular, up to edge effects, $\Theta'(z)$ is a subset of $\Sigma^r$). Thus \[ \fS(\cT(y),z) \lessapprox \tilde\mu(\Sigma^r) \leq e^{-2s'}. \] Thus, if $d_i<1$ there can be no highly concentrated curve neighborhoods. Moreover if $\Theta'(z)$ is not extremely heavy, then unless $d_i >2-O(\epsilon_1)$ then $ \cC(\cT(y),z)$ is not highly concentrated. *Extractive statement; proof gist not independently reconstructed.* ### Defn 9.8 — `def:structure-random-decompostion` Source lines 2078–2098. \par Given $z \in \cI$ such that $\Theta'(z)$ is heavy and normal, and $\Sigma^r$ such that $z \in \Sigma^r$, let us define: \HS(z,r) := \left\{ y \in \fJ\cap \Sigma^r: \cC(\cT(y), z) \subset \fC \text{ is highly concentrated} \right\}, and \SS(z,r) := \bigcup_{y \in \HS(z, r)} \Omega'(y). If there exists $\Sigma^r$ containing $z$ such that \[ \tilde \mu (\SS(z,r)) \ge e^{-2s' - 10 C_1 \epsilon_1 s'}, \] we will call $\Theta'(z)$ highly structured. Then we have the following decomposition for $\bar \cR_i$: \bar \cR_i = \bar \cR^{\fr}_{i} \cup \ *Extractive statement; proof gist not independently reconstructed.* ### Prop 9.9 — `prop:dimension-improvement-random` Source lines 2099–2103. \[ \tilde \mu (\bar \cR^{\fr}_{i}) \le \beta^{22}. \] *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par For a contradiction, let us assume $\tilde \mu(\bar \cR^{\fr}_i) \ge \beta^{22}$. \par For every $y \in \bar \cR^{\fr}_i$, if \[ |u(\fl(y))y \cap \bar \cR^{\fr}_i| \ge \beta^{31} e^{2s'}, \] we will call it a good point. Otherwise, we call it a bad point. Then it is easy to see that the collection of bad points has $\tilde \mu$-measure $\le \beta^{30}$. Therefore, the collection of good points in $\bar \cR^{\fr}_i$, denoted by $\cR'_{i}$, has $\tilde \mu$-measure $\ge \beta^{22.1}$. \par For $r \in [\beta e^{2s'}]$, we say that the cross-section $\Sigma^r \subset \Pi(x)$ is a good cross-section if \[ \tilde \mu_{\fr}(\cR'_i \cap \Sigma^r) \ge \beta^{30} \tilde \mu_{\fr}(\Sigma^r).\] Oth Candidate references: `eq:omega-y-r` (candidate_proof_dependency); `eq:assumption-1` (candidate_proof_dependency); `lm:time-leave` (candidate_proof_dependency); `lm:concentrated-surface` (candidate_proof_dependency); `eq:fScT` (candidate_proof_dependency); `eq:cS-lower-bound` (candidate_proof_dependency). ### Prop 9.10 — `prop:dimension-improvement-strange-part` Source lines 2220–2225. For any $ C_1 \epsilon_1 s' \le j \le 2s' $, we have \[ \tilde{\mu}(\cR_{i,j}) \le \beta^{22}. \] *Extractive statement; proof gist not independently reconstructed.* Proof opening: For each $\Theta'(\bar z) \subset \cR_{i,j}$, fix a subset $\Xi_j(z) \subset \Theta'(\bar z)$ as in \eqref{eq:strange-nbhd-condition} and let $\cR'_{i,j}$ denote the union of all of those $\Xi_j(z)$ for $\Theta'(\bar z) \subset \cR_{i,j}$. To prove $\tilde \mu_{\fr}(\cR_{i,j}) < \beta^{22} $, it suffices to show that $\tilde \mu_{\fr}(\cR'_{i,j}) < \beta^{22.1}$. \par Assume in contradiction that $\tilde \mu_{\fr}(\cR'_{i,j}) \ge \beta^{22.1}$. Using similar arguments as in the proof of Proposition \ref{prop:dimension-improvement-random}, we can get a subset $\cR''_{i,j} \subset \cR'_{i,j} $ such that $\tilde \mu_{\fr}(\cR''_{i,j}) \ge \beta^{22.2}$ and for any $y \in \cR''_{i,j}$, \[|u(\fl( Candidate references: `eq:strange-nbhd-condition` (candidate_proof_dependency); `prop:dimension-improvement-random` (candidate_proof_dependency); `lm:time-leave` (candidate_proof_dependency); `eq: triple sum` (candidate_proof_dependency); `lem:sigma j lemma` (candidate_proof_dependency); `lm:concentrated-surface` (candidate_proof_dependency); `eq:fScT` (candidate_proof_dependency); `lm:initial-dimension-under-a-t` (candidate_proof_dependency); `eq:cIy2j` (candidate_proof_dependency); `eq:j lower bound` (candidate_proof_dependency). ### Lemma 9.11 — `lem:sigma j lemma` Source lines 2293–2298. If there is at least one $y_1\in \cI_{ z} \cap \Xi_j (z')$ so that $(y_2, y_1) \in \diamond_{r,j}$ then \[ z' \in \Sigma_{s', j-1} (y_2). \] *Extractive statement; proof gist not independently reconstructed.* Proof opening: Since $z', y_2 \in \Sigma^r$, it suffices to show that \[ z' \in \Pi_{s', j-1}(y_2). \] Write \[ y_1 = a_0 a u^\ast (r^\ast_{y_1})\exp(\vv w^-) \exp(\vv w^+) u(r_{y_1}) y_2, \] where $\vv w^- \in \vv r^-$ satisfies that $\|\vv w^-\| \in [\beta e^{-s' - j-1}, \beta e^{-s' - j }]$. Then by Lemma~\ref{lm:concentrated-surface}, we have $\|\vv w^+\| \le \beta e^{s' - j}$. Let $\hat y_1 = a(-2t) y_1, \hat y_2 = a(-2t) y_2$. Then we have \[ \hat y_1 = a_0 a u^\ast (\hat r^\ast) \exp (\hat{ \vv w}^-)\exp (\hat{ \vv w}^+) u(\hat r) \hat y_2,\] where $\hat r^\ast, \hat r \in [\beta]$, $\hat{\vv w}^- \in B_{\vv r^-}(\beta e^{-j})$, and $\hat{\vv w}^+ \in B_{\vv r^+}(\beta e^{-j})$. By Lemma \ref{lm:pro Candidate references: `lm:concentrated-surface` (candidate_proof_dependency); `lm:product-w` (candidate_proof_dependency); `eq:hat-y1-y2` (candidate_proof_dependency); `eq:hat-y1-z` (candidate_proof_dependency). ### Prop 10.1 — `prop:dimension-does-not-drop` Source lines 2381–2389. Let us keep the notation as in Proposition \ref{prop:improve-dimension}. Then there exists $\mathfrak{Z} \subset \Pi(x)$ with $\tilde \mu(\mathfrak Z) \le \beta^{50}$ such that for $x \in \cI\setminus\mathfrak{Z}$, \tilde \mu(\Theta'(x)) \le e^{-2s'} e^{-(d_i - C_1 \epsilon_1)s'}. *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par For $z \in \cI$, let us call $\Theta'(z)$ extremely heavy if \[ \tilde \mu(\Theta'(z)) > \tilde M_{s'} \qquad\text{for $ \tilde M_{s'}= e^{-2s'} e^{-(d_i - C_1 \epsilon_1)s'}$}. \] Let $\mathfrak Z$ denote the union of extremely heavy $\Theta'(z)$'s. Then it suffices to show that \[ \tilde \mu (\mathfrak Z ) \le \beta^{50}. \] Similarly to \eqref{eq:strange-normal-decomposition}, let us decompose \[ \fZ = \fZ' \cup \bigcup_{ C_1 \epsilon_1 s' \le j \le 2s'} \fZ_j. \] Here $\fZ'$ denotes the union of extremely heavy $\Theta'(z)$ such that for any $$\Xi_{C_1 \epsilon_1 s'} (y) \subset \Theta'(z),$$ we have \[ \tilde \mu(\Xi_{C_1 \epsilon_1 s'} (y)) \le (1- \beta) \tilde \mu (\Theta'(z)); Candidate references: `prop:improve-dimension` (internal_reference); `eq:strange-normal-decomposition` (candidate_proof_dependency); `prop:dimension-improvement-random` (candidate_proof_dependency); `eq:theta sum'` (candidate_proof_dependency); `eq: y_2 sum for diamond'` (candidate_proof_dependency); `lm:concentrated-surface` (candidate_proof_dependency); `eq:fScT` (candidate_proof_dependency); `prop:dimension-improvement-strange-part` (candidate_proof_dependency). ### Prop 11.1 — `prop:dimension-improvement-structured-component` Source lines 2562–2567. Suppose $ d_i \le 4 - 10^{11} C_1 \epsilon_1 $. We have \[ \tilde \mu (\bar \cR^{\fs}_i) \le \beta^{22}. \] *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Assume in contradiction that \[ \tilde \mu (\bar \cR^{\fs}_i) > \beta^{22}. \] Let $\fZ \subset \Pi(x)$ be the subset from Proposition \ref{prop:dimension-does-not-drop}. By replacing $\bar \cR^{\fs}_i$ with $\bar \cR^{\fs}_i \setminus \mathfrak{Z}$, we can assume that \eqref{eq:upper-theta} holds for any $z \in \cI \cap \bar\cR^{\fs}_i$. Thus we may assume: \cI \cap \bar \cR^{\fs}_i \neq \emptyset \\ \tilde \mu ( \Theta'(z)) \le e^{-2s'} e^{-(d_i - C_1 \epsilon_1) s'} \qquad \text{for any $z \in \cI \cap \bar \cR^{\fs}_i$} { \par Let us fix a $z \in \cI\cap \bar \cR^{\fs}_i$. By the definition of $\bar \cR^{\fs}_i$ (see Definition \ref{def:structure-random-decompostion}), we have that - `prop:dimension-does-not-drop` (proof_dependency; curated_source_check): Let $\fZ \subset \Pi(x)$ be the subset from Proposition \ref{prop:dimension-does-not-drop}. - `lm:integrable-surface` (proof_dependency; curated_source_check): By Lemma \ref{lm:integrable-surface}, we have that for every highly concentrated curve neighborhood $\cC$, there exist at most - `lm:determine-curve-nbhd` (proof_dependency; curated_source_check): By Lemma \ref{lm:determine-curve-nbhd}, we have that the curve neighborhoods from $\mathfrak{L}_n(\cC, m_{\cC})$ are contained - `lm:counting-curves-nbhd` (proof_dependency; curated_source_check): By the last statement of Lemma \ref{lm:counting-curves-nbhd}, we have that each curve neighborhood from $\mathfrak{L}_n(\cC, m_{\cC})$ can cover at most - `lm:curve-in-N` (proof_dependency; curated_source_check): Indeed, by Lemma \ref{lm:curve-in-N}, there exists $z' \in \Theta'(z)$ so that the following holds: - `prop:sl2xr2-closing-lemma` (proof_dependency; curated_source_check): By our discussion at the beginning of \S \ref{sec-reduction}, Proposition \ref{prop:sl2xr2-closing-lemma} holds for $\mu_{\cF_i}$. Candidate references: `prop:dimension-does-not-drop` (candidate_proof_dependency); `eq:upper-theta` (candidate_proof_dependency); `def:structure-random-decompostion` (candidate_proof_dependency); `eq:upper-omega` (candidate_proof_dependency); `eq:SSzr` (candidate_proof_dependency); `eq:upper-theta-2` (candidate_proof_dependency); `eq:full-omega` (candidate_proof_dependency); `rmk:concentrated-surface` (candidate_proof_dependency); `item:line` (candidate_proof_dependency); `lm:integrable-surface` (candidate_proof_dependency); `def:comparable` (candidate_proof_dependency); `eq:structure-part-theta-0` (candidate_proof_dependency); `eq:structure-set-theta-0` (candidate_proof_dependency); `lm:curve-in-N` (candidate_proof_dependency); `sec-reduction` (candidate_proof_dependency); `prop:sl2xr2-closing-lemma` (candidate_proof_dependency); `eq:sszrN-small` (candidate_proof_dependency); `eq:nowweaim` (candidate_proof_dependency); 5 more in the JSON/interactive graph. ### Defn 11.2 — `def:full-omega` Source lines 2572–2580. For $z \in \fJ$, if \tilde \mu(\Omega'(z)) \ge e^{-2s'} e^{-2d_i s' - 8 C_1 \epsilon_1 s'}, we will call $\Omega'(z)$ full. Otherwise, we call it almost empty. *Extractive statement; proof gist not independently reconstructed.* ### Defn 11.3 — `def:comparable` Source lines 2580–2586. For $z \in \cI$, we say that two curve neighborhoods $\cC = \cC(\cT(y), z)$ and $\cC' = \cC(\cT(y'), z)$ are comparable if $\cC'$ is contained in a $e^{-3s' + 11 C_1 \epsilon_1 s'}$-neighborhood of $\cC$. Let us denote by \[ \cC' \approx \cC, \] if $\cC$ and $\cC'$ are comparable. *Extractive statement; proof gist not independently reconstructed.* ### Lemma 11.4 — `lm:hyperbola-plane` Source lines 2587–2607. Let $C \subset \fC = \left[1.2 \beta e^{-s'}\right]^2$ be a hyperbola with the following equation: \[ X = \frac{-Y}{w_1 Y + k}, \] where $|w_1| \in [e^{s' - 10 C_1 \epsilon_1 s'}, \beta e^{s'}]$, and $|k| \in [e^{\ell}, e^{\ell+1}]$ for some $\ell \in \Z_{\ge 0}, \ell \le s'$. Let $C' \subset \fC$ be another hyperbola with the following equation: \[ X = \frac{-Y}{w'_1 Y + k'},\] where $|w'_1| \in [e^{s' - 10 C_1 \epsilon_1 s'}, \beta e^{s'}]$. \par (1) For $0< A < e^{2s'-C_1\epsilon_1 s'}$, if $C'$ is contained in the $A e^{-3s'}$ neighborhood *Extractive statement; proof gist not independently reconstructed.* Candidate references: `eq:w1w'1` (internal_reference). ### Lemma 11.5 — `lm:integrable-surface` Source lines 2704–2717. For $y \in \fJ\cap \Sigma^r , z \in \cI\cap\Sigma^r$, let us denote \[\cC = \cC(\cT(y), z)\subset \fC = \left[1.2 \beta e^{-s'}\right]^2.\] Suppose that $\cC$ has equation \[ (X- X_0) (Y- Y_0) + v_1^{-1} (X- X_0) + w_1^{-1} (Y- Y_0) = 0, \] with $\| (v_1 , w_1) \| \ge e^{s' - 10 C_1 \epsilon_1 s'}$, and $$\max\{|v_1/w_1|, |w_1/v_1|\} \in [e^\ell, e^{\ell + 1}].$$ Then for $\ell < s'$, there exist at most $e^{2s' + 2\ell + 60C_1\epsilon_1 s'}$ different $y' \in \fJ\cap\Sigma^r$ such that \[\cC(\cT(y'), z) \approx \cC.\] \par For $\ell \ge s' $, *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par We first consider the case $\ell < s'$. For $A > 1$, let us denote by $\cC[A]$ the $Ae^{-3s'}$ neighborhood of $\cC$. \par Let us fix $z_0 \in \cI_z$ such that $\fD_z(z_0) = (X'_0, Y'_0) \in \cC[e^{11 C_1 \epsilon_1 s'}]$, and consider all $y' \in \fJ\cap \Sigma^r$ such that \[ \cC \approx \cC(\cT(y'), z). \] Assume in addition that $y'$ is such that there are coefficients $v_{1, y'},w_{1, y'}$ of size $\leq \beta e^{s'}$ and a point $y'_0 \in \Omega(y')$ such that \[ z_0 = \exp(v_{1, y'} \vv v_1 + w_{1, y'} \vv w_1) u(r_{y'}) y'_0. \] Let us denote by $\cM(\cC, z_0)$ the collection of those $y'$'s. \par Fix a $y \in \cM(\cC,z_0)$ and consider the curve neighborhood $\cC'$ with equation - `lm:hyperbola-plane` (proof_dependency; curated_source_check): By Lemma \ref{lm:hyperbola-plane}(1) with $A =2 e^{11C_1\epsilon_1 s'}$, we have that - `rmk:concentrated-surface` (proof_dependency; curated_source_check): In this case, by Remark \ref{rmk:concentrated-surface}, we can consider the corresponding straight lines Candidate references: `eq:prime curve` (candidate_proof_dependency); `eq:not prime curve` (candidate_proof_dependency); `lm:hyperbola-plane` (candidate_proof_dependency); `rmk:concentrated-surface` (candidate_proof_dependency). ### Lemma 11.6 — `lm:determine-curve-nbhd` Source lines 2777–2793. \par Let us fix constants $\ell, m \ge 1$. Let $\cC \subset \fC$ be the $\beta^{-100} e^{-3s'}$-neighborhood of the curve \[ (X- X_0) (Y- Y_0) + v_1^{-1} (X- X_0) + w_1^{-1} (Y- Y_0) = 0, \] with $\|(v_1, w_1)\| \ge e^{s' - 10C_1 \epsilon_1 s'}$ and \[ \max\{|v_1/w_1|, |w_1/v_1|\} \in [e^\ell, e^{\ell + 1}].\] Let $\cC'$ be the $\beta^{-100} e^{-3s'}$-neighborhood of the curve with the following equation \[(X- X_0) (Y- Y_0) + {v'_1}^{-1}(X- X_0) + {w'_1}^{-1}(Y- Y_0) = 0.\] Suppose we have that $\cC$ and $\cC'$ are not comparable. Moreover, sup *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Without loss of generality, we can assume that $(X_0, Y_0) = \vv 0$ and $|w_1/v_1| \in [e^\ell, e^{\ell+1}]$. Then we have $|w'_1/v'_1| \in [e^\ell, e^{\ell+1}]$, $|w_1 - w'_1| \in [e^{s'-m}, e^{s'-m+1}]$, and there exists $(X_1, Y_1) \in \cC \cap \cC'$ with $|Y_1| \ge e^{-s'-10C_1 \epsilon_1 s'}$. \par Let us rewrite the equation of $\cC$ as \[ X = \frac{-Y}{w_1 Y + k}, \text{ where } k = w_1/ v_1, \] and the equation of $\cC'$ as \[ X = \frac{-Y}{w'_1 Y + k'}, \text{ where } k' = w'_1/ v'_1. \] Since $(X_1, Y_1) \in \cC \cap \cC'$, we have \[ \left|\frac{Y_1}{w_1 Y_1 + k} - \frac{Y_1}{w'_{1}Y_1 + k'} \right| \le \beta^{-100}e^{-3s'}. \] By Lemma \ref{lm:hyperbola-plane}(2) with $A = e - `lm:hyperbola-plane` (proof_dependency; curated_source_check): By Lemma \ref{lm:hyperbola-plane}(2) with $A = e^{2s' - 2\ell -m}$ we have that $\cC'$ is contained in the $e^{-s' - m - 2\ell}$-neighborhood of $\cC$. Candidate references: `lm:hyperbola-plane` (candidate_proof_dependency). ### Lemma 11.7 — `lm:counting-curves-nbhd` Source lines 2805–2824. \par Let us fix constants $m, \ell \ge 1$ with $m+2\ell \le 2s' - 10 C_1 \epsilon_1 s'$. Let $\cC \subset \fC$ be the $\beta^{-100} e^{-3s'}$-neighborhood of the curve \[ (X- X_0) (Y- Y_0) + v_1^{-1} (X- X_0) + w_1^{-1} (Y- Y_0) = 0, \] with $\|(v_1, w_1)\| \ge e^{s' - 10C_1 \epsilon_1 s'}$ and \[ \max\{|v_1/w_1|, |w_1/v_1|\} \in [e^\ell, e^{\ell + 1}].\] Let $\fN( \cC, (X_0, Y_0), m)$ denote a collection of non-comparable $\beta^{-100} e^{-3s'}$-curve neighborhoods with equations of the form \[(X- X_0) (Y- Y_0) + {v'_1}^{-1} (X- X_0) + {w'_1}^ *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Without loss of generality, we can assume that $(X_0, Y_0)= \vv 0$, and $|w_1| \ge |v_1|$. \par Let us write the equation of $\cC$ as \[ X = \frac{-Y}{w_1 Y + k}, \text{ where } k = w_1/ v_1. \] Then $|k| \in [e^\ell, e^{\ell +1}]$. Suppose $\cC'$ with equation \[ X = \frac{-Y}{w'_1 Y + k'} \text{ where } k' = w'_1/v'_1 \] is in $\fN(\cC, \vv 0, m)$. Then we have for all $Y \in [ \beta e^{-s'}]$, \[ \left|\frac{Y}{w_1 Y + k} - \frac{Y}{w'_{1}Y + k'} \right| \le e^{-s' - m - 2\ell}.\] By Lemma \ref{lm:hyperbola-plane} (1) with $A = e^{2s' - m - 2 \ell}$, we have |w_1 - w'_{1}| \le e^{s' -m }, \text{ and } |k - k'| \le e^{-m }. Note that by Lemma \ref{lm:hyperbola-plane} (1) with $A = e^{ - `lm:hyperbola-plane` (proof_dependency; curated_source_check): By Lemma \ref{lm:hyperbola-plane} (1) with $A = e^{2s' - m - 2 \ell}$, we have Candidate references: `lm:hyperbola-plane` (candidate_proof_dependency); `eq:counting-conditions` (candidate_proof_dependency). ### Lemma 11.8 — `lm:curve-in-N` Source lines 2861–2871. Given $(X_0, Y_0) \in \fC = \left[1.2\beta e^{-s'}\right]^2$, and $1 < \ell \le s'$, let us denote \[ \cN^\ell = \cN^{\ell}(X_0, Y_0) := (X_0, Y_0) + [\beta e^{-s' - \ell}] \times [\beta e^{-s'}]. \] Suppose we have a cross-section $\Sigma^r$ and $z \in \cI \cap \Sigma^r$, $y \in \fJ\cap\Sigma^r$ such that $$\cC = \cC(\cT(y),z) \subset \cN^{\ell}.$$ Then there exists $z' \in \Theta(z)$ only depending on $\cN^\ell$ (and not on $\cC$) such that $\fD_z(z') \in \cN^{\ell}$ and \[ \Omega'(y) \subset a(2s')Q(\fr_1, \ell-1, \beta ) B^{A_0 H}(\beta) a( *Extractive statement; proof gist not independently reconstructed.* ### Remark 11.9 — `rmk:sl2r2` Source lines 2924–2933. Lemma \ref{lm:curve-in-N} roughly says that given $z \in \cI\cap \Sigma^r$ and $$ \cN^\ell = \cN^\ell(X_0, Y_0) \subset \fC$$ as above, all $y \in \fJ\cap \Sigma^r$ satisfying that \[ \cC(\cT(y), z) \subset \cN^\ell\] is contained in a $a(2s')$-translate of a $\beta e^{-\ell+1}$-neighborhood of a piece of some $\SL(2,\R)\ltimes \R^2$-orbit of size $\beta$. *Extractive statement; proof gist not independently reconstructed.* Candidate references: `lm:curve-in-N` (internal_reference). ### Prop 12.1 — `prop:high-dim-decomposition` Source lines 3243–3260. \par Let $s \le \hat s < t$, $s' =(t-\hat s)/2$, and $\hat \mu$ be a probability measure on $X_{\beta^{1/4}}$ defined by the normalized Lebesgue measure on the $U$-orbit $a(\hat s) u([1])x_0$ removed an exponentially small proportion. Suppose $\hat \mu$ is $(4-\theta, s')$-good. Then $a(2s')_\ast \hat \mu$ can be written as a(2s')_\ast \hat \mu = \nu_{\S} \mu_{\S} + \sum_{k} \nu_k a(2s')_\ast \mu_k, where $\mu_{\S}$ is a probability measure on $X$, $\nu_{\S} = O(\beta)$, and for each $k$, $\mu_k$ is a probability measure on $$\exp\left(B_{\vv r *Extractive statement; proof gist not independently reconstructed.* Proof opening: \par Let us define \Upsilon_{s'} := B^{A_0 A U^\ast}(\beta) \exp\left(B_{\vv r^-} (\beta e^{-s'})\right)\exp\left(B_{\vv r^+} (\beta)\right) B^{U}(\beta), and decompose $X_{\beta^{1/4}}$ as \[ X_{\beta^{1/4}} = \bigcup_{k=1}^{\beta^{-100} e^{2s'}} \Upsilon_{s'} x_k. \] We say $x_k$ is light if \[ \hat \mu\left( \Upsilon_{s'} x_k\right) \le \beta^{-2} e^{-2s' -\theta s'}. \] Otherwise we say $x_k$ is heavy. For each heavy $x_k$, let us denote \[ \bar{\nu}_k = \hat \mu \left( \Upsilon_{s'} x_k \right), \] and \[ \bar{\mu}_k = \bar{\nu}^{-1}_k \hat \mu|_{ \Upsilon_{s'} x_k}.\] Let us define \[ \Upsilon_{\mathrm{light}} := \bigcup_{x_k \text{ light }} \Upsilon_{s'} x_k.\] Then it is easy to see Candidate references: `prop:high-dimension-to-equidistribution-a` (internal_reference); `eq:fvy` (candidate_proof_dependency); `eq:fwy` (candidate_proof_dependency); `eq:fy` (candidate_proof_dependency); `eq:compare-u-orbit` (candidate_proof_dependency); `eq:bary-y-Qs` (candidate_proof_dependency); `eq:first-decompose-hat-mu` (candidate_proof_dependency); `eq:decompose-hat-mu` (candidate_proof_dependency). ### Retained mass: (6.7) — `claim:retained-proportion` Source lines 1040–1040. Initial retained-set estimate The removed proportion is claimed to be exponentially small. - `prop:quantitative-nondivergence` (proof_dependency; curated_source_check): \par By Proposition \ref{prop:quantitative-nondivergence} and our assumption on $x_{\mathrm{initial}}$, it is easy to show that ## External inputs and references ### [BKM01] Bernik-Kleinbock-Margulis — `external:Bernik-Kleinbock-Margulis` Source lines 3358–3365. V~Bernik, D~Kleinbock, and Gregory~A Margulis. \newblock Khintchine-type theorems on manifolds: the convergence case for standard and multiplicative versions. \newblock {\em International Mathematics Research Notices}, 2001(9):453--486, 2001. - `cor:curve` (proof_dependency; curated_source_check): By \cite[Theorem 1.4]{Bernik-Kleinbock-Margulis}, we have that Candidate references: `thm:main-thm` (external_reference). ### [Bur90] burger1990 — `external:burger1990` Source lines 3365–3370. Marc Burger. \newblock Horocycle flow on geometrically finite surfaces. \newblock {\em Duke Mathematical Journal}, 61(3):779--803, 1990. Candidate references: `sec-intro` (external_reference). ### [BV16] Browning2016 — `external:Browning2016` Source lines 3370–3377. Tim Browning and Ilya Vinogradov. \newblock Effective {Ratner} theorem for $\operatorname{SL}(2,\mathbb{R})\ltimes\mathbb{R}^{2}$ and gaps in $ \sqrt{n}$ modulo $1$. \newblock {\em Journal of the London Mathematical Society}, 94(1):61--84, 2016. Candidate references: `sec-intro` (external_reference). ### [CY24] chow-yang — `external:chow-yang` Source lines 3377–3383. Sam Chow and Lei Yang. \newblock Effective equidistribution for multiplicative diophantine approximation on lines. \newblock {\em Inventiones mathematicae}, 235(3):973--1007, 2024. Candidate references: `sec-intro` (external_reference). ### [Dan81] Dani1981 — `external:Dani1981` Source lines 3383–3388. S.~G. Dani. \newblock Invariant measures and minimal sets of horospherical flows. \newblock {\em Inventiones mathematicae}, 64(2):357--385, 1981. Candidate references: `sec-intro` (external_reference). ### [DS84] dani-smillie — `external:dani-smillie` Source lines 3388–3393. Shrikrishna~G Dani and John Smillie. \newblock Uniform distribution of horocycle orbits for fuchsian groups. \newblock {\em Duke Mathematical Journal}, 51(1):185--194, 1984. Candidate references: `sec-intro` (external_reference). ### [Edw21] edwards-effective — `external:edwards-effective` Source lines 3393–3399. Samuel Edwards. \newblock On the rate of equidistribution of expanding translates of horospheres in ${\Gamma} \setminus {G}$. \newblock {\em Commentarii Mathematici Helvetici}, 96(2):275--337, 2021. Candidate references: `sec-intro` (external_reference). ### [EM22] einsiedler-mohammadi — `external:einsiedler-mohammadi` Source lines 3399–3405. M~Einsiedler and A~Mohammadi. \newblock Effective arguments in unipotent dynamics. \newblock {\em Dynamics, geometry, number theory: the impact of margulis on modern mathematics}, 2022. Candidate references: `sec-intro` (external_reference). ### [EMMV20] einsiedler-margulis-mohammadi-venkatesh — `external:einsiedler-margulis-mohammadi-venkatesh` Source lines 3405–3410. Einsiedler, Margulis, Mohammadi, and Venkatesh. \newblock Effective equidistribution and property $(\tau)$. \newblock {\em Journal of the AMS}, 33(1), 2020. Candidate references: `sec-intro` (external_reference). ### [EMV09] einsiedler-margulis-venkatesh — `external:einsiedler-margulis-venkatesh` Source lines 3410–3416. Manfred Einsiedler, Gregory Margulis, and Akshay Venkatesh. \newblock Effective equidistribution for closed orbits of semisimple groups on homogeneous spaces. \newblock {\em Inventiones mathematicae}, 177(1):137--212, 2009. - `prop:initial-bound-dimension` (proof_dependency; curated_source_check): By repeating the same argument as in \cite{einsiedler-margulis-venkatesh}, Candidate references: `sec-intro` (external_reference); `prop:initial-bound-dimension` (external_reference). ### [FF03] Flaminio-Forni — `external:Flaminio-Forni` Source lines 3416–3421. Livio Flaminio and Giovanni Forni. \newblock Invariant distributions and time averages for horocycle flows. \newblock {\em Duke Math. J.}, 119(3):465--526, 2003. Candidate references: `sec-intro` (external_reference). ### [Fur73] furstenberg1973 — `external:furstenberg1973` Source lines 3421–3427. Harry Furstenberg. \newblock The unique ergodigity of the horocycle flow. \newblock In {\em Recent advances in topological dynamics}, pages 95--115. Springer, 1973. Candidate references: `sec-intro` (external_reference). ### [GT12] green_tao2012 — `external:green_tao2012` Source lines 3427–3432. Ben Green and Terence Tao. \newblock The quantitative behaviour of polynomial orbits on nilmanifolds. \newblock {\em Annals of Mathematics}, 175(2):465--540, 2012. Candidate references: `sec-intro` (external_reference). ### [KdSSY24] KNSY — `external:KNSY` Source lines 3432–3438. Dmitry Kleinbock, Nicolas de~Saxc\'e, Nimish~A. Shah, and Pengyu Yang. \newblock Equidistribution in the space of 3-lattices and {D}irichlet-improvable vectors on planar lines. \newblock {\em Ann. Sc. Norm. Super. Pisa Cl. Sci. (5)}, 25(1):565--604, 2024. Candidate references: `rmk:expanding-line` (external_reference). ### [Kim21] kim2021 — `external:kim2021` Source lines 3438–3444. Wooyeon Kim. \newblock Effective equidistribution of expanding translates in the space of affine lattices. \newblock {\em arXiv preprint arXiv:2110.00706}, 2021. Candidate references: `sec-intro` (external_reference). ### [Kle08] kleinbock2008 — `external:kleinbock2008` Source lines 3444–3451. Dmitry Kleinbock. \newblock An extension of quantitative nondivergence and applications to diophantine exponents. \newblock {\em Transactions of the American Mathematical Society}, 360(12):6497--6523, 2008. - `prop:quantitative-nondivergence` (proof_dependency; curated_source_check): By the Kleinbock-Margulis quantitative non-divergence theorem (cf. \cite[Theorem 2.2]{kleinbock2008}, \cite[Theorem 5.2]{Klein_Mar}), if the statement does not hold then there exists Candidate references: `prop:quantitative-nondivergence` (external_reference). ### [KM98] Klein_Mar — `external:Klein_Mar` Source lines 3451–3457. Dmitry Kleinbock and Gregory Margulis. \newblock Flows on homogeneous spaces and diophantine approximation on manifolds. \newblock {\em Annals of Mathematics}, pages 339--360, 1998. - `prop:quantitative-nondivergence` (proof_dependency; curated_source_check): By the Kleinbock-Margulis quantitative non-divergence theorem (cf. \cite[Theorem 2.2]{kleinbock2008}, \cite[Theorem 5.2]{Klein_Mar}), if the statement does not hold then there exists Candidate references: `prop:quantitative-nondivergence` (external_reference). ### [KM12] Klein-Mar-Effective-Equid — `external:Klein-Mar-Effective-Equid` Source lines 3457–3463. Dmitry Kleinbock and Gregory Margulis. \newblock {\em On effective equidistribution of expanding translates of certain orbits in the space of lattices}, pages 385--396. \newblock Springer, Boston, MA, 2012. Candidate references: `sec-intro` (external_reference). ### [LM14] lindenstrauss-margulis — `external:lindenstrauss-margulis` Source lines 3463–3468. Elon Lindenstrauss and Gregory Margulis. \newblock Effective estimates on indefinite ternary forms. \newblock {\em Israel Journal of Mathematics}, 203(1):445--499, 2014. Candidate references: `sec-intro` (external_reference). ### [LM23] LM-preprint2021 — `external:LM-preprint2021` Source lines 3468–3474. Elon Lindenstrauss and Amir Mohammadi. \newblock Polynomial effective density in quotients of $\mathbb{H}^3$ and $\mathbb{H}^2 \times \mathbb{H}^2$. \newblock {\em Inventiones Mathematicae}, 231(3):1141--1237, 2023. - `prop:high-dimension-to-equidistribution-a` (proof_dependency; curated_source_check): The statement can be proved by following the proof of \cite[Proposition 4.2]{LM-preprint2021} step by step. Candidate references: `sec-intro` (external_reference); `sec-prelim` (external_reference); `sec-high-dim-to-equidistribution` (external_reference); `prop:high-dimension-to-equidistribution-a` (external_reference). ### [LMW23] LMW-preprint2022 — `external:LMW-preprint2022` Source lines 3474–3479. Elon Lindenstrauss, Amir Mohammadi, and Zhiren Wang. \newblock Polynomial effective equidistribution. \newblock {\em Comptes Rendus. Math{\'e}matique}, 361(G2):507--520, 2023. Candidate references: `sec-intro` (external_reference); `sec-prelim` (external_reference). ### [Mar04] margulis-thesis — `external:margulis-thesis` Source lines 3479–3485. Gregory~Aleksandrovitsch Margulis. \newblock On some aspects of the theory of anosov systems. \newblock In {\em On Some Aspects of the Theory of Anosov Systems}, pages 1--71. Springer, 2004. Candidate references: `sec-intro` (external_reference). ### [MS95] Mozes_Shah — `external:Mozes_Shah` Source lines 3485–3490. Shahar Mozes and Nimish Shah. \newblock On the space of ergodic invariant measures of unipotent flows. \newblock {\em Ergodic Theory and Dynamical Systems}, 15(01):149--159, 1995. Candidate references: `sec-intro` (external_reference). ### [NV21] nelson-venkatesh — `external:nelson-venkatesh` Source lines 3490–3495. P.~Nelson and A.~Venkatesh. \newblock The orbit method and analysis of automorphic forms. \newblock {\em Acta Mathematica}, 226(1), 2021. Candidate references: `sec-intro` (external_reference). ### [Rat90a] ratner-acta — `external:ratner-acta` Source lines 3495–3500. Marina Ratner. \newblock On measure rigidity of unipotent subgroups of semisimple groups. \newblock {\em Acta mathematica}, 165:229--309, 1990. Candidate references: `sec-intro` (external_reference); `sec-prelim` (external_reference). ### [Rat90b] ratner-invent — `external:ratner-invent` Source lines 3500–3505. Marina Ratner. \newblock Strict measure rigidity for unipotent subgroups of solvable groups. \newblock {\em Inventiones mathematicae}, 101(1):449--482, 1990. Candidate references: `sec-intro` (external_reference). ### [Rat91a] Ratner — `external:Ratner` Source lines 3505–3510. Marina Ratner. \newblock On {Raghunathan's} measure conjecture. \newblock {\em Annals of Mathematics}, pages 545--607, 1991. Candidate references: `sec-intro` (external_reference). ### [Rat91b] ratner_2 — `external:ratner_2` Source lines 3510–3516. Marina Ratner. \newblock Raghunathan's topological conjecture and distributions of unipotent flows. \newblock {\em Duke Math. J}, 63(1):235--280, 1991. Candidate references: `sec-intro` (external_reference). ### [Sar82] sarnak1982 — `external:sarnak1982` Source lines 3516–3523. Peter Sarnak. \newblock Asymptotic behavior of periodic orbits of the horocycle flow and eisenstein series. \newblock {\em Communications on Pure and Applied Mathematics}, 34(6):719--739, 1982. Candidate references: `sec-intro` (external_reference). ### [Sha09] Shah_2 — `external:Shah_2` Source lines 3523–3529. Nimish~A Shah. \newblock Equidistribution of expanding translates of curves and {Dirichlet's} theorem on diophantine approximation. \newblock {\em Inventiones mathematicae}, 177(3):509--532, 2009. Candidate references: `rmk:expanding-curve` (external_reference). ### [Str04] Strombergsson2004 — `external:Strombergsson2004` Source lines 3529–3534. Andreas Str{\"o}mbergsson. \newblock On the uniform equidistribution of long closed horocycles. \newblock {\em Duke Math. J.}, 123(3):507--547, 06 2004. Candidate references: `sec-intro` (external_reference). ### [Str13] Strombergsson2013 — `external:Strombergsson2013` Source lines 3534–3539. Andreas Str{\"o}mbergsson. \newblock On the deviation of ergodic averages for horocycle flows. \newblock {\em Journal of Modern Dynamics}, 7:291, 2013. Candidate references: `sec-intro` (external_reference). ### [Str15] Strombergsson2015 — `external:Strombergsson2015` Source lines 3539–3545. Andreas Str{\"o}mbergsson. \newblock An effective {Ratner} equidistribution result for $\operatorname{SL}(2,\mathbb{R})\ltimes\mathbb{R}^{2}$. \newblock {\em Duke Mathematical Journal}, 164(5):843--902, 04 2015. Candidate references: `sec-intro` (external_reference). ### [SU15] Sarnak-Ubis — `external:Sarnak-Ubis` Source lines 3545–3551. Peter Sarnak and Adri{\'a}n Ubis. \newblock The horocycle flow at prime times. \newblock {\em Journal de Mathématiques Pures et Appliquées}, 103(2):575--618, 2015. Candidate references: `sec-intro` (external_reference). ### [Ven10] Venkatesh2010 — `external:Venkatesh2010` Source lines 3551–3556. A.~Venkatesh. \newblock Sparse equidistribution problems, period bounds and subconvexity. \newblock {\em Annals of Mathematics}, 172:989--1094, 2010. - `prop:high-dimension-to-equidistribution-a` (proof_dependency; curated_source_check): It can be proved by following Venkatesh's argument (\cite[\S 3]{Venkatesh2010} and \cite[Proposition 4.2]{LM-preprint2021} for details). Candidate references: `sec-intro` (external_reference); `sec-high-dim-to-equidistribution` (external_reference). ## Coverage and limits {"mode": "native_latex_index", "claims": 56, "sections": 12, "external_references": 35, "source_bibliography_entries": 35, "unresolved_bibliography": 0, "unresolved": 0} - Reference edges are not certified proof dependencies. Edge direction is prerequisite → consumer. - Numbers reflect simple source counters; labels and line anchors are authoritative. - Extractive statements and proof openings are marked; they are not reconstructed proof gists. - Macros, included files and custom counters require an expanded source or annotated fallback. - This map adds only the selected source-audited proof edges. Other isolated claims and terminal nodes do not establish mathematical independence. - An indexed reference and a literal proof-use quotation establish an intended dependency, not proof of its hypotheses.