Answer: —
Proposition 1 — class: algorithmic
PDF text-layer excerpt — equations and symbol order may be approximateDetermining whether a formula in the language of L[N, X] is valid is a decidable problem.
statement extracted from the paper’s text layer; consult the paper for the exact wording
Given a finite candidate set \(X\), a listed set of ranking types \(S\subseteq L(X)\), and a formula \(\varphi\) with outcome atoms, rational mass-threshold atoms, Boolean connectives, and modalities \(\Diamond_\alpha\), determine whether \(\varphi\) holds for every distribution \(\mu\in\Delta(S)\) and every resolute rule \(F:\Delta(S)\to X\). At \((F,\mu)\), \(\mathsf{Mass}_{t\ge q}\) is true exactly when \(\mu_t\ge q\), and \(\Diamond_\alpha\psi\) holds when some transfer \(\mu'=\mu-\nu+\nu'\), with \(0\le\nu\le\mu\) and \(\sum_t\nu_t=\sum_t\nu'_t=\alpha\), makes \(\psi\) true at \((F,\mu')\).
Input: a nonempty finite candidate set \(X\), with \(m=|X|\), a nonempty explicitly listed set \(S\) of strict ranking types on \(X\), with \(k=|S|\), and a finite formula \(\varphi\).
A society is represented by its support: the list of its \(\tau\) positive-mass types, each with its mass as a binary rational; \(\tau\) is the actual support size, not the number of possible rankings. Here the validity input specifies \(S\), rather than an individual society.
Semantic worlds are all real distributions \(\Delta(S)=\{\mu\in\mathbb R_{\ge0}^{S}:\sum_{t\in S}\mu_t=1\}\), including boundary distributions; explicitly represented rational societies follow the support convention above.
A rule is any total resolute function \(F:\Delta(S)\to X\), with no continuity, measurability, or computability restriction. At \((F,\mu)\), outcome atom \(x\) holds exactly when \(F(\mu)=x\).
Formulas use outcome atoms, atoms \(\mathsf{Mass}_{t\ge q}\) for \(t\in S\) and binary rational \(q\in[0,1]\), Boolean connectives, and arbitrarily nested modalities \(\Diamond_\alpha\) with binary rational \(\alpha\in[0,1]\). The mass atom holds exactly when \(\mu_t\ge q\).
The formula \(\Diamond_\alpha\psi\) holds at \((F,\mu)\) exactly when there exist \(\nu,\nu'\in\mathbb R_{\ge0}^{S}\) with \(\nu\le\mu\) coordinatewise and \(\sum_t\nu_t=\sum_t\nu'_t=\alpha\), such that \(\psi\) holds at \((F,\mu-\nu+\nu')\). Removed mass may be reassigned to its original type; the same \(F\) is used throughout.
Validity means truth for every \(\mu\in\Delta(S)\) and every such \(F\). Let \(L\) be the total binary input length; state running times in \(m,k,L,|\varphi|\), and \(\tau\) whenever an explicitly represented society is involved.
Is this continuous validity problem decidable, or is it undecidable?
Discrete validity with fixed finite agents and candidates, preference and outcome atoms, and modalities allowing a specified coalition to change its ballots is decidable by exhaustive enumeration. [Cinà–Endriss](https://pure.uva.nl/ws/files/42894993/p1009_cina.pdf)
The richer discrete logic including truthful-preference operators is also decidable. [Troquard–van der Hoek–Wooldridge](https://arxiv.org/abs/1102.3341) No result settling exactly the continuous validity problem above was located.
I do not settle the problem for arbitrary $k$. I prove a new special case covering the full language:
Theorem. If $k\le 2$, continuous validity is decidable, with arbitrary outcome atoms, arbitrary Boolean connectives, arbitrary modal nesting, and arbitrary rational radii.
The proof includes boundary distributions and arbitrary total resolute rules. I also construct a satisfiable formula, already with $k=2$, that has no semialgebraic realizing rule. Thus restricting outcome sets to semialgebraic sets is not a sound general reduction.
The remaining question is the full problem with $k\ge 3$.
Write $D=\Delta(S)$. For $\mu,\eta\in D$, define
$$
d_{\mathrm{TV}}(\mu,\eta)
=\frac12\sum_{t\in S}|\mu_t-\eta_t|
=\sum_{t\in S}(\mu_t-\eta_t)_+.
$$
The second equality follows from $\sum_t(\mu_t-\eta_t)=0$.
Lemma 1. The distribution $\eta$ is accessible from $\mu$ through $\Diamond_\alpha$ if and only if
$$
d_{\mathrm{TV}}(\mu,\eta)\le\alpha.
$$
Proof. If $\eta=\mu-\nu+\nu'$, then
$$
(\mu_t-\eta_t)_+=(\nu_t-\nu'_t)_+\le\nu_t.
$$
Summation gives the required inequality.
Conversely, put $d=d_{\mathrm{TV}}(\mu,\eta)\le\alpha$ and define
$$
r_t=(\mu_t-\eta_t)_+,\qquad
s_t=(\eta_t-\mu_t)_+,\qquad
h_t=\min\{\mu_t,\eta_t\}.
$$
Then
$$
\sum_t r_t=\sum_t s_t=d,\qquad
\sum_t h_t=1-d,\qquad
\mu-r+s=\eta.
$$
If $d<1$, let
$$
a_t=\frac{\alpha-d}{1-d}h_t,\qquad
\nu=r+a,\qquad
\nu'=s+a.
$$
Because $0\le\alpha-d\le1-d$, we have $0\le a\le h$. Hence
$$
0\le\nu\le r+h=\mu,\qquad
\sum_t\nu_t=\sum_t\nu'_t=\alpha,
$$
and $\mu-\nu+\nu'=\eta$.
If $d=1$, then $\alpha=1$, and $\nu=r,\nu'=s$ suffice. $\square$
Consequently, $\Diamond_0$ is the identity modality. We may eliminate every occurrence of it before proceeding.
If $k=1$, there is only one world. Every mass atom is true and every modality is the identity. Checking the resulting Boolean formula for each of the $m$ possible outcomes takes
$$
O(L+m|\varphi|)
$$
time.
Now suppose $S=\{t_1,t_2\}$. Identify a distribution with its first coordinate:
$$
p\longleftrightarrow(p,1-p),\qquad 0\le p\le1.
$$
Then
$$
d_{\mathrm{TV}}\bigl((p,1-p),(q,1-q)\bigr)=|p-q|.
$$
Thus the accessible worlds from $p$ are precisely
$$
B_\alpha(p)=[0,1]\cap[p-\alpha,p+\alpha].
$$
Mass atoms become rational linear inequalities:
$$
\mathsf{Mass}_{t_1\ge q}\iff p\ge q,\qquad
\mathsf{Mass}_{t_2\ge q}\iff p\le1-q.
$$
For an arbitrary set $A\subseteq[0,1]$, define
$$
N_\alpha(A)=\{p\in[0,1]:B_\alpha(p)\cap A\ne\varnothing\}.
$$
Lemma 2. If $0<\alpha\le1$, then $N_\alpha(A)$ is a union of at most
$$
\left\lfloor\frac1\alpha\right\rfloor
$$
intervals. Each interval may independently include or exclude either endpoint.
Proof. By symmetry of the distance,
$$
N_\alpha(A)
=\bigcup_{a\in A}
[\max\{0,a-\alpha\},\min\{1,a+\alpha\}].
$$
Every interval in this union has length at least $\alpha$.
Every connected component of the union contains one of these intervals: choose any point in the component and a generating interval containing that point. The generating interval is connected, so it lies in the same component.
Connected subsets of the real line are intervals. Distinct components therefore contain disjoint generating intervals of length at least $\alpha$. If there were $r$ distinct components, choosing one generating interval from each would give
$$
r\alpha\le1.
$$
This also rules out infinitely many components. Each component is a bounded interval, with whichever endpoint inclusion properties its union has. $\square$
This applies without any regularity assumption on $A$. In particular, under an arbitrary rule, the truth set of every positive-radius diamond is a finite union of intervals.
A second elementary observation will control where outcomes can safely be changed.
Lemma 3. Suppose $T\subseteq[0,1]$ is a finite union of intervals. Define
$$
H_\alpha(T)=\{y\in[0,1]:B_\alpha(y)\subseteq T\}.
$$
Every boundary point of $H_\alpha(T)$ belongs to the finite list consisting of $0,1$ and the numbers
$$
e-\alpha,\qquad e+\alpha,
$$
where $e$ ranges over the endpoints of $T$ and over $0,1$.
Proof. We have
$$
H_\alpha(T)
=[0,1]\setminus N_\alpha([0,1]\setminus T).
$$
The complement of $T$ is a finite union of intervals and singleton points whose endpoints come from the endpoints of $T$ and $0,1$.
For a nonempty interval with endpoints $a,b$, its $\alpha$-neighborhood is an interval whose possible boundary points are
$$
\max\{0,a-\alpha\},\qquad
\min\{1,b+\alpha\}.
$$
This follows directly by taking the union of the balls centered in that interval. Endpoint inclusion depends on attainment and clipping, but creates no additional boundary location. A singleton $e$ gives the closed interval $B_\alpha(e)$.
Taking finite unions and then complements creates no boundary points outside the displayed finite list. $\square$
Let $\theta$ be any formula after eliminating zero-radius modalities. Enumerate its modal occurrences as
$$
D_j=\Diamond_{\alpha_j}\psi_j,\qquad 1\le j\le s,
$$
where every $\alpha_j>0$.
Suppose an arbitrary rule $F$ satisfies $\theta$ at $u\in[0,1]$. Let
$$
T_j=\{p\in[0,1]:(F,p)\models D_j\}.
$$
By Lemma 2, each $T_j$ is a finite union of intervals.
Construct a finite set $E\subseteq[0,1]$ containing:
Sort its distinct elements:
$$
0=e_0<e_1<\cdots<e_h=1.
$$
The resulting cells are the singleton points $\{e_i\}$ and the open intervals
$$
I_i=(e_i,e_{i+1}).
$$
For a candidate $c$, define $\Psi_j^c(y)$ as follows. In $\psi_j$, replace outcome atoms according to outcome $c$, and replace each maximal modal subformula $D_\ell$ by the condition $y\in T_\ell$. This is a quantifier-free numerical formula.
Under the original rule,
$$
(F,y)\models\psi_j
\quad\Longleftrightarrow\quad
\Psi_j^{F(y)}(y).
$$
For fixed $j,c$, the truth value of $\Psi_j^c$ is constant on each open cell: all mass-atom and modal-set boundaries belong to $E$. By Lemma 3, membership in $H_{\alpha_j}(T_j)$ is also constant on each open cell.
For each open cell, let
$$
C_i=\{F(y):y\in I_i\}.
$$
This is a nonempty subset of $X$.
Lemma 4. There is a rule $G$ such that:
Consequently, $(G,u)\models\theta$.
Proof. First construct a coloring satisfying conditions 1–4. An open interval can be partitioned into finitely many sets, each dense in it: enumerate its rational subintervals and, for every required color and every such subinterval, select a fresh rational point. Assign the selected points their colors and assign the remaining points any permitted color. If necessary, change the outcome at $u$ to $F(u)$. Changing one point preserves density.
We prove condition 5 by induction on modal depth. Assume the proper modal descendants of $D_j$ already have their original truth sets. Its operand under $G$ is then evaluated by $\Psi_j^{G(y)}(y)$.
First, suppose $p\in T_j$. There is an original witness $y\in B_{\alpha_j}(p)$ with
$$
(F,y)\models\psi_j.
$$
If $y$ is a singleton cell, its outcome is unchanged, so it remains a witness.
Otherwise, $y\in I_i$ and $c=F(y)\in C_i$. The formula $\Psi_j^c$ is true throughout $I_i$. Moreover,
$$
B_{\alpha_j}(p)\cap I_i
$$
contains a nonempty open subinterval. Indeed, if the witness lies exactly at a ball endpoint, moving it slightly toward $p$ stays inside both the ball and $I_i$, because $\alpha_j>0$. Density supplies a point in this intersection colored $c$ by $G$. That point is a new witness.
Conversely, suppose $G$ supplies a witness $y$ for $D_j$ at $p$. A singleton witness is also an original witness.
If $y\in I_i$ and $G(y)=c$, then $c\in C_i$. Choose $z\in I_i$ with $F(z)=c$. Constancy of $\Psi_j^c$ gives
$$
(F,z)\models\psi_j.
$$
By symmetry of accessibility, every center within distance $\alpha_j$ of $z$ has this witness. Hence
$$
B_{\alpha_j}(z)\subseteq T_j,
$$
so $z\in H_{\alpha_j}(T_j)$. Membership in this set is constant on $I_i$, giving $y\in H_{\alpha_j}(T_j)$. Because $p\in B_{\alpha_j}(y)$, we obtain $p\in T_j$.
Thus the truth set of $D_j$ is exactly $T_j$. The induction proves condition 5. The preserved root outcome, mass atoms, and modal truth values establish $\theta$ at $u$. $\square$
The constructed rule can be chosen Borel: on each open cell, all but one of the outcome classes can be countable dense sets, with the remaining class their complement. No Borel restriction is assumed in the semantics; this is a consequence specific to this construction.
We now give an effective satisfiability procedure. Applying it to $\theta=\neg\varphi$ decides validity.
For each modal occurrence, define
$$
B_j=\left\lfloor\frac1{\alpha_j}\right\rfloor.
$$
Make the following finite guesses:
The interval endpoints themselves are real variables. Every fixed guess describes membership in $T_j$ by a Boolean combination of rational linear inequalities.
Form $\Psi_j^c$ using these guessed modal sets, exactly as above. Define $\Theta^c$ similarly from the entire formula $\theta$.
For each $j$, impose the following equation for every $x\in[0,1]$:
$$
T_j(x)\ \longleftrightarrow\
\left(
\bigvee_i
\left(
|x-e_i|\le\alpha_j
\land \Psi_j^{d_i}(e_i)
\right)
\right)
\lor
\left(
\bigvee_i\ \bigvee_{c\in C_i}
\exists y\,
\left(
e_i<y<e_{i+1}
\land |x-y|\le\alpha_j
\land \Psi_j^c(y)
\right)
\right).
$$
Absolute-value inequalities here abbreviate two linear inequalities.
Finally, require a root $u\in[0,1]$ such that $\Theta^{c_0}(u)$ holds and its prescribed outcome is available:
$$
\left(
\bigvee_{\{i:d_i=c_0\}}u=e_i
\right)
\lor
\left(
\bigvee_{\{i:c_0\in C_i\}}e_i<u<e_{i+1}
\right).
$$
Existentially quantify all interval endpoints and $u$, and include the linear constraints describing the guessed intervals and endpoint ordering.
The result is a first-order sentence of rational linear real arithmetic.
If $\theta$ is satisfiable, take its actual sets $T_j$ and apply Lemma 4. Their interval counts meet the bounds $B_j$. Guess the resulting partition, singleton outcomes, available color sets, and root outcome.
Under the canonical rule, an open cell contributes a witness exactly when the corresponding existential numerical condition holds. Constancy of $\Psi_j^c$ and density of color $c$ justify this assertion, including witnesses at distance exactly $\alpha_j$. Therefore every imposed modal equation and the root requirement hold.
Suppose one of the numerical sentences holds. On every open cell, assign every color in $C_i$ densely, and assign $d_i$ at its singleton endpoints. Give the root outcome $c_0$; this preserves density.
For fixed $j,c$, $\Psi_j^c$ is constant on every open cell. Whenever its numerical existential condition holds, the ball intersects that cell in a nonempty open subinterval, so density supplies an actual witness of color $c$. Conversely, any actual witness in that cell satisfies the numerical existential condition. The singleton terms are exact as well.
Induction on modal depth now proves that every $D_j$ has precisely its guessed truth set $T_j$. The root requirement then proves $\theta$.
Thus the finite procedure is sound and complete.
Here is a deliberately loose bound with a self-contained elimination argument.
Put $n=|\varphi|$. Positive binary rational radii satisfy
$$
\frac1{\alpha_j}\le 2^{O(L)}.
$$
Hence the total number of guessed interval endpoints and partition cells is at most
$$
O(n2^{O(L)}).
$$
After expanding the finite disjunctions, the numerical sentence has binary length at most
$$
N=2^{p(m+k+L+n)}
$$
for a fixed polynomial $p$, with $k=2$. The number of finite guesses is at most $2^{N^{O(1)}}$: endpoint orderings, endpoint flags, singleton outcomes, and cell color subsets all fit this bound.
For completeness, rational linear real arithmetic admits the following direct elimination procedure. Put a quantifier-free formula into disjunctive normal form. To eliminate an existentially quantified variable from a conjunction, express each inequality involving it as a lower or upper bound. Every lower bound must be compatible with every upper bound. The resulting comparison is strict precisely when at least one of those two bounds is strict. Constraints not involving the variable are retained. Equalities can be represented by two weak inequalities. Universal quantifiers are eliminated using
$$
\forall v\,\chi\iff\neg\exists v\,\neg\chi.
$$
All resulting coefficients remain rational. This proves effective elimination without quantification over outcome sets.
Define
$$
T_0(z)=z,\qquad T_{h+1}(z)=2^{T_h(z)}.
$$
If the current formula has binary length $H$, one elimination step, including Boolean expansion and rational arithmetic, can conservatively be bounded by $2^{H^{O(1)}}$. There are at most $O(N)$ quantified variables after renaming and prenex conversion. Consequently, for a fixed constant $C$, the entire decision procedure has a bound of the form
$$
T_{\lceil CN\rceil}(N^C),
\qquad
N=2^{p(m+k+L+n)}.
$$
This is an explicit computable upper bound, not a tight classification.
Validity itself has no individual-society input. If instead one asks for truth at a supplied rational society universally over rules, the same procedure fixes $u$ to its first mass coordinate. If that society has encoding length $\ell$ and actual support size $\tau\le2$, use $L+\ell$ in the bound; reading and converting its support representation takes polynomial time in $m,k,\tau,\ell$.
More generally, Lemma 1 lets one check accessibility between two explicitly represented rational societies in polynomial time in $m,k$, their actual support sizes, and their binary encoding lengths: only coordinates in the union of their supports contribute to the distance.
The preceding procedure uses dense colorings. The following example shows that replacing arbitrary rules by semialgebraic rules would lose satisfiable formulas.
Take three candidates $a,b,c$ and two ranking types. Write $p=\mu_{t_1}$ and set
$$
\varepsilon=\frac14.
$$
The numerical conditions below are expressible by the allowed atoms:
$$
p>\varepsilon
\iff
\neg\mathsf{Mass}_{t_2\ge3/4},
$$
and
$$
0<p<\varepsilon
\iff
\neg\mathsf{Mass}_{t_2\ge1}
\land
\neg\mathsf{Mass}_{t_1\ge1/4}.
$$
Let $\Box_1\chi$ abbreviate $\neg\Diamond_1\neg\chi$. Consider
$$
\Gamma=
\Box_1
\left(
\bigl((a\lor b)\rightarrow p>\varepsilon\bigr)
\land
\bigl(
(0<p<\varepsilon)
\rightarrow
(\Diamond_\varepsilon a\land\Diamond_\varepsilon b)
\bigr)
\right).
$$
Proposition. The formula $\Gamma$ is satisfiable, but no rule satisfying it has both outcome sets for $a$ and $b$ semialgebraic.
Proof. Partition $(\varepsilon,1]$ into two dense sets, assign them outcomes $a,b$, and assign $c$ on $[0,\varepsilon]$. For every $p\in(0,\varepsilon)$,
$$
B_\varepsilon(p)\cap(\varepsilon,1]
=(\varepsilon,\varepsilon+p].
$$
This contains a nonempty open interval, so it contains both outcomes. The first conjunct also holds. Since $\Diamond_1$ is global, this proves $\Gamma$.
Conversely, suppose a rule satisfies $\Gamma$. Its $a$- and $b$-outcome sets are disjoint and lie strictly above $\varepsilon$. For every $p\in(0,\varepsilon)$, each set has a point in
$$
(\varepsilon,\varepsilon+p].
$$
Thus both sets accumulate at $\varepsilon$ from the right.
A semialgebraic subset of the real line is a finite union of intervals and points. Indeed, in a finite polynomial description, the finitely many roots of its nonzero polynomials partition the line into intervals on which every polynomial sign, and hence membership, is constant.
A semialgebraic set lying above $\varepsilon$ and accumulating there must therefore contain $(\varepsilon,\varepsilon+\delta)$ for some $\delta>0$. If both outcome sets were semialgebraic, they would overlap on such an interval, contradicting resoluteness. $\square$
This obstruction already occurs in the decidable case $k=2$.
The proof settles the full language for $k\le2$. Its essential additional fact is one-dimensional: every positive-radius diamond has a uniformly bounded finite interval presentation. That permits a finite partition on which dense recoloring preserves all modal truth sets.
No corresponding representation has been established here for higher-dimensional simplices. Accordingly, this argument proves neither decidability nor undecidability of the full input problem.
⟨structured verdict parsed — rendered above⟩
The output establishes decidability for $k\le 2$. The interval bounds, preservation of modal truth under dense recoloring, and reduction to rational linear real arithmetic are sound. The semialgebraic counterexample is also correct.
It does not resolve the assigned problem, whose inputs allow arbitrary $k$. The prover explicitly acknowledges this limitation. The appropriate assessment is partial, with a major scope limitation but no identified mathematical error in the special-case proof.
Lemma 1 is correct for all permitted $k$ and $\alpha$.
The necessary inequality follows coordinatewise from
$$
(\mu_t-\eta_t)_+=(\nu_t-\nu'_t)_+\le \nu_t.
$$
Summing uses exactly the required condition $\sum_t\nu_t=\alpha$.
For sufficiency, the stated identities for $r,s,h$ are correct. In particular, $r+h=\mu$ coordinatewise. When $d<1$, the assumptions $d\le\alpha\le1$ ensure
$$
0\le\frac{\alpha-d}{1-d}\le1.
$$
Consequently, the proposed removal vector satisfies $\nu\le\mu$, both vectors have total mass $\alpha$, and the resulting distribution is $\eta$. The separate case $d=1$ correctly forces $\alpha=1$ and avoids division by zero.
This checks the boundary cases $\alpha=0$, $\alpha=1$, and distributions with zero coordinates. Allowing reassignment to the original type is essential to the common padding vector $a$, and is explicitly permitted by the task.
The subsequent reductions are correct:
The stated $k=1$ running time is consistent with reading the input and evaluating the formula for each possible outcome.
Lemma 2 is correct, including its bound.
Each generating interval has length at least $\alpha$, since its center belongs to $[0,1]$ and $0<\alpha\le1$. Every connected component contains a generating interval: a point of the component belongs to one such interval, and that connected interval must lie within the same component.
Generating intervals chosen from distinct components are disjoint. Their total length therefore gives the claimed inequality
$$
r\alpha\le1.
$$
The argument also excludes infinitely many components: an infinite collection would contain a finite collection exceeding the bound. Connected subsets of the real line are intervals, so the resulting finite interval presentation follows.
The proof does not assume that $A$ is measurable, closed, or otherwise regular. Open endpoints of components are compatible with taking an arbitrary union of closed generating intervals.
Lemma 3 is also correct.
The identity
$$
H_\alpha(T)=[0,1]\setminus N_\alpha([0,1]\setminus T)
$$
uses precisely the closed-ball definition. For a finite union of intervals, the complement has a finite interval-and-point presentation using the stated endpoints. Neighborhood boundaries occur only at shifted endpoints or at clipping locations $0,1$. Endpoint inclusion changes membership at a boundary, but introduces no new boundary location.
Thus the proposed partition contains all boundaries needed for both modal-set membership and membership in the relevant sets $H_{\alpha_j}(T_j)$.
Lemma 4 is sound.
The numerical replacement $\Psi_j^c$ correctly accounts for outcome atoms, mass atoms, and maximal modal subformulas. Under the original rule, the asserted equivalence with $\Psi_j^{F(y)}(y)$ follows from the definitions.
For fixed $j,c$, all boundaries affecting $\Psi_j^c$ belong to $E$. Its truth value is therefore constant on each open cell. Lemma 3 supplies the corresponding constancy for $H_{\alpha_j}(T_j)$.
The coloring construction is valid. Each open cell has a nonempty finite set of permitted outcomes. Selecting distinct rational points in every rational subinterval produces a dense set for each permitted outcome. Altering the outcome at one point preserves density and permits preservation of the root outcome.
Both directions of the modal preservation argument check out:
Induction on modal depth is well founded and uses only proper modal descendants. Preservation of the root outcome, mass atoms, and modal truth values establishes the final assertion about $\theta$.
The Borel observation is justified by the described countable dense color classes, their complements within finitely many cells, and finitely many point modifications.
The finite guessing procedure and its soundness and completeness arguments are correct.
The interval count bounds make the number of endpoint variables and discrete guesses finite. Endpoint inclusions, weak orderings, singleton outcomes, and nonempty cell color sets account for the relevant choices.
Once a weak ordering is fixed, the cells and their endpoints can be described by rational linear constraints. Membership in each guessed modal set, the formulas $\Psi_j^c$, and the root formula $\Theta^c$ are Boolean combinations of linear comparisons.
The modal equations correctly distinguish singleton witnesses from witnesses in open cells. Their use of an existential numerical witness in an open cell is justified by the same positive-radius intersection argument used in Lemma 4. It remains valid at distance exactly $\alpha_j$.
The root availability constraint correctly handles both possibilities:
The necessity argument obtains a satisfying numerical sentence from an actual model and the canonical coloring. The sufficiency argument constructs an actual rule and verifies the guessed truth sets by modal-depth induction. There is no circular reliance on the guessed sets already being actual truth sets.
Consequently, applying the procedure to $\neg\varphi$ decides validity for $k=2$, including arbitrary rules and boundary worlds.
The deliberately loose computable upper bound is supported.
A positive binary rational radius has reciprocal bounded by $2^{O(L)}$. Hence the interval and partition sizes can be exponentially bounded in the stated parameters. The expanded arithmetic sentences and the finite guesses fit the generous bounds supplied.
The elimination argument is valid for linear real arithmetic. Compatibility of each lower bound with each upper bound is the correct projection condition, with strictness required whenever either bound is strict. Equalities can be expressed using weak inequalities, and universal quantifiers can be handled through negation and existential elimination. Rational coefficients remain rational.
An exponential bound in a polynomial of the current formula length per elimination step supports a tower bound with height proportional to the number of quantified variables, after increasing the fixed constants as allowed in the statement. Enumerating the finite guesses is also absorbed by that bound.
This establishes a computable upper bound for the special case; it does not establish polynomial-time solvability.
The supplied-society discussion correctly fixes the first coordinate and accounts for a support of size $\tau\le2$. The accessibility claim for rational societies follows from Lemma 1: coordinates outside the union of the supports contribute zero, and the remaining rational arithmetic has polynomial bit complexity.
The proposition is correct.
The mass-atom expressions accurately encode both strict numerical conditions. By Lemma 1, $\Box_1$ quantifies over the entire simplex.
In the proposed model, outcomes $a,b$ occur only above $\varepsilon$. For every $p\in(0,\varepsilon)$, the accessible portion above $\varepsilon$ is exactly
$$
(\varepsilon,\varepsilon+p],
$$
which contains a nonempty open interval. Density supplies both required outcomes.
Conversely, any satisfying rule must place both outcome sets strictly above $\varepsilon$, and each must meet every interval of the displayed form. Thus both accumulate at $\varepsilon$ from the right.
The finite polynomial-sign argument correctly establishes the needed one-dimensional structure of semialgebraic sets. A semialgebraic set lying strictly above $\varepsilon$ and accumulating there must contain an interval immediately to its right. Applying this to both outcome sets would force an overlap, contradicting resoluteness.
This proves that restricting all outcome sets to semialgebraic sets would lose satisfiable instances. It does not imply undecidability.
Major — the general input problem remains unresolved.
The task asks for decidability or undecidability when $k$ is unrestricted. The decision procedure depends on the one-dimensional finite interval presentation and is established only for $k\le2$. The accessibility characterization for arbitrary $k$ does not provide a decision procedure in higher dimensions.
This is an acknowledged limitation, not a false claim of completeness. No clarification alone can close it. A further submission must supply and verify an argument resolving unrestricted $k$; the current special-case result and semialgebraic obstruction do not determine that answer.
No minor mathematical issues requiring repair were identified.
⟨structured verdict parsed — rendered above⟩
Tier: machine-proved, adversarially reviewed by an independent model. No human has checked this proof. Generated from pipeline artifacts by tools/atlas_build.py.