An illustrative urban-air-mobility corridor instance, built from the published structure of the Rio de Janeiro Concept of Operations and solved in exact rational arithmetic. Scenario one is mathematically certified unique, residuals identically zero, with the uniqueness condition’s margin stated as an exact integer. Scenario two is the finding: two fleet operators on the document’s two approved corridors, where equilibrium pins each corridor’s total traffic exactly — and leaves who flies which corridor as a one-dimensional face of equally valid equilibria, exhibited and verified, with the point-uniqueness certificate honestly REFUSED. One word of scope before anything else: in aviation, “certified” is the regulator’s word. Everything certified on this page is mathematics, and it carries no airworthiness, separation-assurance or operational-approval meaning.
The source is the Eve-led Concept of Operations for Sustainable Urban Air Mobility in
Rio de Janeiro (April 2022), produced with eleven partners including Brazil’s
civil-aviation authority ANAC and airspace-control department DECEA. The copy this page
works from is pinned: sha256
0d38f35ae667e4f613de54df1789c1012896c0a812b4ced2cb8670aa5a8b536b, 82 pages,
retrieved via the Internet Archive’s snapshot of the publisher’s own URL.
Taken from the document: the two approved routes between the Barra da Tijuca vertiport (CEMHS) and Galeão airport flown in its 2021 simulation exercise — a main corridor with an 11-minute average trip and a shoreline alternative in the 15–20 minute range (its p. 52); the suggested eVTOL route list connecting Barra, Copacabana, Centro and Galeão among others (p. 55); the airport-demand proportions of its market study — Barra 12%, Copacabana 22%, Centro 7% of Galeão’s passengers (p. 22); and its expectation of multiple fleet operators acting at the same time (p. 52). Stylized by us: congestion coefficients and demand units. The document itself declares its network vision generic (“vertiport locations are generic”, p. 55), and this instance follows suit: it is illustrative, not Eve’s data, and asserts nothing about any traffic-management product.
Route choice on a congested network is a Wardrop equilibrium problem: each population takes the cheapest route available to it, and a flow is at equilibrium when no one can switch and do better. Here the network has four nodes — Barra, Copacabana, Centro, Galeão — and four corridors, with affine costs cʳₖ = aₖ + bₖ·(total flow) + gₖ·(own-population flow). This cost is symmetric across populations, so the game is a potential game, and uniqueness has a structural test: the per-edge cost Jacobian is positive definite exactly when gₖ > 0 and R·bₖ + gₖ > 0 — an exact integer check whose smallest eigenvalue is the stated margin. Evaluating a sufficient condition on an instance is standard practice, not a new method; the modern multi-population condition line is due to Colombo, Giuzzi & Marcellini (J. Optim. Theory Appl. 206:31, 2025, DOI 10.1007/s10957-025-02706-4), and the bridge between mean-field games on networks and Wardrop equilibrium is Al Saleh, Bakaryan, Gomes & Ribeiro’s (arXiv:2207.01397). What this page contributes is the instance-level verdict: exact equilibria, an exact margin where uniqueness holds, and an honest refusal where it does not.
Three populations head for the airport with the document’s demand proportions as integer units — Barra 12, Copacabana 22, Centro 7. Barra can fly the main corridor or the shoreline chain; the others join the shared corridors mid-way. Solved exactly over BigInt rationals (an active-set KKT solve; no floating point anywhere in the certificate):
| quantity | value (exact) | meaning |
|---|---|---|
| Barra’s split | 128/11 main · 4/11 shoreline | the population genuinely uses both routes — the Wardrop choice is live, not degenerate |
| Kirchhoff conservation | 0 | identically zero, per population — not a tolerance |
| support tightness | 0 | every used route exactly cheapest — identically zero |
| off-support slack | ≥ 0 | no unused route is a shortcut |
| minimum support flow | 4/11 | strictly positive — the support is honest |
| uniqueness margin | 1 | smallest eigenvalue of the per-edge Jacobians, exact integer — the condition holds with room stated, not asserted |
| independent restart | identical | re-solved from the opposite route seed; same support, same exact flows |
Now the document’s other expectation: two fleet operators, six flights each, sharing the two approved corridors — and congestion costs that depend on total corridor occupancy, blind to whose aircraft it is (g = 0). Equilibrium still pins the corridor totals exactly: 29/4 of the twelve flights on the main corridor, 19/4 on the shoreline. But the uniqueness condition now fails exactly — the determinant of the cost Jacobian’s symmetric part is identically zero, with the operator-swap direction in its null space — and this is not a technicality: the operator assignment is a one-dimensional face of equally valid equilibria, operator A’s main-corridor share ranging over [5/4, 6], width 19/4. The verifier exhibits both extremes and the midpoint and checks each one exactly. The point-uniqueness certificate is REFUSED, with the witness printed.
Why this is worth a page. A simulation or optimizer run on this instance converges to one split and reports it, silently choosing the equilibrium for you; nothing in its output reveals that a whole family of other assignments was equally consistent. The exact computation makes the indeterminacy itself the result: equilibrium does not decide who flies which corridor here — something else must. That “something else” has a name in the air-traffic-management literature: equilibrium selection, a stated design goal of recent decentralized-ATM work (arXiv:2602.15333). This page’s contribution to that conversation is a machine-checkable instance where the selection problem is exhibited rather than assumed.
The map around the instance, first — two exact boundaries the verifier re-derives. Scaling every demand by a factor t, the shoreline route becomes economically active at exactly t = 5/9: below it Barra rides the main corridor alone, and the whole three-corridor chain enters at once (routes enter as paths, not one corridor at a time). And the operator-assignment face of scenario two exists exactly when total operator demand exceeds 5/2; below that, everyone fits on the main corridor and the assignment is forced.
Then the question scenario two leaves open: if equilibrium will not choose, what does? Two classical selection mechanisms, both computed exactly on this instance. A differentiated per-operator price — any positive amount, however small — restores determinacy, and the vanishing-price limit is the textbook Tikhonov selection: it picks the least-norm point of the solution face (Mangasarian & Meyer, SIAM J. Control Optim. 17, 1979, DOI 10.1137/0317052). With asymmetric operators (eight flights against four, same corridor totals) that point is exactly 37/8 — equivalently, operators split their demand difference equally — and the verifier witnesses the least-norm identity directly, in exact arithmetic. A bounded-rationality learner (a logit-smoothed best response, the quantal-response tradition of McKelvey & Palfrey, DOI 10.1006/game.1995.1023) also forgets where it started and also selects — the demand-proportional split, exactly 29/6: the shape the traffic literature names by its condition of proportionality (Bar-Gera, Boyce & Nie, Transp. Res. B 46, 2012, DOI 10.1016/j.trb.2011.10.010), with entropy-based selection of flow splits studied since 1989 and, for the multi-class case, as recently as Entropy maximization in multi-class traffic assignment (Transp. Res. B 192, 2025, DOI 10.1016/j.trb.2024.103136). The two selected points differ by exactly 5/24 and coincide only when the operators are identical. The other two dynamics tested complete the picture: plain deterministic best response never selects at all — its landing point is a fossil of its starting condition — and random perturbation never settles, finding the face’s centre only as a long-run average.
None of the mechanisms is new here, and neither is the bare fact that different selections can differ — a least-norm point and a maximum-entropy point of a face part company whenever the face is asymmetric, a one-line convexity observation on top of decades-old theorems, and comparing quantal-response selections is itself a published genre (Zhang & Hofbauer, Games Econ. Behav. 97, 2016, DOI 10.1016/j.geb.2016.03.002). What we have not located — a documented search, which is evidence and not proof — is a published instance-level computation exhibiting both selection limits in exact arithmetic against an exactly certified face. That executable object is this section’s contribution: press the third button on the figure above and the gauge shows both classical selections sitting at different points of the same certified face. The learning experiments behind the qualitative claims ran under a preregistered, seeded battery whose first registration was partly falsified — by the registrant’s own errors, kept in the battery header as the record, in this site’s usual way.
| tie-breaker | selects | here (exact) |
|---|---|---|
| vanishing differentiated price | the equal-difference point | 37/8 |
| bounded-rationality (quantal) learning | the proportional point | 29/6 |
| deterministic best response | nothing — the start decides | start-dependent |
| random perturbation | nothing — averages the centre | 29/8 in time-average |
The instance is illustrative. Its topology and free-flow times follow the ConOps; its congestion coefficients and demand units are stylized. No operational conclusion about Rio de Janeiro, about any operator, or about any product follows from it — and “mathematically certified” here means exact-arithmetic verification of an equilibrium statement, never anything a regulator certifies.
What is new here is narrow, and stated as such. Equilibrium models for urban air mobility exist: the closest assignment paper computes a system-optimal plan (Wang, Delahaye, Farges & Alam, J. Aerospace Info. Systems 2021, DOI 10.2514/1.I010954 — their own text: cooperative assignment minimizing total cost), and a land–air network-equilibrium model with a model-level existence-and-uniqueness statement is published (Zhang, Liu, Dong, Zhou, Liu & Chen, Transp. Res. Part A, 2024, DOI 10.1016/j.tra.2024.104160; the precise condition sits behind the paywall and is not characterized here). Applying an exact-equilibrium toolkit to a new domain is routine for anyone holding the toolkit. What we have not located — by a documented search, which is evidence and not proof — is prior work that computes a UAM corridor equilibrium in exact or interval arithmetic, states a uniqueness condition’s margin on the instance, or issues REFUSED/MULTIPLE as a first-class per-instance verdict. That narrow, checkable packaging is this page’s contribution; the finding of scenario two is what it is for.
Self-published, not peer-reviewed; the checks and the code share one author. The verifier below is how you disagree with this page by running something.
The verifier is a single file, published beside this page — Node only, nothing installed. It recomputes every number above in exact rationals and ends with two mutation controls that must go red, because a check that has never been seen failing proves nothing:
git clone --depth 1 https://github.com/carlostoledo1891/mfg-lab
cd mfg-lab/technical-reports/lane/uam-corridor
node verify.js # 13 checks, incl. 2 mutation controls -> ALL PASS, exit 0What counts as a certificate on this site — and what gets refused the word — is defined once, at /certificates. The refusal grammar this page uses (an honest REFUSED as a first-class verdict) is the same one the Wardrop reproduction and the uniqueness-certificate pages earn their results with.