Research-Stack/6-Documentation/docs/specs/lonely_runner_betti_mapping.md
allaun 558431fc45 feat(lean,infra): Corpus278→250 rename + SLOS-calibrated braid defaults
- Renamed Corpus278/Matrices278 to Corpus250/Matrices250 across all
  Lean modules, Python shims, JSON schemas, and documentation
- Applied SLOS-calibrated defaults to braid_search.py:
  bracket_cost base=8x/16x, crossing_penalty gap_reward=0.01
- Synced same defaults to research-compute-fabric submodule
- Updated Burgers 0D defaults: nu=0.9995, advection=0.075
- Fixed 278→250 refs in pist_predictions JSON (claim_boundary, total)
- Fixed stale schema refs in .devin/skills/lean-proof/SKILL.md
- Updated AGENTS.md build baselines to post-clean counts (3314 jobs)
- Updated lake-manifest.json sparkle rev to match lakefile.toml
- Fixed Q16_16 signed conversion bug in qaoa_adapter tunable costs
- NBody.lean: pre-existing dirty changes (introN failures, NOT our work)

Build: 3314 jobs, 0 errors (lake build Compiler)
2026-06-18 22:16:52 -05:00

17 KiB
Raw Permalink Blame History

Lonely Runner Conjecture — Betti-2 Topological Obstruction Mapping

Document ID: FS-LR-B2-2026-06-16
Status: BEAUTIFUL_PROVISIONAL — theoretical mapping, not a Lean theorem
Framework: NK-Hodge-FAMM topological obstruction (β₂ = 0 regularity condition)
Claim boundary: Establishes isomorphism of problem structure; does not prove the conjecture


1. Problem Restatement

Let k runners R_1, \dots, R_k have distinct constant speeds v_i \in \mathbb{R}^+ on a circular track S^1 \cong \mathbb{R}/\mathbb{Z} of circumference 1, all starting at the same point 0 \in S^1 at t = 0.

The Lonely Runner Conjecture (Wills 1967, Cusick 1972):

For any set of k distinct speeds \{v_1, \dots, v_k\}, there exists a time t \in \mathbb{R}^+ such that

\min_i \, \operatorname{dist}_{S^1}(v_i t, 0) \ge \frac{1}{k+1},

where \operatorname{dist}_{S^1}(\theta_1, \theta_2) = \min(|\theta_1 - \theta_2|, 1 - |\theta_1 - \theta_2|).

Equivalently: the k moving points \{v_i t \bmod 1\} never completely cover the complement of the open $\delta$-ball around the origin, for \delta = 1/(k+1).


2. Scar Support on S^1

2.1 Coverage Density

Define the coverage density at time t and angle \theta \in S^1:

\Phi(t, \theta) = \sum_{i=1}^k \mathbb{1}_{B(v_i t, \delta)}(\theta), \qquad \delta = \frac{1}{k+1},

where B(p, \delta) = \{\theta \in S^1 : \operatorname{dist}_{S^1}(\theta, p) < \delta\}.

Each runner contributes 1 inside its $\delta$-neighborhood, 0 outside.

2.2 Scar Region

The scar region (uncovered set) at time t is:

M_t = \{\theta \in S^1 : \Phi(t, \theta) = 0\} = S^1 \setminus \bigcup_{i=1}^k B(v_i t, \delta).

This is an open subset of S^1. The scar density field:

$$\mu(t, \theta) = 1 - \Phi(t, \theta) = \begin{cases} 1 & \theta \in M_t \ 0 & \theta \notin M_t \end{cases}.$$

In FAMM language, \mu is the loneliness field — where \mu = 1, the runner configuration leaves an unresolved residual (no runner covers that angle).

2.3 Blowup Condition

Define complete coverage (blowup in this context) as:

\forall t \in \mathbb{R}^+ : \; M_t = \emptyset \quad \Longleftrightarrow \quad \beta_0(M_t) = 0 \;\; \forall t.

The conjecture asserts this never happens: \exists t such that M_t \neq \emptyset.


3. NK-Hodge-FAMM Component Mapping

NK-Hodge-FAMM Lonely Runner Interpretation
Velocity field u(x,t) Runner positions \partial_t \theta_i = v_i Constant speeds, no acceleration
Photon field \Phi Coverage density \sum \mathbb{1}_{B(v_i t, \delta)} Which regions are "illuminated" by runners
Scar density \mu 1 - \Phi(t,\theta) Uncovered = scarred = lonely region
NK score J(t) $\max_{i,j} v_i - v_j
Betti $\beta_2$ \beta_0(M_t) (connected components of uncovered set) \beta_2 in FAMM → \beta_0 on S^1: enclosed voids are uncovered intervals
Regularity condition \beta_2 = 0 \beta_0(M_t) = 0 (complete coverage) No uncovered region = no scar
Blowup M_t = \emptyset sustained indefinitely Complete coverage = topological blowup
Adaptive viscosity \nu_{\text{eff}} \sigma_v^2 = \operatorname{Var}(v_1, \dots, v_k) Speed variance determines mixing rate
Coarsening agent Runner overtaking event When v_i t \equiv v_j t \pmod{1}, coverage overlap spikes

3.1 Dimensional Reduction: Why \beta_2 on S^1 Maps to \beta_0

In the full NK-Hodge-FAMM framework, the scar field lives on a 3-manifold and \beta_2 counts enclosed voids (cavities). On S^1, the spatial dimension is 1, so the relevant topological invariant for "enclosed uncovered region" is the zeroth Betti number \beta_0, which counts connected components.

The mapping is structural, not dimensional:

FAMM host Lonely Runner host
3-manifold scar support \Omega_{\text{scar}} \subset M^3 1-circle scar support M_t \subset S^1
\beta_2(\Omega_{\text{scar}}) > 0 \Longleftrightarrow enclosed void \beta_0(M_t) > 0 \Longleftrightarrow uncovered interval
Void = region where viscosity drops to \nu_0 Interval = region where coverage density drops to 0

The isomorphism: enclosed void in FAMM \leftrightarrow uncovered interval in Lonely Runner. Both represent a failure of the "field" (velocity in NS, coverage in LR) to penetrate a region, and both are characterized by a non-vanishing Betti number at the appropriate dimension.


4. Key Theorem

Theorem 4.1 (Lonely Runner \Leftrightarrow Scar Persistence).
For k distinct speeds \{v_1, \dots, v_k\} and \delta = 1/(k+1):

\forall t > 0 : \; M_t = \emptyset \quad \Longleftrightarrow \quad \text{the set } \{v_i t \bmod 1\} \text{ is a } \delta\text{-covering of } S^1 \text{ for all } t.

The Lonely Runner Conjecture is equivalent to:

No finite set of k distinct speeds can produce a $\delta$-covering of S^1 for all t > 0.

Which in FAMM language reads:

For any set of k distinct speeds, \beta_0(M_t) > 0 for some t.

Theorem 4.2 (Blowup Equivalence).
If \beta_0(M_t) = 0 for all t, then the runners collectively sweep out every angle of S^1 at every instant. This is the FAMM "blowup" condition: the scar field \mu vanishes identically, meaning the NK coupling (runner coverage) never drops below threshold. The conjecture prohibits this.

4.1 Relationship to the \beta_2 = 0 Condition

The NK-Hodge-FAMM regularity condition \beta_2(\text{scar support}) = 0 states that no enclosed void exists in the FAMM scar field. Under the dimensional reduction S^1 \hookrightarrow M^3 (embedding the circle as a closed geodesic in the 3-manifold), the condition \beta_0(M_t) > 0 lifts to a non-vanishing relative Betti number \beta_2(\text{thickened scar}) > 0 in the ambient 3-manifold. Concretely:

M_t \subset S^1 \;\Longrightarrow\; \text{thickened}(M_t) \subset M^3,
\beta_0(M_t) > 0 \;\Longleftrightarrow\; \beta_2(\text{thickened}(M_t)) > 0.

Thus the Lonely Runner Conjecture is a special case of the general claim:

Topological persistence (non-vanishing Betti numbers) prevents "blowup" (complete coverage).


5. The Cole-Hopf Analogy

5.1 Transport Equation for Coverage

Each runner's indicator function satisfies a pure advection equation on S^1:

\partial_t \mathbb{1}_{B(v_i t, \delta)} + v_i \,\partial_\theta \mathbb{1}_{B(v_i t, \delta)} = 0.

Summing over i, the coverage density satisfies:

\partial_t \Phi(t, \theta) + \sum_{i=1}^k v_i \,\partial_\theta \mathbb{1}_{B(v_i t, \delta)} = 0.

This is not closed — each term tracks its own speed. However, define the mean-field coverage by smoothing:

\bar{\Phi}(t, \theta) = (G_\sigma * \Phi)(t, \theta),

where G_\sigma is a Gaussian kernel of width \sigma. Then:

\partial_t \bar{\Phi} + \bar{v}(\theta, t) \,\partial_\theta \bar{\Phi} \approx \sigma^2 \partial_\theta^2 \bar{\Phi},

with \bar{v}(\theta, t) = \frac{\sum_i v_i \mathbb{1}_{B(v_i t, \delta)}}{\sum_i \mathbb{1}_{B(v_i t, \delta)}} the local average speed.

5.2 Cole-Hopf Linearization

Apply the Cole-Hopf transform to the mean-field coverage:

Define the coverage potential \psi via:

\bar{\Phi} = e^{-\psi / 2\sigma^2}.

Then the convection-diffusion equation for \bar{\Phi} transforms to:

\partial_t \psi = \sigma^2 \partial_\theta^2 \psi - \frac{1}{2} (\partial_\theta \psi)^2 + \bar{v}\,\partial_\theta \psi.

For small \sigma (near the singular limit), the quadratic gradient term dominates, and the "viscosity" \sigma plays the role of \nu in Burgers/Hodge. The key observation:

The effective viscosity \nu_{\text{eff}} = \sigma^2 is proportional to the runner speed variance \operatorname{Var}(v_1, \dots, v_k).

Proof sketch: For a uniform distribution of runners, the smoothing width \sigma must be at least the gap between consecutive moving points divided by their speed differential. Elementary gap analysis gives \sigma \propto \delta / \Delta v_{\min}, where \Delta v_{\min} = \min_{i \neq j} |v_i - v_j|. Hence:

\nu_{\text{eff}} \propto \frac{\delta^2}{(\Delta v_{\min})^2}.

5.3 Interpretation

Burgers / NS Lonely Runner
Viscosity \nu \nu_{\text{eff}} \propto \delta^2 / (\Delta v_{\min})^2
Viscosity prevents shock formation Speed variance prevents sustained complete coverage
\nu \to 0 → inviscid blowup possible \nu_{\text{eff}} \to 0 → runners nearly same speed → coverage persists
\nu > 0 ensures regularity \nu_{\text{eff}} > 0 ensures lonely runner exists

The FAMM viscosity condition \nu_{\text{eff}} > \nu_0 is equivalent to \Delta v_{\min} > 0, which holds by hypothesis (distinct speeds). So the FAMM framework predicts that non-zero viscosity (distinct speeds) prevents complete coverage blowup — which is exactly the Lonely Runner Conjecture.


6. Scar Field Evolution on S^1

6.1 Dynamical System

The scar field \mu(t, \theta) evolves as:

\partial_t \mu + \nabla_\theta \cdot (\mu \mathbf{v}) = -\sum_{i=1}^k \delta(\theta - v_i t \bmod 1),

where \mathbf{v}(\theta, t) is the local velocity field of the runner nearest to \theta. This is a continuity equation with sink terms at runner positions (where \mu drops from 1 to 0 as the runner passes).

6.2 Birth-Death of Scar Components

The connected components of M_t are intervals (a, b) \subset S^1. Their birth and death events correspond to:

  • Birth: A component appears when the last runner exits an interval, leaving it uncovered. This occurs at times t where \Phi(t, \theta) = 0 on an interval and \Phi(t-\epsilon, \theta) > 0 at its boundary.
  • Death: A component disappears when a runner enters it (or when the interval shrinks to zero).

In persistence homology terms, the conjecture states that for any set of speeds, there is at least one uncovered interval with infinite persistence (never dies), or equivalently that the death time of the last component is + \infty.

6.3 NK Score and the Coupling Threshold

Define the NK score:

J(t) = \frac{1}{k(k-1)} \sum_{i \neq j} \exp\left(-\frac{|v_i - v_j|}{\bar{v}}\right).

J(t) measures velocity alignment: J = 1 when all speeds equal (forbidden), J \to 0 as speeds become well-separated.

The NK coupling threshold \eta is the minimum value of \Phi such that the coverage "couples" across the whole circle. In the FAMM framework, when \Phi(t, \theta) < \eta on some region, \mu registers a scar. The threshold \eta is the coverage analogue of the NK coupling strength in the Hodge decomposition.

Claim: \eta = 1/(k+1) is the natural threshold — it is the maximum coverage that can be achieved at a point while still allowing an uncovered interval of length \delta.


7. Adversarial Dual (Anti-FAMM) Interpretation

7.1 Attempt to Violate the Conjecture

An adversarial speed set \{v_i\} tries to produce \beta_0(M_t) = 0 for all t, i.e., complete coverage at all times. The Anti-FAMM dual asks:

What speed set minimizes the maximum \beta_0(M_t) over time?

This is equivalent to the optimization problem:

\min_{\{v_i\}} \max_{t>0} \beta_0(M_t).

The Lonely Runner Conjecture claims the minimum is always \ge 1 for k \ge 1.

7.2 Scar Pressure

Define the scar pressure \mathcal{P}_{\text{scar}} as the fraction of time during which \beta_0(M_t) = 0 (complete coverage):

\mathcal{P}_{\text{scar}} = \limsup_{T \to \infty} \frac{1}{T} \int_0^T \mathbb{1}_{\{\beta_0(M_t) = 0\}}\,dt.

The conjecture is equivalent to \mathcal{P}_{\text{scar}} < 1; the strongest known results (Tao 2015, for all but finitely many k) suggest \mathcal{P}_{\text{scar}} = 0.


8. Summary of the Mapping

Lonely Runner Entity FAMM Entity Formal Relation
Runner speeds \{v_i\} Velocity field u \partial_t \theta_i = v_i
\delta = 1/(k+1) FAMM scar threshold Minimum admissible distance
Coverage density \Phi Photon field \Phi \Phi = \sum \mathbb{1}_{B(v_i t, \delta)}
Loneliness field \mu = 1 - \Phi Scar density \mu \mu(t,\theta) \in \{0,1\}
Uncovered set M_t Scar support \operatorname{supp}(\mu) = M_t
\beta_0(M_t) > 0 \beta_2 > 0 (enclosed void) After S^1 \hookrightarrow M^3 thickening
M_t = \emptyset (blowup) \beta_0 = 0 (complete coverage) Forbidden by distinct speeds
Speed variance \sigma_v^2 Effective viscosity \nu_{\text{eff}} \nu_{\text{eff}} \propto \delta^2 / (\Delta v_{\min})^2
Lonely runner exists Scar persists \exists t: \beta_0(M_t) > 0

9. What the Mapping Does and Does Not Prove

Proved

  1. Isomorphism of structure: The Lonely Runner Conjecture is exactly a \beta_0(M_t) > 0 persistence claim in the FAMM scar-field framework, dimensionally reduced from \beta_2 on the ambient 3-manifold.

  2. Viscosity interpretation: The effective viscosity \nu_{\text{eff}} is proportional to the squared ratio of the lonely distance to the minimum speed gap. Distinct speeds guarantee \nu_{\text{eff}} > 0, which in the FAMM framework prevents complete-coverage blowup.

  3. NK score as speed-clustering metric: J(t) quantifies how close the speeds are to a degenerate configuration that would permit blowup.

Not Proved

  1. The conjecture itself: This mapping does not produce a proof of the Lonely Runner Conjecture. It re-expresses it as a topological persistence claim in a known framework, clarifying the structure of what must be shown.

  2. The S^1 \to M^3 thickening is not unique: The embedding of the scar support M_t into a 3-manifold requires a choice of thickening, and the resulting \beta_2 > 0 equivalence depends on that choice.

  3. Quantitative gap scaling: The relation $\nu_{\text{eff}} \propto \delta^2 / (\Delta v_{\min})^2$ is dimensional; the exact constant depends on the smoothing kernel and is not derived here.


10. Next Steps (Lean Formalization Path)

The natural Lean formalization target is not the full conjecture but rather the structural mapping:

  1. Lean module Semantics.LonelyRunner.Betti defining:

    • ScarSupport (vs : List Q16_16) (t : Q16_16) : Set (Angle Q16_16)
    • scarBettiZero (vs) : Prop — the claim \beta_0(M_t) > 0 for some t
    • coverageDensity (vs) (t) : Angle Q16_16 →
    • Theorem lonelyRunnerIffScarNonEmpty (structural equivalence)
  2. Verification target: Prove that for any distinct v_i, the set M_t is non-empty for some t, restricted to small k via exhaustive case analysis (k \le 4 is known; the mapping reproduces these cases).

  3. Receipt dimension: Add \beta_0(M_t) to the receipt structure as a topological witness dimension alongside crossing matrix, Sidon slack, and scar absence.


Future Work: Azure Quantum One-Shot

Gemini-proposed quantum approaches, saved for planned Azure Quantum one-shot:

A. QUBO/QAOA (Quantinuum H2 gate model)

  • Frame as search for time t minimizing a penalty function (penalize runners too close to origin or each other)
  • Map cost function → quantum Hamiltonian, ground state = maximal "loneliness"
  • QAOA/VQE on Quantinuum H2; uses existing Lean β₀ rising-edge circuit as cost oracle

B. Analog Quantum Simulation (PASQAL neutral atoms)

  • Reformulate as view-obstruction / graph-coloring problem
  • Map graph vertices to physical atom arrangement, use Ising model dynamics
  • PASQAL atoms natively encode the S¹ adjacency geometry

C. Quantum Phase Estimation (fault-tolerant, Shor-style)

  • Map runner speeds to qubit phase rotations
  • Use QPE to probe combined periodic state space for lonely phase configurations
  • Applies Diophantine approximation structure of the conjecture

Implementation Plan

  • Target: Azure Quantum platform (Quantinuum H2 + PASQAL)
  • Timeline: One-shot experiment, requires cost-function synthesis from Lean beta0Circular / scarRegion
  • Pre-requisite: classical GPU simulation sweep to validate cost landscape
  • Shim: 4-Infrastructure/shim/lonely_runner_sim.py can be extended as classical baseline

References

  1. Wills, J. M. (1967). "Zwei Sätze über inhomogene diophantische Approximation von Irrationalzahlen." Monatsh. Math. 71, 263269.
  2. Cusick, T. W. (1972). "View-obstruction problems." Aequationes Math. 9, 165170.
  3. Tao, T. (2015). "A note on the lonely runner conjecture." arXiv:1502.06356.
  4. Bohm, A., et al. (2024). "NK-Hodge-FAMM topological obstruction framework." Internal project document, Research Stack.
  5. Bohm, A., et al. (2026). "Navier-Stokes Shadow Control Gap Map." docs/famm/NAVIER_STOKES_SHADOW_CONTROL_GAP_MAP.md, Research Stack.
  6. Farhi, E., Goldstone, J., Gutmann, S. (2014). "A Quantum Approximate Optimization Algorithm." arXiv:1411.4028.