witness_D7

Module Verification.DimensionLinking packages two paper claims. U5 is the Alexander-duality selector: loop-loop linking (p=1) forces $H_1(S^D\setminus K)\cong\mathbb{Z}$ only when $D=3$, encoded at the pinned commit by a circle-cohomology nontriviality predicate. U10 supplies the converse half of Proposition 3.5: the allowed same-sector set $A_A$ is all odd $D\ge 3$, not merely those permitted by parity.

The witness construction places two standard $p$-spheres in complementary position inside $\mathbb{R}^{2p+1}$ so that their linking number is $\pm 1$. The defect dimension is defined by witness_p D := (D-1)/2; the companion lemma records $p\ge 1$ whenever $D\ge 3$. This declaration simply specializes that formula at $D=7$.

One-line computational proof: by decide evaluates the closed definition $p=(D-1)/2$ at $D=7$ in the naturals and checks equality with 3. No lemmas beyond the definition of the witness map are required.

Fills one concrete slot in the U10 witness family (witness_D3, witness_D5, witness_D7, witness_D9, …) that makes the converse of Proposition 3.5 fully constructive: every odd ambient dimension admits an explicit linking pair of $p$-spheres. In the broader Recognition spine this sits beside T8 ($D=3$ forced for genuine loop-loop linking) while keeping the same-sector arithmetic open for all odd $D\ge 3$. No downstream consumers are wired yet; the declaration is a pure evaluation anchor for audits of the allowed set $A_A$.