The Missing Graph-Theoretic Ingredient Vertex Distinguishability in G16 and the Canonical Relational Realisation

We prove that in the Hasse diagram G16 of the Boolean lattice 2^[4] over F_2^4 ≅ (Z/2Z)^4, no two distinct vertices share the same undirected neighbourhood. That is, the neighbourhood map v ↦ N(v), where N(v) = {v ⊕ e_i : i ∈ [4]}, is injective on F_2^4. The proof is elementary and self-contained, using only the Hamming weight structure of the Boolean hypercube. This property—referred to as Lemma I5.1 in the internal documentation of the TAGC programme—provides the remaining graph-theoretic ingredient required in the proof of injectivity of the canonical relational realisation ι : (X, R) → (R^64/V_48, B̄) at level L2 of the programme; the complementary algebraic ingredient is supplied by the spectral structure of A_inter established in. We record it here as a standalone result, together with the proof, four clarifying remarks, and an account of its role in the TAGC deductive chain.