# Shortest paths - 2026-10-02 [Proved] For `bang dim 2, code 7` at odd side `N` and level `L` the closures of all voids are pairwise disjoint, so paths through corner contacts never arise, the closed set and its interior give the same shortest-path distance, and the visibility graph on void corners computes it exactly. Witness: walks.md, section "Shortest paths: two limits that do not commute". - 2026-10-02 [Proved] The corner distance of `bang dim 2, code 7` at odd side `N` and level `L` satisfies `sqrt(2) <= D(N, L) <= 2 - (2 - sqrt(2)) (1 - 1/N)^L`, so `lim_(N -> infinity) D(N, L) = sqrt(2)` at every level and `limsup_(N -> infinity) D(N, cN) <= 2 - (2 - sqrt(2)) e^(-c)`. Witness: walks.md, section "Shortest paths: two limits that do not commute". - 2026-10-02 [Proved] For odd `N >= 5` the limit set of `bang dim 2, code 7` at side `N` holds no segment of non-axis slope, every rectifiable path in it is at least as long as the taxicab distance between its ends, and `D(N, L)` is nondecreasing in `L` with limit `2`, so the side and level limits of the corner distance do not commute; no rate is proved. Witness: walks.md, section "Shortest paths: two limits that do not commute". - 2026-10-02 [Proved] At side 3, `D(3, L) = 2 sqrt(5)/3` at every level `L >= 1` and in the limit, attained by `(0,0) -> (2/3, 1/3) -> (1,1)` of slopes `1/2` and `2`. Witness: walks.md, section "Shortest paths: two limits that do not commute". - 2026-10-02 [Proved] At level 1, `D(N, 1) = sqrt(2) + (2 sqrt(5) - 3 sqrt(2))/N` for every odd `N`. Witness: walks.md, section "Shortest paths: two limits that do not commute". - 2026-10-02 [Proved] At infinite side the level-1 street grid of `bang dim 2, code 7` has exactly the axes and the diagonals as free directions, and a line of slope `s` in `(0, 1)` that rises 3 rows passes a point whose disc of radius `(1 - s)/(2 (1 + s))` lies inside a void, a sharp radius. Witness: walks.md, section "Shortest paths: two limits that do not commute". - 2026-10-02 [Proved] The map `Phi`, the stable norm of the street grid carrying a norm, is monotone, satisfies `Phi(nu) >= nu` and fixes the free directions, and `Phi^L(euclid)` increases to the regular octagon gauge `oct` uniformly; every fixed point has as ball the octagon of its own free unit vectors, so `oct` is the only one equal to `1` on them. Witness: walks.md, section "Shortest paths: two limits that do not commute". - 2026-10-02 [Proved] For `bang dim 3, code 23` with paths in the closed filled cells, the map's free directions are the 6 axes and the 12 face diagonals, the body diagonals are blocked, and `Phi^L(euclid)` increases to the gauge of the hull of the 18 free unit vectors, which has 18 vertices, 48 edges and 32 triangular faces. Witness: walks.md, section "Shortest paths: two limits that do not commute"; `lab/py/carpet-geodesics`, verb `hull`, recounts. - 2026-10-02 [Verified] Exact corner distances of `bang dim 2, code 7`: `D(3, L) = 1.490711985000` at `L = 1..4`, `D(5, L) = 1.460112615949, 1.485180310941, 1.504787873051` at `L = 1, 2, 3`, `D(7, L) = 1.446998600642, 1.464884551783` at `L = 1, 2`, `D(9, 2) = 1.458269875850`, `D(11, 2) = 1.449562910791`. Witness: `lab/py/carpet-geodesics`, verb `corner`. - 2026-10-02 [Verified] `D(N, 1) = sqrt(2) + (2 sqrt(5) - 3 sqrt(2))/N` at every odd `N` from 3 to 41, to `4.4e-16`. Witness: `lab/py/carpet-geodesics`, verb `level1`. - 2026-10-02 [Verified] Upper bounds from cycle points of the true ball, window 6 periods: `Phi^L(euclid)` at angle `22.5` degrees is at most `1.029173, 1.050508, 1.064891, 1.073404` at `L = 1..4` against `oct = 1.082392`, so its gap to the octagon is at least `5.21e-2, 3.26e-2, 1.85e-2, 9.71e-3`. Witness: `lab/py/carpet-geodesics`, verb `map`. - 2026-10-02 [Verified] The exact level-1 distance from `(0,0)` to `(1, (N-1)/(2N))` reads `1.122716, 1.135394, 1.136527, 1.139652` at `N = 11, 21, 31, 41` against `1.128108, 1.135734, 1.138440, 1.139826` from the level-1 norm, within `0.06/N`. Witness: `lab/py/carpet-geodesics`, verb `bridge`. - 2026-10-02 [Verified] At level 2, `N (D(N, 2) - sqrt(2))` reads `0.354834, 0.354697, 0.396507, 0.388843` at `N = 5, 7, 9, 11` against `0.458991`, twice the level-1 constant, and `N (D(5, 3) - sqrt(2)) = 0.452872` against `0.688486`. Witness: `lab/py/carpet-geodesics`, verb `corner` with `5,3 11,2`. - 2026-10-02 [Refuted] An excess of the corner distance over `sqrt(2)` of at least `a L log N / N` for some `a > 0`. Witness: the proved envelope `D(N, L) - sqrt(2) <= (2 - sqrt(2)) L/N`, walks.md, section "Shortest paths: two limits that do not commute". - 2026-10-02 [Conjecture] Side first then level first, the render's distance tends to the octagon gauge, `lim_L lim_N d_(N,L)(x, y) = oct(x - y)`; it follows from the map theorem once `lim_N d_(N,L) = Phi^L(euclid)` is proved; likewise the render of `bang dim 3, code 23` tends to the gauge of the hull of the 18 free unit vectors. Witness: `lab/py/carpet-geodesics`, verb `bridge`, at dim 2 level 1 only; dim 3 untested.