This is the condensed on-page manuscript. The attached PDF includes the complete discussion and executable Lean compiler listing; the versioned source archive includes the Rust backends and evidence.
Abstract
We specify transit optimization in the internal language of a topos with a natural number object (NNO), and interpret it in higher toposes. Directed journey categories yield simplicial route spaces, while weighted realizations determine which changes of representation preserve optimization. A Lean implementation provides typed arithmetic, logical and higher-cell terms, and compiles a finite resource-constrained fragment to Rust with scalar, AVX2 and Rayon backends. We prove finite-search correctness, exact-realization invariance, safe subdivision and a higher truncation principle. Kernel-checked lemmas and executable tests are distinguished from mathematical arguments and unverified backend code.
Keywords: natural number object; transit routing; simplicial set; enriched category; higher topos; dependent types; staged compilation.
1. Problem, scope and contribution
Can a bus-routing problem be represented in another topological or higher-categorical space without changing its optimal journeys? Yes, provided the representation retains direction, feasible composition, resource consumption and objective values. An unweighted homotopy type does not suffice.
We study passenger journey optimization in a fixed, finite timetable: minimize nonnegative integral generalized cost subject to a boarding budget and decidable edge constraints. This is a foundation for dispatch software, not a solution to every fleet-design, vehicle-routing or network-design problem. Vehicle capacities, driver duties and interactions among passengers require additional state or joint optimization.
2. Ambient topos, NNO and arithmetic
Let $\mathcal E$ be an elementary topos with a natural number object $(N,0,s)$. Thus for every $z:1\to A$ and $h:A\to A$ there is a unique $f:N\to A$ with $f0=z$ and $fs=hf$. Parameterized recursion follows in a cartesian closed category by transposing into an exponential. This universal property, rather than an assumed external machine integer type, specifies arithmetic.
Primitive recursion defines addition, multiplication, exponentiation, truncated subtraction, minimum, maximum, comparison, quotient and remainder. We choose total conventions $a/0=0$ and $a\bmod0=a$. The comparison relations on $N$ are decidable constructively. Given a decidable predicate, bounded conjunction and disjunction are computable by NNO recursion. These operations suffice for the executable constraints below. Negative integers and rationals admit further constructions, but the current backend uses bounded natural numbers; decidable comparison of arbitrary real numbers is not asserted.
Proposition 2.1 (finite internal minimization). Suppose a list of candidates has a specified finite length in $N$, a decidable feasibility predicate and a natural-valued objective. There is an internally definable operation returning either no feasible candidate or a feasible candidate with least objective value.
Proof. Fold over the list while maintaining an optional best candidate. Ignore infeasible entries; initialize from the first feasible entry; replace the current best precisely when a smaller objective is encountered. Decidability makes each branch available. NNO induction proves that the accumulator is empty exactly when no processed entry is feasible, and otherwise is feasible and no more expensive than every processed feasible entry. No excluded middle for general propositions or choice principle is used. $\square$
For an $\infty$-topos $\mathcal X$, take $N_{\mathcal X}=\coprod_{k\in\mathbb N}1$. It is $0$-truncated. The shift and zeroth summand define successor and zero; the space of recursion maps together with their coherent recursion data is contractible. One construction is the colimit of the initial chain for $1+(-)$; coproducts preserve the relevant colimit. Equivalently, recursion assigns the successive iterates of a specified endomorphism, with a contractible space of choices. We use this higher universal property, not a collection of independent numerals in each homotopy dimension. Arithmetic remains discrete even when the objects on which it acts have higher cells.
3. A decidable finite transit fragment
Work internally in $\mathcal E$. Fix a positive bound $n:N$, vertices $V=\{i:N\mid i<n\}$, and a finite list $E$ of directed, possibly parallel edges. Each edge carries source $u_e$, target $v_e$, cost $c_e:N$ and boarding count $b_e:N$. Require $u_e<v_e$ and $c_e<W$ for a positive $W$. A typed Boolean guard filters the list. Fix source $a$, destination $z$ and budget $B$.
A candidate is an edge-list path from $a$ to $z$ with total boardings at most $B$. Its objective is $c(p)=\sum_{e\in p}c_e$. The empty path is admitted at a vertex and has cost and resource zero. Strictly increasing ranks imply that a path has at most $n-1$ edges, so bounded enumeration is available. Repeated stops are permitted when they occur at distinct time-expanded states.
Write $D(v,j)$ for minimum cost to $v$ with exactly $j$ boardings, using a formal $\infty$ for the empty minimum. Initialize $D(a,0)=0$ and all other entries to $\infty$. In increasing vertex order, for each edge $e:u\to v$ and $j+b_e\le B$, update
$$D(v,j+b_e)\leftarrow\min\{D(v,j+b_e),D(u,j)+c_e\}.$$
Return $\min_{j\le B}D(z,j)$ and a predecessor witness, or infeasible.
Theorem 3.1 (internal DP correctness). This recurrence returns exactly the least cost of a feasible candidate, and a path attaining it when one exists.
Proof. At vertex $v$, every nonempty path ending there has a last edge from some $u<v$. Its prefix has already been processed. Conversely every update appends an actual allowed edge to a feasible prefix and adds its exact resources. Induction on vertex rank therefore proves equality between each finalized table entry and the minimum over paths with those endpoints and exact boarding count. Initialization supplies precisely the empty path. Minimization over the finitely many counts proves the claim. A finite minimizing predecessor exists whenever a value is finite; following predecessors strictly decreases vertex rank and reconstructs a witness. All induction and comparisons are internal NNO operations. $\square$
4. The simplicial route space
Let $C_G$ be the free category on the allowed finite directed graph. Objects are event states; arrows are actual directed edge-list journeys; composition concatenates lists. The nerve has
$$K_r=N(C_G)_r=\coprod_{x_0,\ldots,x_r}C_G(x_0,x_1)\times\cdots\times C_G(x_{r-1},x_r).$$
Faces compose or omit arrows, and degeneracies insert identities. Thus a $2$-simplex records $f,g,gf$ with their compositional compatibility; it is not an assertion that three nearby stops are mutually reachable. Associativity supplies the higher simplicial identities. The nerve is an $\infty$-category, generally not a Kan complex. Its realization $X_G=|K|$ is the requested alternative topological route space, used together with its original directed simplicial and weighted data.
The cost and resource label $w(p)=(c(p),b(p))$ is additive under composition. Consequently each triangular face satisfies $w(gf)=w(f)+w(g)$. Scalar shortest costs give a Lawvere metric with values in $([0,\infty],\ge,+,0)$: $d(x,x)=0$ and $d(x,z)\le d(x,y)+d(y,z)$. Symmetry is unnecessary. The finite resource table retains more information than a single scalar distance.
Proposition 4.1 (topology alone is insufficient). Ordinary homotopy equivalence of route realizations does not imply preservation of reachability or optimum cost.
Proof. A single directed edge and its reversal both realize an interval; fixing named endpoints, the reachability answers are opposite. Keeping its orientation and changing its cost from $1$ to $100$ leaves the entire unweighted nerve unchanged but changes the optimum. Inverting arrows to obtain a groupoid also admits reverse journeys that the input need not allow. $\square$
Theorem 4.2 (safe simplicial refinement). Replace an edge $u\to v$ by $u\to q\to v$, where $q$ is new, has no other incident edges, and is not a query endpoint. Split both labels additively into nonnegative integers. Then feasible endpoint journeys correspond bijectively with identical cost and boarding count.
Proof. Expand each occurrence of the original edge into the two new edges. Every path through $q$ must use exactly those two edges consecutively, so contraction gives the inverse. Additivity preserves labels and budget tests. The expanded graph has a compatible rank order obtained by topological sorting. A new guard must retain both refined edges, and new machine-range certificates must be checked; arbitrary guards are not automatically preserved by subdivision. $\square$
5. Higher cells, toposes and finite realization
Higher cells can express certified route rewrites, associators, commuting independent actions and coherent refinements. They do not automatically erase time or resource differences. For example, declare a $2$-cell between two routes only when the intended semantics permits that rewrite, and require equal objective/resource labels if the cell is to be invisible to this optimizer.
Proposition 5.1 (discrete objectives factor through components). If a mapping space $M$ in an $\infty$-topos has a cost map $M\to N_{\mathcal X}$, it factors uniquely up to contractible choice through its $0$-truncation $\tau_{\le0}M$.
Proof. This is the defining adjunction for $0$-truncation applied to a $0$-truncated target. Thus connected higher cells have identical cost under a genuinely defined cost map. The same applies to a pair of natural-valued labels and to decidable feasibility. $\square$
This proposition neither says that all routes are equivalent nor that higher witnesses have no verification value. It identifies exactly what a discrete objective can observe. The finite backend requires a finite realization of the relevant feasible components; it need not enumerate every syntactic representative.
Definition 5.2 (exact finite realization). A source specification has a type $S$ of semantic candidates, a feasibility predicate $F$ and objective $q:S\to N$. A finite routing problem $P$ realizes it when there are: (i) a decoder taking each feasible route $r$ of $P$ to $s_r:S$ with $F(s_r)$ and $q(s_r)=c(r)$; (ii) for every feasible $s:S$, some feasible $r$ with $c(r)=q(s)$. Injectivity is unnecessary.
Theorem 5.3 (minimum transport). If a least-cost feasible route of $P$ exists, its decoded candidate is a least-cost feasible source candidate. Conversely source feasibility is equivalent to route feasibility; infeasibility and the set of feasible objective values are preserved.
Proof. Decoding gives a feasible source candidate with the same cost. For every competing source candidate, clause (ii) supplies a route with that objective, so route minimality gives the required inequality. The two clauses give both inclusions of feasible objective-value sets and both directions of feasibility. $\square$
The theorem applies to terms in a higher-category model or the internal language of a topos when those terms come with the stated finite realization. It does not provide a decision procedure for arbitrary higher-topos terms. In particular, NNO recursion does not make unbounded quantification decidable.
6. Implemented Lean source language and compiler
Its source layer includes: a universe-polymorphic category with intrinsically typed composition; the NNO universal property and a checked set model; dimension-indexed higher-cell generators, identities and compositions; and a typed internal-language syntax with products, functions, $N$, Booleans, $\Omega$, power-object terms, primitive recursion, arithmetic, comparisons, and bounded quantifiers. Unbounded logical quantification is allowed into $\Omega$ but has no elimination into executable Boolean constraints.
The general compiler interface accepts any Lean type $\alpha$ together with an exact realization, including types of categorical/higher-cell or internal-language terms. In abbreviated form, the implemented contract is:
structure Realization {H n w} (α : Type u) (p : Problem H n w) where
feasible : α → Prop
objective : α → Nat
decode : Candidate p → α
sound : ∀ r, feasible (decode r)
costExact : ∀ r, objective (decode r) = r.val.cost
complete : ∀ a, feasible a → ∃ r : Candidate p,
r.val.cost = objective aThe emitter prints only checked natural-number literals in a fixed Rust template. The library provides the DP and witness reconstruction. Its integer sentinel is $I=2^{30}-1$; certificates require $nW<I$, $B\le65535$ and $n(B+1)\le16777216$. Thus every path cost is below $I$, and the target can distinguish unreachable from reachable entries. Rust revalidates the range contract, including user-supplied CLI budget overrides.
The implemented evaluator interprets terms in sets. HigherModel is an operation signature; laws and coherences of a nontrivial higher model must be supplied separately. The NNO set model is checked, but the general topos interpretation is mathematical semantics. This release does not implement all dependent type formers or automatically construct higher toposes.
7. Rust execution and accelerator contract
The AVX2 backend uses eight unsigned 32-bit lanes via Rust's std::arch intrinsics [8]. For an edge of resource $b$, lane $j$ updates destination lane $j+b$. Source rank is strictly lower than destination rank, so the slices are disjoint. Runtime feature detection selects AVX2 or a scalar fallback. Explicit avx2 requests fail on unsupported processors.
Proposition 7.1 (kernel equivalence under the range contract). The scalar, AVX2 and Rayon lane updates implement the same recurrence.
Proof. Each output lane is $\min(d,\min(I,s+c))$. All finite labels and $c$ are below $I$; hence even an unreachable label plus cost is below $2I<2^{31}$ and cannot wrap a 32-bit lane. Unsigned vector addition followed by unsigned minimum therefore agrees with scalar arithmetic and sentinel saturation. Full chunks update eight independent lanes; the tail uses the scalar operation. Rayon partitions distinct mutable destination entries [9]; edges remain sequential, so there is no shared-write race between edge updates. $\square$
This is a mathematical refinement argument, not a kernel-checked Rust proof. Unsafe intrinsic code, memory allocation, the Lean evaluator/compiler, source emission, Rust compilation and the processor remain in the execution trust boundary. There is no GPU backend in this release. A GPU implementation needs a separately checked memory, scheduling and arithmetic contract.
8. Reproducible evidence and limitations
Version 0.1.0 includes all source, a lockfile, generated Rust, positive/negative examples, tests, raw validation logs and benchmark data. Six Rust tests passed with Rayon enabled. One test compares scalar, automatic AVX2 and Rayon results on 600 deterministic small DAGs, and compares optimal values against exhaustive path enumeration. Other tests cover boarding budgets, invalid graphs/ranges, empty/unreachable routes, SIMD tails/sentinels and corrupted witnesses. Three Lean fixtures are intentionally rejected: a Boolean in arithmetic, a backward edge, and a dimension mismatch.
The example gives optimum costs $20,12,8$ for boarding budgets $0,1,2$. Both generated scalar/AVX2 execution and the Rayon executable produce a checked route witness for the compiled budget. #print axioms reports no axioms for minimum transport, the lowering projections, recursion equations or categorical associativity; the set-NNO construction uses the standard Quot.sound dependency through function extensionality. There are no admitted proofs or added axioms in the artifact. The full DP theorem, general higher-topos interpretation and Rust equivalence are proved on paper, not formalized end to end in Lean.
The distance-only synthetic benchmark used 256 vertices, 1,014 edges, budget 1,023, three warmups and 15 timed runs (Rust 1.85.1 release mode; four Rayon threads). It excludes compilation and witness validation, uses no real city data, and is not a comparison with RAPTOR/CSA.
| Backend | Median microseconds |
|---|---|
| Scalar | 922.148 |
| Automatic AVX2 | 171.288 |
| Rayon | 52327.352 |
9. Authorship, evidence and availability
Anonymous human-directed research submission. The responsible submitting human selected the problem, authorized anonymous submission and accepted the journal's interaction terms. An OpenAI assistant drafted the manuscript, implemented the software, ran the checks and prepared the artifacts. No independent referee review, field trial, formal Rust verification or deployment is claimed. Original software is distributed under the included MIT license. Proofs and evidence are open to correction. The submission bundle contains the full Lean compiler, Rust library, reproducibility instructions and this manuscript; its ready artifacts become publicly accessible only if the journal approves publication.
References
[1] D. Delling, T. Pajor and R. F. Werneck. Round-Based Public Transit Routing. ALENEX, 2012. Author-hosted publication and paper.
[2] J. Dibbelt, T. Pajor, B. Strasser and D. Wagner. Connection Scan Algorithm. arXiv:1703.05997, 2017. Manuscript.
[3] F. W. Lawvere. Metric Spaces, Generalized Logic, and Closed Categories. 1973; TAC reprint 1, 2002. Journal reprint.
[4] M. Grandis. The Fundamental Weighted Category of a Weighted Space. arXiv:math/0604506, 2006. Manuscript.
[5] J. Lurie. Higher Topos Theory. Princeton University Press, 2009; arXiv:math/0608040. Author's manuscript record.
[6] GTFS. Schedule Reference, consulted 1 November 2026. Official specification.
[7] Lean project. The Lean Language Reference, sections on the type system, IO and compilation, consulted 1 November 2026. Official manual.
[8] Rust project. core::arch, _mm256_min_epu32 and runtime feature detection. Intrinsic documentation; feature detection.
[9] Rayon contributors. Rayon, version 1.10.0 used in the artifact. Project repository.