allowed_set_A_characterization
plain-language theorem explainer
The allowed same-sector dimension set equals the odd naturals at least 3: existence of a linking degree p ≥ 1 with D = 2p+1 is equivalent to D odd and D ≥ 3. Citation target for the T8 / U10 audit that same-sector arithmetic does not force D = 3 by itself. Proof is a two-direction constructor: one side applies the oddness lemma, the other rebuilds p from an explicit witness.
Claim. For every natural number $D$, there exists an integer $p \ge 1$ such that $D = 2p+1$ if and only if $D \ge 3$ and $D$ is odd.
background
Module Verification.DimensionLinking packages the U5/U10 linking witnesses that connect Alexander duality to the forced spatial dimension. Same-sector linking of two $p$-spheres in $\mathbb{R}^D$ is arithmetically possible precisely when $D = 2p+1$ for some $p \ge 1$; the paper's set $A_A$ is the collection of such ambient dimensions.
The forward direction is the elementary parity fact already recorded as same_sector_forces_odd: any $D = 2p+1$ with $p \ge 1$ is odd and at least 3. The converse needs an explicit reconstruction of $p$ from $D$, supplied by the local witness family (witness_p, witness_p_ge_one, witness_reconstruction). Loop-loop linking is the special case $p = 1$, which pins $D = 3$ only after the Alexander-duality selector is imposed; the present characterization deliberately stops at the parity level.
Framework landmark: T8 forces spatial dimension $D = 3$ only after the loop-loop specialization, not from same-sector arithmetic alone.
proof idea
Term-mode constructor on the biconditional.
Left-to-right: unpack the existential $\langle p, hp, hD\rangle$ and apply same_sector_forces_odd D p hp hD, which returns $D \ge 3$ and oddness.
Right-to-left: from $D \ge 3$ and $\neg 2 \mid D$, build the witness triple $\langle$witness_p D, witness_p_ge_one hD, witness_reconstruction hD hodd$\rangle$. The first component is the reconstructed $p = (D-1)/2$; the second proves $p \ge 1$; the third restores $D = 2p+1$.
why it matters
Closes the arithmetic half of paper Proposition 3.5: $A_A = {3,5,7,\ldots}$. Downstream audit theorem t8_same_sector_allows_odd_dimensions is literally the symmetric form of this biconditional, and its doc-comment states the intended reading: "Same-sector linking arithmetic permits every odd $D \ge 3$; the loop-loop specialization $p = 1$ is an additional choice."
In the forcing chain this separates T8's genuine topological input (Alexander duality / circle-reduced cohomology forcing $D = 3$ for $p = 1$) from the weaker parity constraint that would otherwise leave all odd dimensions open. Without this characterization the U10 converse (every odd $D \ge 3$ supports a nontrivial same-sector witness) would remain a prose claim rather than a Lean fact.
Switch to Lean above to see the machine-checked source, dependencies, and usage graph.