Plectis Atlas
Incompressible transport of solid boxes
Family 376: Universal computation in forced Navier–Stokes flows
No paper statement selected
no paper statement matches the Lean text clearly enough to pair, so the closest candidates are listed below.
The Lean statement says
theorem balanced_box_routing (n : ℕ) (a b h k : Fin n → RationalSpace) (hh : ∀ i j, 0 < h i j) (hk : ∀ i j, 0 < k i j) (ha : Pairwise fun i j => Disjoint (solidBox (a i) (h i)) (solidBox (a j) (h j))) (hb : Pairwise fun i j => Disjoint (solidBox (b i) (k i)) (solidBox (b j) (k j))) (hvol : ∀ i, ∏ j : Fin 3, k i j / h i j = 1) : ∃ U : Field, ∃ Φ : ℝ → Space → Space, AdmissibleField U ∧ IsGlobalFlow U Φ ∧ Delivers a b h k Φ := by sorryA Lean statement states the theorem and leaves its proof as sorry on purpose. OpenAI’s proof is in a separate solution module, and a program called Comparator checks that proof against this statement.