Rabdos Lean Bench

The statement is interpreted for a split connected reductive algebraic group G over a field k, with a split maximal torus T of G and a chosen positive-root system for (G,T).

The admissibility condition on $\lambda$ is precisely that it is a dominant character of T, $\lambda\in X(T)_+$, with dominance computed from the chosen positive roots.

For every dominant $\lambda$, the exact module whose character occurs in the formula is the contextually defined canonical module $L(\lambda)=\operatorname{soc}_G H^0(\lambda)$, or a module definitionally equal, isomorphic, or otherwise proved equivalent to that object in a way that preserves its T-weight spaces. A canonical socle construction, including the supremum or sum of the simple algebraic G-subrepresentations of $H^0(\lambda)$, suffices by itself; it need not be accompanied by a separate theorem certifying that the resulting object is nonzero, G-stable, and simple. An unrelated module selected merely because it has the desired character does not satisfy this requirement.

The formal character $\operatorname{ch} M$ is the finitely supported element of $\mathbf Z[X(T)]$ whose coefficient at each weight $\mu$ is $\dim_k M_\mu$, with the natural-number dimension embedded in $\mathbf Z$.

The relation $\mu<\lambda$ is the strict weight order fixed by the chosen positive roots: $\lambda-\mu$ is a nonnegative integral combination of the positive simple roots and $\mu\ne\lambda$. It is fixed independently of $L(\lambda)$, its support, and the desired equality.

The displayed character equality remains the conclusion to be proved from independent representation-theoretic facts, such as finite weight support, highest-weight multiplicity one, and the upper weight bound, or from mathematically equivalent prior results; the equality itself is not installed as a hypothesis, hidden in a definition, or used circularly.

For a fixed scalar field $\mathbb{K}$ used consistently by the distribution theory, the statement must range over every $\mathbb{K}$-valued scalar distribution $u$ on $\mathbb{R}^n$. The choice $\mathbb{K}=\mathbb{R}$ is valid, as is another standard scalar field when all pairings and norms are interpreted compatibly; no substantive assumptions such as compact support, prior continuity, local integrability of $u$ as a function, membership of $u$ itself in $L^p$, smoothness, or a pre-existing function representative may be added.

The Lebesgue exponent $p$ must be a real parameter subject to the strict supercritical hypothesis $(n:\mathbb{R})<p$, with no stronger substantive restriction substituted for it.

For every coordinate $j$, the standard distributional derivative $\partial_j u$ must be represented by a global function $g_j\in L^p(\mathbb{R}^n;\mathbb{K})$. Equivalently, for every compatible compactly supported smooth test function $\varphi$, the encoding must express $u(\partial_j\varphi)=-\int_{\mathbb{R}^n}g_j\varphi$ using its standard scalar-field pairing convention, and this must hold for all $n$ coordinates.

The conclusion must produce a globally continuous function $f:\mathbb{R}^n\to\mathbb{K}$, with exactly the same scalar field $\mathbb{K}$ as $u$, whose induced regular distribution is exactly $u$. Thus every compatible compactly supported smooth test function must satisfy the standard regular-distribution pairing identity $u(\varphi)=\int_{\mathbb{R}^n}f(x)\varphi(x)\,dx$, interpreted with the encoding's standard scalar-field convention. This same function $f$ must be the representative used in the quantitative estimate.

For every pair of distinct points $x,y\in\mathbb{R}^n$, the continuous representative must satisfy the global upper bound $\frac{|f(x)-f(y)|}{\lVert x-y\rVert^{\,1-(n:\mathbb{R})/p}}\le C\,M.$ An equivalent denominator-cleared or supremum formulation is acceptable, but a local estimate, a reversed or strict inequality, mere continuity, mere finiteness, or a smaller Hölder exponent is not.

The constant $C$ must be chosen uniformly before $u$, its derivative representatives, the continuous representative $f$, and the points $x,y$; it may depend only on the fixed parameters $n$ and $p$.

The ambient objects are finite simple undirected graphs, with no loops, and every vertex degree is at most the same fixed bound D; label choices, quotients by isomorphism, and equivalent graph representations are allowed.

Distinguishability by sampling requires the existence of one shared positive finite radius r, one shared positive finite sample count k, and one decision property Q on ordered k-tuples of radius-r rooted observations.

For the same witnesses r, k, and Q, every graph in $\mathcal P_1$ has Q-acceptance probability at least $2/3$, while every graph in $\mathcal P_2$ has Q-acceptance probability at most $1/3$, under k independent uniformly sampled vertices.

The inter-property distance is $\delta_{\mathcal G}(\mathcal P_1,\mathcal P_2)=\inf\{\delta_{\square}(G_1,G_2):G_1\in\mathcal P_1,\ G_2\in\mathcal P_2\}$ over all cross-pairs. It is interpreted in an extended nonnegative codomain with $\inf\varnothing=\infty$, or by an equivalent explicit convention, so the value is infinite when either property is empty.

The top-level proposition joins sampling distinguishability and sampling-distance separation by a biconditional, so it contains both the forward and reverse implications.

Sampling distinguishability and inter-property distance are defined independently of one another, and no custom wrapper, hypothesis, or structure encodes the desired biconditional or strict-positivity conclusion by construction.