witness_D3
plain-language theorem explainer
For ambient dimension D = 3 the witness defect index is p = 1. Anyone citing the explicit same-sector linking witnesses (U10) or the loop-loop specialization that forces D = 3 will use this evaluation. The proof is a one-line decidable arithmetic check of (3 − 1)/2.
Claim. The witness index attached to ambient dimension $D = 3$ equals $1$: if $p(D) = (D-1)/2$, then $p(3) = 1$.
background
The module supplies linking nontriviality witnesses for the paper's U5 (Alexander duality selector) and U10 (converse for the allowed set $A_A$). For loop-loop linking the duality statement $H_1(S^D \ K) \cong \mathbb{Z}$ holds precisely when $D = 3$, encoded at the pinned commit by a circle-reduced cohomology nontriviality predicate that forces the degree to be 1.
Same-sector arithmetic alone permits every odd $D \ge 3$. The converse half of Proposition 3.5 (that every such odd dimension supports nontrivial same-sector linking) is witnessed by a concrete geometric construction: in $\mathbb{R}^{2p+1}$ two standard $p$-spheres in complementary position have linking number $\pm 1$. The auxiliary map witness_p records the sphere dimension $p = (D-1)/2$ used by that construction.
proof idea
Pure computation. Unfold $p(D) = (D-1)/2$, substitute $D = 3$, and discharge $(3-1)/2 = 1$ by the decide tactic (Nat arithmetic is decidable).
why it matters
Closes the first concrete instance of the U10 witness family (siblings cover $D = 5,7,9$). Together with the loop-loop specialization $p = 1$, it anchors the topological forcing of spatial dimension $D = 3$ (forcing-chain landmark T8) inside the verification layer. The module doc ties the same data to the Alexander-duality selector and to the audit that same-sector parity only yields odd dimensions, while $p = 1$ recovers uniqueness of $D = 3$. No downstream consumers are recorded yet; the value is the explicit base case for the allowed-set converse.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.