03-ilang-space / 04-neighbours
04neighboursverified
Summary Defines neighbouring points and a distance along chains of neighbours from the witness angle alone, and tests both on an explicit chain.
# External verification: 04-neighbours - **Subproject:** 03-ilang-space - **Package:** 04-neighbours - **Verified version:** v1 - **External round:** 1 of 2 - **Date:** 2026-10-08T16:49:07+02:00 - **Focus points:** none --- VERDICT: correct ## Summary The derivation answers all four requested items using the quoted inputs and stated assumptions. The order-invariance argument and finite-angle induction correctly establish the neighbour relation’s properties and preservation of connected components; the shortest-path construction correctly yields the claimed extended metric. The chain example is correctly derived for every finite \(m\ge1\), including the disconnected \(m=1\) case and the example with \(\ell>\pi/2\). ## Issues None. ## Focus points None given.