fix: MathJax rendering in theorem blocks and display math

docs/exposition/coincidence-length.md

@@ -2,9 +2,7 @@
 
 In his landmark 1981 paper, Takens proved that for a compact manifold \(M\) of dimension \(m\), the delay coordinate map
 
-\[
-\Phi_{(\varphi, y)}(x) = \bigl(y(x),\; y(\varphi(x)),\; \ldots,\; y(\varphi^{2m}(x))\bigr)
-\]
+$$\Phi_{(\varphi, y)}(x) = \bigl(y(x),\; y(\varphi(x)),\; \ldots,\; y(\varphi^{2m}(x))\bigr)$$
 
 is an embedding for **generic** pairs \((\varphi, y)\) in the \(C^2\) topology --- that is, for a residual set (in the sense of Baire category) of diffeomorphisms \(\varphi : M \to M\) and observations \(y : M \to \mathbb{R}\).
 
@@ -22,9 +20,7 @@ Given a dynamical system \(f : X \to X\) and an observation \(\alpha : X \to \ma
 
 **Definition.** Let \(f : X \to X\) and \(\alpha : X \to \mathbb{R}\). The *coincidence length* of two states \(x, y \in X\) is
 
-\[
-\mathrm{coinc}(x, y) \;=\; \begin{cases} \min\bigl\{\, i \in \mathbb{N} \;\big|\; \alpha(f^i(x)) \neq \alpha(f^i(y)) \,\bigr\} & \text{if such } i \text{ exists,} \\[4pt] \infty & \text{otherwise.} \end{cases}
-\]
+$$\mathrm{coinc}(x, y) \;=\; \begin{cases} \min\bigl\{\, i \in \mathbb{N} \;\big|\; \alpha(f^i(x)) \neq \alpha(f^i(y)) \,\bigr\} & \text{if such } i \text{ exists,} \\[4pt] \infty & \text{otherwise.} \end{cases}$$
 
 The coincidence length takes values in \(\mathbb{N}_\infty = \mathbb{N} \cup \{\infty\}\). It is finite for a pair \((x, y)\) precisely when the observation \(\alpha\) eventually distinguishes the orbits of \(x\) and \(y\).
 </div>
@@ -51,9 +47,7 @@ The coincidence length leads directly to a sharp characterization of when a non-
 
 Recall that the delay embedding of window length \(k\) is defined as
 
-\[
-\Phi_k(x) = \bigl(\alpha(x),\; \alpha(f(x)),\; \ldots,\; \alpha(f^{k-1}(x))\bigr) \in \mathbb{R}^k,
-\]
+$$\Phi_k(x) = \bigl(\alpha(x),\; \alpha(f(x)),\; \ldots,\; \alpha(f^{k-1}(x))\bigr) \in \mathbb{R}^k,$$
 
 and we say \(\alpha\) **separates \(f\)-orbits of length \(k\)** if \(\Phi_k\) is injective: whenever \(\alpha(f^i(x)) = \alpha(f^i(y))\) for all \(0 \leq i < k\), then \(x = y\).
 
@@ -68,15 +62,11 @@ and we say \(\alpha\) **separates \(f\)-orbits of length \(k\)** if \(\Phi_k\) i
 
 Equivalently, in terms of the coincidence length:
 
-\[
-\bigl(\exists\, k.\; \Phi_k \text{ is injective}\bigr) \;\iff\; \bigl(\forall\, x \neq y.\; \mathrm{coinc}(x, y) < \infty\bigr).
-\]
+$$\bigl(\exists\, k.\; \Phi_k \text{ is injective}\bigr) \;\iff\; \bigl(\forall\, x \neq y.\; \mathrm{coinc}(x, y) < \infty\bigr).$$
 
 Moreover, when these conditions hold, the witness \(k\) is constructed explicitly as
 
-\[
-k \;=\; 1 + \max_{x, y \in X}\, \mathrm{coinc}(x, y),
-\]
+$$k \;=\; 1 + \max_{x, y \in X}\, \mathrm{coinc}(x, y),$$
 
 the supremum of all pairwise coincidence lengths, plus one.
 </div>
@@ -105,9 +95,7 @@ The proof of the reverse direction (2 implies 1) uses finiteness of \(X\) in an
 
 **Connection to the main injectivity theorem.** The separating window theorem sits naturally alongside `delayEmbedding_injective_iff_separatesOrbits`, which establishes
 
-\[
-\Phi_k \text{ is injective} \;\iff\; \operatorname{SeparatesOrbits}(f, \alpha, k).
-\]
+$$\Phi_k \text{ is injective} \;\iff\; \operatorname{SeparatesOrbits}(f, \alpha, k).$$
 
 Together, these two theorems give a complete picture: the injectivity--separation equivalence characterizes *what it means* for a given window to work, while the separating window theorem characterizes *whether any window can work at all* and how large it must be.
 

docs/exposition/delay-embedding.md

@@ -5,9 +5,7 @@ dynamical system \(f : X \to X\) and a scalar observation \(\alpha : X \to \math
 the delay embedding of window length \(k\) maps each state \(x\) to the vector
 of consecutive observations along its orbit,
 
-\[
-\Phi_{f,\alpha,k}(x) \;=\; \bigl(\alpha(x),\; \alpha(f(x)),\; \dots,\; \alpha(f^{k-1}(x))\bigr) \;\in\; \mathbb{R}^k.
-\]
+$$\Phi_{f,\alpha,k}(x) \;=\; \bigl(\alpha(x),\; \alpha(f(x)),\; \dots,\; \alpha(f^{k-1}(x))\bigr) \;\in\; \mathbb{R}^k.$$
 
 The headline result of this module is an exact characterization: the delay
 embedding is injective if and only if the observation function separates
@@ -21,9 +19,9 @@ is the foundation on which the rest of Route B is built.
 <span class="theorem-name">(delayEmbedding)</span>
 
 **Definition.** The *delay embedding* of window length \(k\) for dynamics \(f : X \to X\) and observation \(\alpha : X \to \mathbb{R}\) is the map
-\[
-\Phi_{f,\alpha,k} : X \to \mathbb{R}^k, \qquad \Phi_{f,\alpha,k}(x)(i) = \alpha(f^i(x)), \quad 0 \le i < k.
-\]
+
+$$\Phi_{f,\alpha,k} : X \to \mathbb{R}^k, \qquad \Phi_{f,\alpha,k}(x)(i) = \alpha(f^i(x)), \quad 0 \le i < k.$$
+
 </div>
 
 <details>
@@ -40,9 +38,9 @@ def delayEmbedding (f : X → X) (α : X → ℝ) (k : ℕ) (x : X) : Fin k →
 <span class="theorem-name">(SeparatesOrbits)</span>
 
 **Definition.** An observation \(\alpha\) *separates \(f\)-orbits of length \(k\)* if, for all \(x, y \in X\),
-\[
-\bigl(\forall\, 0 \le i < k,\; \alpha(f^i(x)) = \alpha(f^i(y))\bigr) \;\Longrightarrow\; x = y.
-\]
+
+$$\bigl(\forall\, 0 \le i < k,\; \alpha(f^i(x)) = \alpha(f^i(y))\bigr) \;\Longrightarrow\; x = y.$$
+
 </div>
 
 <details>
@@ -78,9 +76,9 @@ def WindowDistinct (f : X → X) (α : X → ℝ) (k : ℕ) (x : X) : Prop :=
 <span class="theorem-name">(delayEmbedding_injective_iff_separatesOrbits)</span>
 
 **Theorem.** The delay embedding \(\Phi_{f,\alpha,k}\) is injective if and only if \(\alpha\) separates \(f\)-orbits of length \(k\):
-\[
-\Phi_{f,\alpha,k} \text{ injective} \;\iff\; \operatorname{SeparatesOrbits}(f, \alpha, k).
-\]
+
+$$\Phi_{f,\alpha,k} \text{ injective} \;\iff\; \operatorname{SeparatesOrbits}(f, \alpha, k).$$
+
 </div>
 
 <details>
@@ -122,9 +120,9 @@ theorem delayEmbedding_continuous [TopologicalSpace X]
 <span class="theorem-name">(delayEmbedding_image_card_le)</span>
 
 **Theorem.** On a finite type \(X\), the number of distinct delay windows is at most \(|X|\):
-\[
-\bigl|\{\Phi_{f,\alpha,k}(x) : x \in X\}\bigr| \;\le\; |X|.
-\]
+
+$$\bigl|\{\Phi_{f,\alpha,k}(x) : x \in X\}\bigr| \;\le\; |X|.$$
+
 </div>
 
 <details>
@@ -142,9 +140,9 @@ theorem delayEmbedding_image_card_le [Fintype X]
 <span class="theorem-name">(delayEmbedding_image_card_of_injective)</span>
 
 **Theorem.** If \(\Phi_{f,\alpha,k}\) is injective on a finite type, the image has exactly \(|X|\) elements:
-\[
-\Phi_{f,\alpha,k} \text{ injective} \;\Longrightarrow\; \bigl|\{\Phi_{f,\alpha,k}(x) : x \in X\}\bigr| = |X|.
-\]
+
+$$\Phi_{f,\alpha,k} \text{ injective} \;\Longrightarrow\; \bigl|\{\Phi_{f,\alpha,k}(x) : x \in X\}\bigr| = |X|.$$
+
 </div>
 
 <details>
@@ -186,9 +184,9 @@ theorem separatesOrbits_of_injective {f : X → X} {α : X → ℝ}
 <span class="theorem-name">(windowDistinct_of_injective_of_le_minimalPeriod)</span>
 
 **Theorem.** If \(\alpha\) is injective and \(k \le p(x)\), where \(p(x)\) is the minimal period of \(x\) under \(f\), then the delay window at \(x\) is tie-free:
-\[
-\alpha \text{ injective},\; k \le \operatorname{minPeriod}_f(x) \;\Longrightarrow\; \operatorname{WindowDistinct}(f, \alpha, k, x).
-\]
+
+$$\alpha \text{ injective},\; k \le \operatorname{minPeriod}_f(x) \;\Longrightarrow\; \operatorname{WindowDistinct}(f, \alpha, k, x).$$
+
 This is the key precondition for ordinal pattern extraction.
 </div>
 

docs/exposition/ordinal-compression.md

@@ -6,9 +6,7 @@ Given an injective function \(f : \{0, \dots, d-1\} \to \mathbb{R}\), its ordina
 pattern is the unique permutation \(\sigma \in S_d\) such that
 \(f \circ \sigma\) is strictly increasing:
 
-\[
-f(\sigma(0)) < f(\sigma(1)) < \cdots < f(\sigma(d-1)).
-\]
+$$f(\sigma(0)) < f(\sigma(1)) < \cdots < f(\sigma(d-1)).$$
 
 This construction, due to Bandt and Pompe (2002), is the basis of permutation
 entropy and a wide family of complexity measures for time series. Composing
@@ -23,9 +21,9 @@ observation transforms and whose codomain has size at most \(d!\).
 <span class="theorem-name">(IsOrdinalPatternOf)</span>
 
 **Definition.** A permutation \(\sigma \in S_d\) is the *ordinal pattern of* \(f : \{0,\dots,d-1\} \to \mathbb{R}\) if \(f \circ \sigma\) is strictly monotone:
-\[
-\operatorname{IsOrdinalPatternOf}(\sigma, f) \;\iff\; f(\sigma(i)) < f(\sigma(j)) \text{ for all } i < j.
-\]
+
+$$\operatorname{IsOrdinalPatternOf}(\sigma, f) \;\iff\; f(\sigma(i)) < f(\sigma(j)) \text{ for all } i < j.$$
+
 </div>
 
 <details>
@@ -59,9 +57,9 @@ noncomputable def ordinalPattern (f : Fin d → ℝ) (hf : Injective f) :
 <span class="theorem-name">(ordinalPattern_exists_unique)</span>
 
 **Theorem.** For any injective \(f : \{0,\dots,d-1\} \to \mathbb{R}\), there exists a unique permutation \(\sigma \in S_d\) such that \(f \circ \sigma\) is strictly monotone:
-\[
-\exists!\, \sigma \in S_d, \quad \operatorname{IsOrdinalPatternOf}(\sigma, f).
-\]
+
+$$\exists!\, \sigma \in S_d, \quad \operatorname{IsOrdinalPatternOf}(\sigma, f).$$
+
 </div>
 
 <details>
@@ -82,9 +80,9 @@ input.
 <span class="theorem-name">(isOrdinalPatternOf_comp_strictMono)</span>
 
 **Theorem (Monotone invariance).** If \(\sigma\) is the ordinal pattern of \(f\) and \(g : \mathbb{R} \to \mathbb{R}\) is strictly monotone, then \(\sigma\) is also the ordinal pattern of \(g \circ f\):
-\[
-\operatorname{IsOrdinalPatternOf}(\sigma, f) \;\wedge\; g \text{ strictly monotone} \;\Longrightarrow\; \operatorname{IsOrdinalPatternOf}(\sigma, g \circ f).
-\]
+
+$$\operatorname{IsOrdinalPatternOf}(\sigma, f) \;\wedge\; g \text{ strictly monotone} \;\Longrightarrow\; \operatorname{IsOrdinalPatternOf}(\sigma, g \circ f).$$
+
 Ordinal patterns depend only on relative ordering, not on the scale or shape of the observation function.
 </div>
 
@@ -104,9 +102,9 @@ theorem isOrdinalPatternOf_comp_strictMono {σ : Equiv.Perm (Fin d)}
 <span class="theorem-name">(ordinalPattern_surjective)</span>
 
 **Theorem (Surjectivity).** Every permutation \(\sigma \in S_d\) is realizable as the ordinal pattern of some injective function:
-\[
-\forall\, \sigma \in S_d, \quad \exists\, f : \{0,\dots,d-1\} \hookrightarrow \mathbb{R}, \quad \pi(f) = \sigma.
-\]
+
+$$\forall\, \sigma \in S_d, \quad \exists\, f : \{0,\dots,d-1\} \hookrightarrow \mathbb{R}, \quad \pi(f) = \sigma.$$
+
 </div>
 
 <details>
@@ -131,9 +129,9 @@ injectivity of the input function.
 <span class="theorem-name">(ordinalDelayMap)</span>
 
 **Definition.** The *ordinal delay map* of window length \(k\) sends each state \(x\) (with tie-free window) to the ordinal pattern of its delay vector:
-\[
-\Pi_{f,\alpha,k} : \{x \in X \mid \operatorname{WindowDistinct}(f,\alpha,k,x)\} \;\to\; S_k, \qquad \Pi_{f,\alpha,k}(x) = \pi\bigl(\Phi_{f,\alpha,k}(x)\bigr).
-\]
+
+$$\Pi_{f,\alpha,k} : \{x \in X \mid \operatorname{WindowDistinct}(f,\alpha,k,x)\} \;\to\; S_k, \qquad \Pi_{f,\alpha,k}(x) = \pi\bigl(\Phi_{f,\alpha,k}(x)\bigr).$$
+
 </div>
 
 <details>
@@ -151,9 +149,9 @@ noncomputable def ordinalDelayMap (f : X → X) (α : X → ℝ) (k : ℕ)
 <span class="theorem-name">(ordinalDelayMap_monotone_invariant)</span>
 
 **Theorem (Monotone invariance of the ordinal delay map).** If \(g : \mathbb{R} \to \mathbb{R}\) is strictly monotone, then replacing \(\alpha\) by \(g \circ \alpha\) does not change the ordinal delay map:
-\[
-g \text{ strictly monotone} \;\Longrightarrow\; \Pi_{f,\, g \circ \alpha,\, k}(x) \;=\; \Pi_{f,\alpha,k}(x).
-\]
+
+$$g \text{ strictly monotone} \;\Longrightarrow\; \Pi_{f,\, g \circ \alpha,\, k}(x) \;=\; \Pi_{f,\alpha,k}(x).$$
+
 This is the formal justification for the robustness of permutation entropy to monotone signal transformations.
 </div>
 
@@ -201,9 +199,9 @@ upper bounds constrain the size of this set.
 <span class="theorem-name">(observedPatterns)</span>
 
 **Definition.** The *observed patterns* along an orbit of length \(N\) with window size \(d\):
-\[
-\operatorname{ObsPatterns}(f, \alpha, d, x, N) \;=\; \bigl\{\pi\bigl(\alpha(f^{t}(x)),\, \dots,\, \alpha(f^{t+d-1}(x))\bigr) : 0 \le t < N \bigr\} \;\subseteq\; S_d.
-\]
+
+$$\operatorname{ObsPatterns}(f, \alpha, d, x, N) \;=\; \bigl\{\pi\bigl(\alpha(f^{t}(x)),\, \dots,\, \alpha(f^{t+d-1}(x))\bigr) : 0 \le t < N \bigr\} \;\subseteq\; S_d.$$
+
 </div>
 
 <details>
@@ -257,9 +255,9 @@ theorem card_observedPatterns_le_length
 <span class="theorem-name">(card_observedPatterns_le_period)</span>
 
 **Theorem (Period bound).** On a periodic orbit, the number of distinct ordinal patterns is at most the minimal period:
-\[
-x \in \operatorname{PeriodicPts}(f) \;\Longrightarrow\; \bigl|\operatorname{ObsPatterns}(f, \alpha, d, x, N)\bigr| \;\le\; \operatorname{minPeriod}_f(x).
-\]
+
+$$x \in \operatorname{PeriodicPts}(f) \;\Longrightarrow\; \bigl|\operatorname{ObsPatterns}(f, \alpha, d, x, N)\bigr| \;\le\; \operatorname{minPeriod}_f(x).$$
+
 </div>
 
 <details>
@@ -285,9 +283,7 @@ ordinal dynamics:
 | \(\le p(x)\) | Periodicity | Low-period attractors |
 
 The *permutation entropy* of Bandt and Pompe (2002) is defined as
-\[
-H_d(f, \alpha, x) \;=\; -\sum_{\sigma \in S_d} p_\sigma \log p_\sigma,
-\]
+$$H_d(f, \alpha, x) \;=\; -\sum_{\sigma \in S_d} p_\sigma \log p_\sigma,$$
 where \(p_\sigma\) is the relative frequency of pattern \(\sigma\) along the orbit.
 The factorial bound gives the maximum entropy \(\log(d!)\); the period bound
 shows that periodic orbits have entropy at most \(\log(p(x))\), independent

docs/exposition/sard-infrastructure.md

@@ -18,9 +18,8 @@ This file builds the infrastructure for Sard's theorem in the setting of finite-
 
 **Definition.** The *critical set* of \(f : E \to F\) is
 
-\[
-\operatorname{Crit}(f) \;=\; \bigl\{\, x \in E \;\big|\; Df(x) : E \to F \text{ is not surjective}\,\bigr\}.
-\]
+$$\operatorname{Crit}(f) \;=\; \bigl\{\, x \in E \;\big|\; Df(x) : E \to F \text{ is not surjective}\,\bigr\}.$$
+
 </div>
 
 <details>
@@ -72,9 +71,8 @@ lemma det_fderiv_eq_zero_of_not_surjective (L : E →L[ℝ] E)
 
 **Theorem.** A continuous linear endomorphism \(L : E \to_L E\) on a finite-dimensional space is surjective iff \(\det L \ne 0\):
 
-\[
-L \text{ surjective} \;\iff\; \det L \ne 0.
-\]
+$$L \text{ surjective} \;\iff\; \det L \ne 0.$$
+
 </div>
 
 <details>

docs/exposition/smooth-embedding.md

@@ -2,9 +2,7 @@
 
 Route A of the formalization addresses the *smooth* side of Takens' delay embedding theorem (Takens, 1981): given a dynamical system \(T : X \to X\) and an observation function \(h : X \to \mathbb{R}\), the delay coordinate map
 
-\[
-\Phi_{T,h,n} : X \longrightarrow \mathbb{R}^n, \qquad x \longmapsto \bigl(h(x),\, h(Tx),\, \dots,\, h(T^{n-1}x)\bigr)
-\]
+$$\Phi_{T,h,n} : X \longrightarrow \mathbb{R}^n, \qquad x \longmapsto \bigl(h(x),\, h(Tx),\, \dots,\, h(T^{n-1}x)\bigr)$$
 
 is a topological embedding under appropriate hypotheses. This page documents the **embedding chain**: the sequence of results that, starting from the bare definition, establishes continuity, then promotes injectivity on a compact space to a closed embedding, and finally constructs a homeomorphism onto the image.
 
@@ -18,9 +16,8 @@ The most notable structural feature of this file is that **it is entirely axiom-
 
 **Definition.** Let \(X\) be a topological space, \(T : X \to X\) a self-map, \(h : X \to \mathbb{R}\) an observation function, and \(n \in \mathbb{N}\). The *smooth delay map* is
 
-\[
-\operatorname{smoothDelayMap}(T, h, n)(x) \;=\; \bigl(i \mapsto h(T^i(x))\bigr) \;\in\; \mathbb{R}^n.
-\]
+$$\operatorname{smoothDelayMap}(T, h, n)(x) \;=\; \bigl(i \mapsto h(T^i(x))\bigr) \;\in\; \mathbb{R}^n.$$
+
 </div>
 
 <details>
@@ -106,9 +103,8 @@ theorem smoothDelayMap_isEmbedding [CompactSpace X]
 
 **Definition.** Under the same hypotheses, the range factorization of the smooth delay map is a homeomorphism
 
-\[
-X \;\cong_{\mathrm{top}}\; \operatorname{range}\bigl(\operatorname{smoothDelayMap}(T, h, n)\bigr).
-\]
+$$X \;\cong_{\mathrm{top}}\; \operatorname{range}\bigl(\operatorname{smoothDelayMap}(T, h, n)\bigr).$$
+
 </div>
 
 This is the terminal result of the embedding chain. The construction uses `Equiv.ofInjective` to build a bijection onto the range, then lifts it to a homeomorphism via the inducing property of the closed embedding. The result is a concrete `Homeomorph` (`\cong_\top`), not merely an abstract existence statement.

docs/reference/axiom-dashboard.md

@@ -13,9 +13,7 @@ nontrivial Lean proof uses.
 
 ### `propext` -- Propositional extensionality
 
-$$
-(P \leftrightarrow Q) \;\Longrightarrow\; P = Q
-$$
+$$(P \leftrightarrow Q) \;\Longrightarrow\; P = Q$$
 
 Two propositions that are logically equivalent are equal as terms.
 This is the principle that lets Lean treat "if and only if" as