witness_D9

Module Verification.DimensionLinking supplies linking nontriviality witnesses for paper items U5 and U10. U5 encodes the Alexander-duality selector that forces $D = 3$ for loop-loop linking ($p = 1$); U10 supplies the converse direction of Proposition 3.5, that every odd $D \geq 3$ admits nontrivial same-sector linking.

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 auxiliary definition witness_p records the sphere dimension: for odd $D \geq 3$, $p = (D-1)/2$. Sibling facts pin the same arithmetic at $D = 3,5,7$ and the inequality $p \geq 1$ when $D \geq 3$.

One-line tactic proof: decide evaluates the closed natural-number expression $(9-1)/2$ against $4$ and closes by computation. No lemmas beyond the definition of the witness map are required.

Fills one concrete cell of the U10 witness table that supports the converse half of Proposition 3.5: every odd dimension $D \geq 3$ carries a nontrivial same-sector linking witness. Together with the $D = 3,5,7$ siblings it makes the infinite odd family $A_A = {3,5,7,\ldots}$ explicitly inhabited rather than parity-only. In the broader forcing chain this sits under the T8 claim that spatial dimension is three: same-sector arithmetic still permits all odd $D$, while the loop-loop specialization $p = 1$ selects $D = 3$. No downstream consumers are wired yet; the declaration is a leaf audit fact.